Theorem mpd3an23 1375

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 1273	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  exp0  10806  bcpasc  11029  bccl  11030  pw2dvds  12756  qnumdencoprm  12783  qeqnumdivden  12784  grpinvid  13661  qus0  13840  ghmid  13854  mgpvalg  13955  mgpex  13957  opprex  14105  unitgrpid  14151  qusmul2  14562  psrbaglesuppg  14705  dvef  15470  2lgs  15852  uhgrsubgrself  16136