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  1396  disjiun  3998  tfrlem1  6308  tfrcl  6364  mkvprop  7155  ccfunen  7262  caucvgprprlemval  7686  suplocsrlem  7806  peano5uzti  9360  zfz1iso  10820  lcmneg  12073  prmind2  12119  pcfac  12347  cnmpt12  13757  cnmpt22  13764  limccnp2lem  14115  2sqlem6  14437  2sqlem8  14440  sbthom  14744