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  1846  ax13lem1  2373  ax13lem2  2375  axc11n  2425  reuss2  4201  reupick  4205  elinxp  5857  ordtr2  6210  suc11  6269  funimass4  6728  fliftfun  7072  omlimcl  8228  nneob  8303  rankwflemb  9288  cflm  9743  domtriomlem  9935  grothomex  10322  sup3  11668  caubnd  14801  fbflim2  22721  ellimc3  24623  usgruspgrb  27118  usgredgsscusgredg  27393  3cyclfrgrrn1  28214  dfon2lem6  33328  opnrebl2  34140  bj-nfimt  34446  axc11n11r  34492  bj-nnf-alrim  34564  stdpc5t  34630  wl-ax13lem1  35277  diaintclN  38684  dibintclN  38793  dihintcl  38970  pm11.71  41537  axc11next  41546  rrx2plord2  45586