Theorem mpd3an23 1352

Description: An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)

Hypotheses

Ref	Expression
mpd3an23.1	|- ( ph -> ps )
mpd3an23.2	|- ( ph -> ch )
mpd3an23.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mpd3an23	|- ( ph -> th )

Proof of Theorem mpd3an23

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ph -> ph )
2		mpd3an23.1	. 2 |- ( ph -> ps )
3		mpd3an23.2	. 2 |- ( ph -> ch )
4		mpd3an23.3	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
5	1, 2, 3, 4	syl3anc 1250	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  exp0  10688  bcpasc  10911  bccl  10912  pw2dvds  12488  qnumdencoprm  12515  qeqnumdivden  12516  grpinvid  13392  qus0  13571  ghmid  13585  mgpvalg  13685  mgpex  13687  opprex  13835  unitgrpid  13880  qusmul2  14291  psrbaglesuppg  14434  dvef  15199  2lgs  15581