Theorem mp3an23 1265

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	|- ps
mp3an23.2	|- ch
mp3an23.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an23	|- ( ph -> th )

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 |- ps
2		mp3an23.2	. . 3 |- ch
3		mp3an23.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an3 1262	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan2 416	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 924

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  sbciegf  2868  ac6sfi  6594  1qec  6926  ltaddnq  6945  halfnqq  6948  1idsr  7293  pn0sr  7296  muleqadd  8111  halfcl  8612  rehalfcl  8613  half0  8614  2halves  8615  halfpos2  8616  halfnneg2  8618  halfaddsub  8620  nneoor  8818  zeo  8821  fztp  9459  modqfrac  9709  iexpcyc  10024  bcn2  10137  bcpasc  10139  imre  10250  reim  10251  crim  10257  addcj  10290  imval2  10293  odd2np1lem  10965  odd2np1  10966