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  6583  tfrcl  6639  mkvprop  7505  ccfunen  7637  caucvgprprlemval  8062  suplocsrlem  8182  peano5uzti  9766  seqf1oglem2  10979  zfz1iso  11316  wrd2ind  11518  lcmneg  12878  prmind2  12924  pcfac  13159  cnmpt12  15525  cnmpt22  15532  limccnp2lem  15914  2sqlem6  16456  2sqlem8  16459  gropd  16505  grstructd2dom  16506  sbthom  17289