Theorem mpsyl 59

Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)

Hypotheses

Ref	Expression
mpsyl.1	|- ph
mpsyl.2	|- (ps -> ch)
mpsyl.3	|- (ph -> (ch -> th))

Assertion

Ref	Expression
mpsyl	|- (ps -> th)

Proof of Theorem mpsyl

Step	Hyp	Ref	Expression
1		mpsyl.1	. . 3 |- ph
2	1	a1i 9	. 2 |- (ps -> ph)
3		mpsyl.2	. 2 |- (ps -> ch)
4		mpsyl.3	. 2 |- (ph -> (ch -> th))
5	2, 3, 4	sylc 56	1 |- (ps -> th)

Syntax hints:   -> wi 4

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

This theorem is referenced by:  relcnvtr  4783  relresfld  4790  relcoi1  4792  funco  4883  foimacnv  5087  fvi  5173  isoini2  5401  ovidig  5560  smores2  5850  tfrlem5  5871  cauappcvgprlemm  6617  caucvgprlemm  6639