Theorem syl3c 63

Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)

Hypotheses

Ref	Expression
syl3c.1	⊢ (𝜑 → 𝜓)
syl3c.2	⊢ (𝜑 → 𝜒)
syl3c.3	⊢ (𝜑 → 𝜃)
syl3c.4	⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))

Assertion

Ref	Expression
syl3c	⊢ (𝜑 → 𝜏)

Proof of Theorem syl3c

Step	Hyp	Ref	Expression
1		syl3c.3	. 2 ⊢ (𝜑 → 𝜃)
2		syl3c.1	. . 3 ⊢ (𝜑 → 𝜓)
3		syl3c.2	. . 3 ⊢ (𝜑 → 𝜒)
4		syl3c.4	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
5	2, 3, 4	sylc 62	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
6	1, 5	mpd 13	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  bilukdc  1445  disjiun  4125  tfrlem1  6579  tfrcl  6635  mkvprop  7498  ccfunen  7630  caucvgprprlemval  8055  suplocsrlem  8175  peano5uzti  9756  seqf1oglem2  10959  zfz1iso  11295  wrd2ind  11497  lcmneg  12854  prmind2  12900  pcfac  13131  cnmpt12  15390  cnmpt22  15397  limccnp2lem  15779  2sqlem6  16251  2sqlem8  16254  gropd  16300  grstructd2dom  16301  sbthom  17083