Theorem mp3an23 1324

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

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  sbciegf  2986  ac6sfi  6876  dju0en  7191  1qec  7350  ltaddnq  7369  halfnqq  7372  1idsr  7730  pn0sr  7733  ltm1sr  7739  muleqadd  8586  halfcl  9104  rehalfcl  9105  half0  9106  2halves  9107  halfpos2  9108  halfnneg2  9110  halfaddsub  9112  nneoor  9314  zeo  9317  fztp  10034  modqfrac  10293  iexpcyc  10580  bcn2  10698  bcpasc  10700  imre  10815  reim  10816  crim  10822  addcj  10855  imval2  10858  sinf  11667  efi4p  11680  resin4p  11681  recos4p  11682  sinneg  11689  efival  11695  cosadd  11700  sinmul  11707  sinbnd  11715  cosbnd  11716  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  odd2np1lem  11831  odd2np1  11832  pythagtriplem12  12229  pockthi  12310  mopnex  13299  sincosq1lem  13540  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  abssinper  13561  coskpi  13563  rpcxpsqrt  13636  logsqrt  13637