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  507  19.38a  1841  ax13lem1  2376  ax13lem2  2378  axc11n  2428  rspc6v  3595  reuss2  4276  reupick  4279  elinxp  5976  ordtr2  6360  suc11  6424  funimass4  6896  fliftfun  7256  omlimcl  8503  nneob  8582  rankwflemb  9703  cflm  10158  domtriomlem  10350  grothomex  10738  sup3  12097  caubnd  15280  fbflim2  23919  ellimc3  25834  usgruspgrb  29205  usgredgsscusgredg  29482  3cyclfrgrrn1  30309  dfon2lem6  35929  opnrebl2  36464  bj-nfimt  36781  axc11n11r  36827  bj-nnf-alrim  36899  stdpc5t  36971  wl-ax13lem1  37638  diaintclN  41257  dibintclN  41366  dihintcl  41543  sn-sup3d  42689  dflim5  43513  pm11.71  44580  axc11next  44589  rrx2plord2  48910