Theorem mp3an23 1329

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

Syntax hints:   -> wi 4   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  sbciegf  2992  ac6sfi  6888  dju0en  7203  1qec  7362  ltaddnq  7381  halfnqq  7384  1idsr  7742  pn0sr  7745  ltm1sr  7751  muleqadd  8598  halfcl  9118  rehalfcl  9119  half0  9120  2halves  9121  halfpos2  9122  halfnneg2  9124  halfaddsub  9126  nneoor  9328  zeo  9331  fztp  10048  modqfrac  10307  iexpcyc  10594  bcn2  10712  bcpasc  10714  imre  10828  reim  10829  crim  10835  addcj  10868  imval2  10871  sinf  11680  efi4p  11693  resin4p  11694  recos4p  11695  sinneg  11702  efival  11708  cosadd  11713  sinmul  11720  sinbnd  11728  cosbnd  11729  ef01bndlem  11732  sin01bnd  11733  cos01bnd  11734  sin01gt0  11737  cos01gt0  11738  sin02gt0  11739  odd2np1lem  11844  odd2np1  11845  pythagtriplem12  12242  pockthi  12323  mopnex  13576  sincosq1lem  13817  sincosq2sgn  13819  sincosq3sgn  13820  sincosq4sgn  13821  sinq12gt0  13822  abssinper  13838  coskpi  13840  rpcxpsqrt  13913  logsqrt  13914