Theorem mp3an23 1307

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 1304	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan2 421	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  sbciegf  2940  ac6sfi  6792  dju0en  7070  1qec  7196  ltaddnq  7215  halfnqq  7218  1idsr  7576  pn0sr  7579  ltm1sr  7585  muleqadd  8429  halfcl  8946  rehalfcl  8947  half0  8948  2halves  8949  halfpos2  8950  halfnneg2  8952  halfaddsub  8954  nneoor  9153  zeo  9156  fztp  9858  modqfrac  10110  iexpcyc  10397  bcn2  10510  bcpasc  10512  imre  10623  reim  10624  crim  10630  addcj  10663  imval2  10666  sinf  11411  efi4p  11424  resin4p  11425  recos4p  11426  sinneg  11433  efival  11439  cosadd  11444  sinmul  11451  sinbnd  11459  cosbnd  11460  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  odd2np1lem  11569  odd2np1  11570  mopnex  12674  sincosq1lem  12906  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  sinq12gt0  12911  abssinper  12927  coskpi  12929