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 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  bilukdc  1441  disjiun  4103  tfrlem1  6538  tfrcl  6594  mkvprop  7448  ccfunen  7574  caucvgprprlemval  7999  suplocsrlem  8119  peano5uzti  9682  seqf1oglem2  10878  zfz1iso  11206  wrd2ind  11408  lcmneg  12764  prmind2  12810  pcfac  13041  cnmpt12  15139  cnmpt22  15146  limccnp2lem  15528  2sqlem6  15980  2sqlem8  15983  gropd  16029  grstructd2dom  16030  sbthom  16793