Theorem syl7 74

Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses

Ref	Expression
syl7.1	⊢ (𝜑 → 𝜓)
syl7.2	⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏)))

Assertion

Ref	Expression
syl7	⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏)))

Proof of Theorem syl7

Step	Hyp	Ref	Expression
1		syl7.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3		syl7.2	. 2 ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏)))
4	2, 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:  syl7bi  256  ax12  2431  hbae  2439  ceqsalt  3466  elabgtOLD  3618  tz7.7  6343  fvmptt  6963  f1oweALT  7921  nneneq  9137  cfcoflem  10192  nnunb  12431  ndvdssub  16376  lsmcv  21141  uvcendim  21829  gsummoncoe1  22301  2ndcsep  23449  atcvat4i  32493  mdsymlem5  32503  sumdmdii  32511  axsepg4  35331  dfon2lem6  36021  colineardim1  36296  bj-hbaeb2  37178  hbae-o  39402  ax12fromc15  39404  cvrat4  39942  llncvrlpln2  40056  lplncvrlvol2  40114  dihmeetlem3N  41804  naddgeoa  43846  eel2122old  45168