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  1841  ax13lem1  2378  ax13lem2  2380  axc11n  2430  rspc6v  3597  reuss2  4278  reupick  4281  elinxp  5978  ordtr2  6362  suc11  6426  funimass4  6898  fliftfun  7258  omlimcl  8505  nneob  8584  rankwflemb  9705  cflm  10160  domtriomlem  10352  grothomex  10740  sup3  12099  caubnd  15282  fbflim2  23921  ellimc3  25836  usgruspgrb  29256  usgredgsscusgredg  29533  3cyclfrgrrn1  30360  dfon2lem6  35980  opnrebl2  36515  bj-nfimt  36838  axc11n11r  36884  bj-nnf-alrim  36956  stdpc5t  37028  wl-ax13lem1  37699  diaintclN  41318  dibintclN  41427  dihintcl  41604  sn-sup3d  42747  dflim5  43571  pm11.71  44638  axc11next  44647  rrx2plord2  48968