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  506  19.38a  1835  ax13lem1  2368  ax13lem2  2370  axc11n  2420  rspc6v  3628  reuss2  4318  reupick  4321  elinxp  6028  ordtr2  6420  suc11  6483  funimass4  6967  fliftfun  7324  omlimcl  8608  nneob  8686  rankwflemb  9836  cflm  10293  domtriomlem  10485  grothomex  10872  sup3  12223  caubnd  15363  fbflim2  23972  ellimc3  25899  usgruspgrb  29119  usgredgsscusgredg  29396  3cyclfrgrrn1  30218  dfon2lem6  35612  opnrebl2  36033  bj-nfimt  36342  axc11n11r  36388  bj-nnf-alrim  36460  stdpc5t  36532  wl-ax13lem1  37201  diaintclN  40757  dibintclN  40866  dihintcl  41043  sn-sup3d  42252  dflim5  42995  pm11.71  44071  axc11next  44080  rrx2plord2  48110