Theorem mpd3an23 1380

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

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  exp0  10958  bcpasc  11182  bccl  11183  hashfibc  11261  pw2dvds  12922  qnumdencoprm  12949  qeqnumdivden  12950  ballotfilem1ri  13256  grpinvid  13842  qus0  14015  ghmid  14029  mgpvalg  14197  mgpex  14199  opprex  14351  unitgrpid  14398  qusmul2  14838  psrbaglesuppg  14980  dvef  15751  2lgs  16137  uhgrsubgrself  16421