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  510  19.38a  1836  ax13lem1  2388  ax13lem2  2390  axc11n  2444  sbequiOLD  2530  sbequiALT  2592  reuss2  4282  reupick  4286  elinxp  5889  ordtr2  6234  suc11  6293  funimass4  6729  fliftfun  7064  omlimcl  8203  nneob  8278  rankwflemb  9221  cflm  9671  domtriomlem  9863  grothomex  10250  sup3  11597  caubnd  14717  fbflim2  22584  ellimc3  24476  usgruspgrb  26965  usgredgsscusgredg  27240  3cyclfrgrrn1  28063  dfon2lem6  33033  opnrebl2  33669  bj-nfimt  33971  axc11n11r  34017  bj-nnf-alrim  34084  stdpc5t  34150  wl-ax13lem1  34745  diaintclN  38193  dibintclN  38302  dihintcl  38479  pm11.71  40727  axc11next  40736  rrx2plord2  44708