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  1836  ax13lem1  2376  ax13lem2  2378  axc11n  2428  rspc6v  3642  reuss2  4331  reupick  4334  elinxp  6038  ordtr2  6429  suc11  6492  funimass4  6972  fliftfun  7331  omlimcl  8614  nneob  8692  rankwflemb  9830  cflm  10287  domtriomlem  10479  grothomex  10866  sup3  12222  caubnd  15393  fbflim2  24000  ellimc3  25928  usgruspgrb  29214  usgredgsscusgredg  29491  3cyclfrgrrn1  30313  dfon2lem6  35769  opnrebl2  36303  bj-nfimt  36620  axc11n11r  36665  bj-nnf-alrim  36737  stdpc5t  36809  wl-ax13lem1  37476  diaintclN  41040  dibintclN  41149  dihintcl  41326  sn-sup3d  42478  dflim5  43318  pm11.71  44392  axc11next  44401  rrx2plord2  48571