Theorem mpd3an23 1350

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  exp0  10617  bcpasc  10840  bccl  10841  pw2dvds  12307  qnumdencoprm  12334  qeqnumdivden  12335  grpinvid  13135  qus0  13308  ghmid  13322  mgpvalg  13422  mgpex  13424  opprex  13572  unitgrpid  13617  qusmul2  14028  psrbaglesuppg  14169  dvef  14906  2lgs  15261