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  508  19.38a  1842  ax13lem1  2373  ax13lem2  2375  axc11n  2425  rspc6v  3630  reuss2  4314  reupick  4317  elinxp  6017  ordtr2  6405  suc11  6468  funimass4  6953  fliftfun  7305  omlimcl  8574  nneob  8651  rankwflemb  9784  cflm  10241  domtriomlem  10433  grothomex  10820  sup3  12167  caubnd  15301  fbflim2  23472  ellimc3  25387  usgruspgrb  28430  usgredgsscusgredg  28705  3cyclfrgrrn1  29527  dfon2lem6  34748  opnrebl2  35194  bj-nfimt  35503  axc11n11r  35549  bj-nnf-alrim  35621  stdpc5t  35693  wl-ax13lem1  36363  diaintclN  39917  dibintclN  40026  dihintcl  40203  dflim5  42064  pm11.71  43141  axc11next  43150  rrx2plord2  47361