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  509  19.38a  1843  ax13lem1  2374  ax13lem2  2376  axc11n  2426  rspc6v  3632  reuss2  4316  reupick  4319  elinxp  6020  ordtr2  6409  suc11  6472  funimass4  6957  fliftfun  7309  omlimcl  8578  nneob  8655  rankwflemb  9788  cflm  10245  domtriomlem  10437  grothomex  10824  sup3  12171  caubnd  15305  fbflim2  23481  ellimc3  25396  usgruspgrb  28441  usgredgsscusgredg  28716  3cyclfrgrrn1  29538  dfon2lem6  34760  opnrebl2  35206  bj-nfimt  35515  axc11n11r  35561  bj-nnf-alrim  35633  stdpc5t  35705  wl-ax13lem1  36375  diaintclN  39929  dibintclN  40038  dihintcl  40215  dflim5  42079  pm11.71  43156  axc11next  43165  rrx2plord2  47408