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  3598  reuss2  4277  reupick  4280  elinxp  5970  ordtr2  6352  suc11  6416  funimass4  6887  fliftfun  7249  omlimcl  8496  nneob  8574  rankwflemb  9689  cflm  10144  domtriomlem  10336  grothomex  10723  sup3  12082  caubnd  15266  fbflim2  23862  ellimc3  25778  usgruspgrb  29128  usgredgsscusgredg  29405  3cyclfrgrrn1  30229  dfon2lem6  35762  opnrebl2  36295  bj-nfimt  36612  axc11n11r  36657  bj-nnf-alrim  36729  stdpc5t  36801  wl-ax13lem1  37468  diaintclN  41037  dibintclN  41146  dihintcl  41323  sn-sup3d  42465  dflim5  43302  pm11.71  44370  axc11next  44379  rrx2plord2  48707