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  1438  disjiun  4078  tfrlem1  6465  tfrcl  6521  mkvprop  7341  ccfunen  7466  caucvgprprlemval  7891  suplocsrlem  8011  peano5uzti  9571  seqf1oglem2  10759  zfz1iso  11081  wrd2ind  11276  lcmneg  12617  prmind2  12663  pcfac  12894  cnmpt12  14982  cnmpt22  14989  limccnp2lem  15371  2sqlem6  15820  2sqlem8  15823  gropd  15869  grstructd2dom  15870  sbthom  16508