Theorem mp3an23 1365

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  sbciegf  3063  ac6sfi  7086  dju0en  7428  1qec  7607  ltaddnq  7626  halfnqq  7629  1idsr  7987  pn0sr  7990  ltm1sr  7996  muleqadd  8847  halfcl  9369  rehalfcl  9370  half0  9371  2halves  9372  halfpos2  9373  halfnneg2  9375  halfaddsub  9377  nneoor  9581  zeo  9584  fztp  10312  modqfrac  10598  iexpcyc  10905  bcn2  11025  bcpasc  11027  imre  11411  reim  11412  crim  11418  addcj  11451  imval2  11454  sinf  12264  efi4p  12277  resin4p  12278  recos4p  12279  sinneg  12286  efival  12292  cosadd  12297  sinmul  12304  sinbnd  12312  cosbnd  12313  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  odd2np1lem  12432  odd2np1  12433  pythagtriplem12  12847  pockthi  12930  opprsubrngg  14224  opprdomnbg  14287  isridl  14517  zlmval  14640  zlmlemg  14641  zlmsca  14645  zlmvscag  14646  mopnex  15228  sub1cncf  15325  sub2cncf  15326  sincosq1lem  15548  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  abssinper  15569  coskpi  15571  rpcxpsqrt  15645  logsqrt  15646  2lgsoddprmlem2  15834