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  3609  reuss2  4289  reupick  4292  elinxp  5990  ordtr2  6377  suc11  6441  funimass4  6925  fliftfun  7287  omlimcl  8542  nneob  8620  rankwflemb  9746  cflm  10203  domtriomlem  10395  grothomex  10782  sup3  12140  caubnd  15325  fbflim2  23864  ellimc3  25780  usgruspgrb  29110  usgredgsscusgredg  29387  3cyclfrgrrn1  30214  dfon2lem6  35776  opnrebl2  36309  bj-nfimt  36626  axc11n11r  36671  bj-nnf-alrim  36743  stdpc5t  36815  wl-ax13lem1  37482  diaintclN  41052  dibintclN  41161  dihintcl  41338  sn-sup3d  42480  dflim5  43318  pm11.71  44386  axc11next  44395  rrx2plord2  48711