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  511  19.38a  1841  ax13lem1  2381  ax13lem2  2383  axc11n  2437  sbequiALT  2572  reuss2  4235  reupick  4239  elinxp  5856  ordtr2  6203  suc11  6262  funimass4  6705  fliftfun  7044  omlimcl  8187  nneob  8262  rankwflemb  9206  cflm  9661  domtriomlem  9853  grothomex  10240  sup3  11585  caubnd  14710  fbflim2  22582  ellimc3  24482  usgruspgrb  26974  usgredgsscusgredg  27249  3cyclfrgrrn1  28070  dfon2lem6  33146  opnrebl2  33782  bj-nfimt  34084  axc11n11r  34130  bj-nnf-alrim  34199  stdpc5t  34265  wl-ax13lem1  34911  diaintclN  38354  dibintclN  38463  dihintcl  38640  pm11.71  41101  axc11next  41110  rrx2plord2  45136