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  11001  bcpasc  11226  bccl  11227  hashfibc  11305  qnumdencoprm  12998  qeqnumdivden  12999  ballotfilem1ri  13336  grpinvid  13924  qus0  14097  ghmid  14111  mgpvalg  14327  mgpex  14330  opprex  14487  unitgrpid  14534  qusmul2  14975  psrbaglesuppg  15166  psrbaglefifi  15172  dvef  15953  2lgs  16428  uhgrsubgrself  16712