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  1872  ax13lem1  2403  ax13lem2  2405  axc11n  2455  rspc6v  3596  reuss2  4270  reupick  4273  axprglem  5394  elinxp  6010  ordtr2  6411  suc11  6475  funimass4  6954  fliftfun  7324  omlimcl  8593  nneob  8672  rankwflemb  9807  rankwflembOLD  9808  cflm  10334  domtriomlem  10527  grothomex  10921  sup3  12281  caubnd  15535  fbflim2  24305  ellimc3  26208  usgruspgrb  29773  usgredgsscusgredg  30049  3cyclfrgrrn1  30895  dfon2lem6  36646  opnrebl2  37205  axtco1from2  37359  bj-nfimt  37618  axc11n11r  37681  bj-nnf-alrim  37743  stdpc5t  37835  wl-ax13lem1  38526  diaintclN  42224  dibintclN  42333  dihintcl  42510  sn-sup3d  43665  dflim5  44440  pm11.71  45490  axc11next  45499  rrx2plord2  49943