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  245  syl3an3  1361  ax12  2304  hbae  2315  ax12OLD  2341  tz7.7  5749  fvmptt  6300  f1oweALT  7152  wfrlem12  7426  nneneq  8143  pr2nelem  8827  cfcoflem  9094  nnunb  11288  ndvdssub  15133  lsmcv  19141  gsummoncoe1  19674  uvcendim  20186  2ndcsep  21262  atcvat4i  29256  mdsymlem5  29266  sumdmdii  29274  dfon2lem6  31693  frrlem11  31792  colineardim1  32168  bj-hbaeb2  32805  hbae-o  34188  ax12fromc15  34190  cvrat4  34729  llncvrlpln2  34843  lplncvrlvol2  34901  dihmeetlem3N  36594  eel2122old  38943