Theorem mpd3an23 1376

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  exp0  10851  bcpasc  11074  bccl  11075  pw2dvds  12801  qnumdencoprm  12828  qeqnumdivden  12829  grpinvid  13706  qus0  13885  ghmid  13899  mgpvalg  14000  mgpex  14002  opprex  14150  unitgrpid  14196  qusmul2  14608  psrbaglesuppg  14751  dvef  15521  2lgs  15906  uhgrsubgrself  16190