Theorem mp3an23 1319

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

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  sbciegf  2981  ac6sfi  6860  dju0en  7166  1qec  7325  ltaddnq  7344  halfnqq  7347  1idsr  7705  pn0sr  7708  ltm1sr  7714  muleqadd  8561  halfcl  9079  rehalfcl  9080  half0  9081  2halves  9082  halfpos2  9083  halfnneg2  9085  halfaddsub  9087  nneoor  9289  zeo  9292  fztp  10009  modqfrac  10268  iexpcyc  10555  bcn2  10673  bcpasc  10675  imre  10789  reim  10790  crim  10796  addcj  10829  imval2  10832  sinf  11641  efi4p  11654  resin4p  11655  recos4p  11656  sinneg  11663  efival  11669  cosadd  11674  sinmul  11681  sinbnd  11689  cosbnd  11690  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  sin01gt0  11698  cos01gt0  11699  sin02gt0  11700  odd2np1lem  11805  odd2np1  11806  pythagtriplem12  12203  pockthi  12284  mopnex  13105  sincosq1lem  13346  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  abssinper  13367  coskpi  13369  rpcxpsqrt  13442  logsqrt  13443