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  507  19.38a  1840  ax13lem1  2372  ax13lem2  2374  axc11n  2424  rspc6v  3606  reuss2  4285  reupick  4288  elinxp  5979  ordtr2  6365  suc11  6429  funimass4  6907  fliftfun  7269  omlimcl  8519  nneob  8597  rankwflemb  9722  cflm  10179  domtriomlem  10371  grothomex  10758  sup3  12116  caubnd  15301  fbflim2  23840  ellimc3  25756  usgruspgrb  29086  usgredgsscusgredg  29363  3cyclfrgrrn1  30187  dfon2lem6  35749  opnrebl2  36282  bj-nfimt  36599  axc11n11r  36644  bj-nnf-alrim  36716  stdpc5t  36788  wl-ax13lem1  37455  diaintclN  41025  dibintclN  41134  dihintcl  41311  sn-sup3d  42453  dflim5  43291  pm11.71  44359  axc11next  44368  rrx2plord2  48684