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  2378  ax13lem2  2380  axc11n  2430  rspc6v  3622  reuss2  4301  reupick  4304  elinxp  6006  ordtr2  6397  suc11  6461  funimass4  6943  fliftfun  7305  omlimcl  8590  nneob  8668  rankwflemb  9807  cflm  10264  domtriomlem  10456  grothomex  10843  sup3  12199  caubnd  15377  fbflim2  23915  ellimc3  25832  usgruspgrb  29162  usgredgsscusgredg  29439  3cyclfrgrrn1  30266  dfon2lem6  35806  opnrebl2  36339  bj-nfimt  36656  axc11n11r  36701  bj-nnf-alrim  36773  stdpc5t  36845  wl-ax13lem1  37512  diaintclN  41077  dibintclN  41186  dihintcl  41363  sn-sup3d  42515  dflim5  43353  pm11.71  44421  axc11next  44430  rrx2plord2  48702