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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  exp0  10980  bcpasc  11204  bccl  11205  hashfibc  11283  pw2dvds  12944  qnumdencoprm  12971  qeqnumdivden  12972  ballotfilem1ri  13278  grpinvid  13865  qus0  14038  ghmid  14052  mgpvalg  14220  mgpex  14223  opprex  14378  unitgrpid  14425  qusmul2  14866  psrbaglesuppg  15057  dvef  15828  2lgs  16223  uhgrsubgrself  16507