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  2406  ax13lem2  2408  axc11n  2458  rspc6v  3600  reuss2  4274  reupick  4277  axprglem  5401  elinxp  6026  ordtr2  6434  suc11  6498  funimass4  6980  fliftfun  7351  omlimcl  8624  nneob  8703  rankwflemb  9837  rankwflembOLD  9838  cflm  10366  domtriomlem  10559  grothomex  10953  sup3  12314  caubnd  15570  fbflim2  24351  ellimc3  26254  usgruspgrb  29821  usgredgsscusgredg  30097  3cyclfrgrrn1  30943  elpssmo  36673  dfon2lem6  36765  opnrebl2  37324  axtco1from2  37478  bj-nfimt  37737  axc11n11r  37800  bj-nnf-alrim  37862  stdpc5t  37954  wl-ax13lem1  38685  diaintclN  42381  dibintclN  42490  dihintcl  42667  sn-sup3d  43822  dflim5  44592  pm11.71  45642  axc11next  45651  rrx2plord2  50166