Theorem syl8 24

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.

Hypotheses

Ref	Expression
syl8.1	⊢ (φ → (ψ → (χ → θ)))
syl8.2	⊢ (θ → τ)

Assertion

Ref	Expression
syl8	⊢ (φ → (ψ → (χ → τ)))

Proof of Theorem syl8

Step	Hyp	Ref	Expression
1		syl8.1	. 2 ⊢ (φ → (ψ → (χ → θ)))
2		syl8.2	. . 3 ⊢ (θ → τ)
3	2	imim2i 17	. 2 ⊢ ((χ → θ) → (χ → τ))
4	1, 3	syl6 22	1 ⊢ (φ → (ψ → (χ → τ)))

Syntax hints:   → wi 3

This theorem is referenced by:  syl8ib 215  a12studyALT 1418  onfr 3014  suctr 3055  ssorduni 3147  tfindsg 3213  findsg 3245  tz7.49 4260  nneneq 4659  aceq6b 4888  ltbtwnpq 5238  reclem3pr 5312  suppsr2 5377  qreccl 6412  iserzgt0 7415  nmoubi 8689  nmopub 10112  nmfnleub 10129  sumdmdlem2 10628  prj1 10809  bwt2 11123  altretop 11144  com45 11325  a1i4 11334  ordiso 11426  compsub 11488  isufil2 11650  txcn 11979

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain