Theorem syl9 78

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 74	1 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl9r  79  com23  87  sylan9  517  19.38a  1873  ax13lem1  2404  ax13lem2  2406  axc11n  2456  rspc6v  3597  reuss2  4272  reupick  4275  axprglem  5394  elinxp  6008  ordtr2  6407  suc11  6471  funimass4  6947  fliftfun  7318  omlimcl  8579  nneob  8658  rankwflemb  9793  rankwflembOLD  9794  cflm  10320  domtriomlem  10513  grothomex  10907  sup3  12267  caubnd  15519  fbflim2  24289  ellimc3  26192  usgruspgrb  29757  usgredgsscusgredg  30033  3cyclfrgrrn1  30879  dfon2lem6  36530  opnrebl2  37089  axtco1from2  37243  bj-nfimt  37502  axc11n11r  37565  bj-nnf-alrim  37627  stdpc5t  37719  wl-ax13lem1  38397  diaintclN  42095  dibintclN  42204  dihintcl  42381  sn-sup3d  43536  dflim5  44315  pm11.71  45366  axc11next  45375  rrx2plord2  49803