Theorem syl9 78

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 74	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  79  com23  87  sylan9  516  19.38a  1867  ax13lem1  2412  ax13lem2  2414  axc11n  2464  rspc6v  3611  reuss2  4287  reupick  4290  axprglem  5408  elinxp  6019  ordtr2  6407  suc11  6471  funimass4  6946  fliftfun  7311  omlimcl  8562  nneob  8641  rankwflemb  9764  cflm  10232  domtriomlem  10425  grothomex  10813  sup3  12171  caubnd  15409  fbflim2  24102  ellimc3  26006  usgruspgrb  29473  usgredgsscusgredg  29749  3cyclfrgrrn1  30576  dfon2lem6  36176  opnrebl2  36720  axtco1from2  36874  bj-nfimt  37133  axc11n11r  37196  bj-nnf-alrim  37258  stdpc5t  37350  wl-ax13lem1  38027  diaintclN  41721  dibintclN  41830  dihintcl  42007  sn-sup3d  43155  dflim5  43947  pm11.71  44998  axc11next  45007  rrx2plord2  49386