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

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  79  com23  87  sylan9  516  19.38a  1870  ax13lem1  2406  ax13lem2  2408  axc11n  2458  rspc6v  3602  reuss2  4279  reupick  4282  axprglem  5407  elinxp  6018  ordtr2  6406  suc11  6470  funimass4  6945  fliftfun  7310  omlimcl  8559  nneob  8638  rankwflemb  9761  cflm  10228  domtriomlem  10421  grothomex  10809  sup3  12167  caubnd  15406  fbflim2  24134  ellimc3  26038  usgruspgrb  29533  usgredgsscusgredg  29809  3cyclfrgrrn1  30636  dfon2lem6  36278  opnrebl2  36832  axtco1from2  36986  bj-nfimt  37245  axc11n11r  37308  bj-nnf-alrim  37370  stdpc5t  37462  wl-ax13lem1  38140  diaintclN  41832  dibintclN  41941  dihintcl  42118  sn-sup3d  43266  dflim5  44056  pm11.71  45107  axc11next  45116  rrx2plord2  49502