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 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl9r  79  com23  87  sylan9  517  19.38a  1873  ax13lem1  2409  ax13lem2  2411  axc11n  2461  rspc6v  3605  reuss2  4282  reupick  4285  axprglem  5410  elinxp  6021  ordtr2  6410  suc11  6474  funimass4  6949  fliftfun  7314  omlimcl  8565  nneob  8644  rankwflemb  9767  cflm  10243  domtriomlem  10436  grothomex  10824  sup3  12182  caubnd  15421  fbflim2  24149  ellimc3  26053  usgruspgrb  29548  usgredgsscusgredg  29824  3cyclfrgrrn1  30651  dfon2lem6  36290  opnrebl2  36864  axtco1from2  37018  bj-nfimt  37277  axc11n11r  37340  bj-nnf-alrim  37402  stdpc5t  37494  wl-ax13lem1  38172  diaintclN  41864  dibintclN  41973  dihintcl  42150  sn-sup3d  43298  dflim5  44088  pm11.71  45139  axc11next  45148  rrx2plord2  49534