Theorem mp3an23 1308

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

Syntax hints:   -> wi 4   /\ w3a 963

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 965

This theorem is referenced by:  sbciegf  2944  ac6sfi  6800  dju0en  7087  1qec  7220  ltaddnq  7239  halfnqq  7242  1idsr  7600  pn0sr  7603  ltm1sr  7609  muleqadd  8453  halfcl  8970  rehalfcl  8971  half0  8972  2halves  8973  halfpos2  8974  halfnneg2  8976  halfaddsub  8978  nneoor  9177  zeo  9180  fztp  9889  modqfrac  10141  iexpcyc  10428  bcn2  10542  bcpasc  10544  imre  10655  reim  10656  crim  10662  addcj  10695  imval2  10698  sinf  11447  efi4p  11460  resin4p  11461  recos4p  11462  sinneg  11469  efival  11475  cosadd  11480  sinmul  11487  sinbnd  11495  cosbnd  11496  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  odd2np1lem  11605  odd2np1  11606  mopnex  12713  sincosq1lem  12954  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  abssinper  12975  coskpi  12977  rpcxpsqrt  13050  logsqrt  13051