Theorem syl3c 84

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

Hypotheses

Ref	Expression
syl3c.1	|- (ph -> ps)
syl3c.2	|- (ph -> ch)
syl3c.3	|- (ph -> th)
syl3c.4	|- (ps -> (ch -> (th -> ta)))

Assertion

Ref	Expression
syl3c	|- (ph -> ta)

Proof of Theorem syl3c

Step	Hyp	Ref	Expression
1		syl3c.3	. 2 |- (ph -> th)
2		syl3c.1	. . 3 |- (ph -> ps)
3		syl3c.2	. . 3 |- (ph -> ch)
4		syl3c.4	. . 3 |- (ps -> (ch -> (th -> ta)))
5	2, 3, 4	sylc 83	. 2 |- (ph -> (th -> ta))
6	1, 5	mpd 29	1 |- (ph -> ta)

Syntax hints:   -> wi 3

This theorem is referenced by:  fodomr 5547  sbcoreleleq 5830  ordelordaxr 5833  trsbc 5843  psasym 9994  pstr 9995  pjoi0 11297  atomli 11954  bnj1128 13428  ee110 16567  ee101 16569  ee011 16571  ee100 16573  ee010 16575  ee001 16577  cvrat4 17076

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

Copyright terms: Public domain