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  515  19.38a  1860  ax13lem1  2405  ax13lem2  2407  axc11n  2457  rspc6v  3602  reuss2  4278  reupick  4281  axprglem  5393  elinxp  6005  ordtr2  6391  suc11  6455  funimass4  6931  fliftfun  7296  omlimcl  8547  nneob  8626  rankwflemb  9751  cflm  10206  domtriomlem  10399  grothomex  10787  sup3  12149  caubnd  15386  fbflim2  24034  ellimc3  25938  usgruspgrb  29381  usgredgsscusgredg  29657  3cyclfrgrrn1  30484  dfon2lem6  36133  opnrebl2  36678  axtco1from2  36832  bj-nfimt  37092  axc11n11r  37155  bj-nnf-alrim  37217  stdpc5t  37309  wl-ax13lem1  37985  diaintclN  41679  dibintclN  41788  dihintcl  41965  sn-sup3d  43111  dflim5  43903  pm11.71  44970  axc11next  44979  rrx2plord2  49341