Theorem syl9 77

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

Hypotheses

Ref	Expression
syl9.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl9.2	⊢ (𝜃 → (𝜒 → 𝜏))

Assertion

Ref	Expression
syl9	⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

Proof of Theorem syl9

Step	Hyp	Ref	Expression
1		syl9.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl9.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏)))
4	1, 3	syl5d 73	1 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

Syntax hints:   → wi 4

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

This theorem is referenced by:  syl9r  78  com23  86  sylan9  499  19.21tOLDOLD  2241  19.21t-1OLD  2386  ax13lem1  2422  ax13lem2  2463  axc11n  2474  sbequi  2534  reuss2  4108  reupick  4112  elinxp  5637  elresOLD  5639  ordtr2  5981  suc11  6044  funimass4  6468  fliftfun  6786  omlimcl  7895  nneob  7969  rankwflemb  8903  cflm  9357  domtriomlem  9549  grothomex  9936  sup3  11265  caubnd  14321  fbflim2  21994  ellimc3  23857  usgruspgrb  26291  usgredgsscusgredg  26583  3cyclfrgrrn1  27460  dfon2lem6  32013  opnrebl2  32637  bj-nfimt  32932  axc11n11r  32988  stdpc5t  33127  wl-ax13lem1  33605  diaintclN  36839  dibintclN  36948  dihintcl  37125  pm11.71  39097  axc11next  39106