Theorem mp3an23 1340

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  sbciegf  3017  ac6sfi  6954  dju0en  7274  1qec  7448  ltaddnq  7467  halfnqq  7470  1idsr  7828  pn0sr  7831  ltm1sr  7837  muleqadd  8687  halfcl  9208  rehalfcl  9209  half0  9210  2halves  9211  halfpos2  9212  halfnneg2  9214  halfaddsub  9216  nneoor  9419  zeo  9422  fztp  10144  modqfrac  10408  iexpcyc  10715  bcn2  10835  bcpasc  10837  imre  10995  reim  10996  crim  11002  addcj  11035  imval2  11038  sinf  11847  efi4p  11860  resin4p  11861  recos4p  11862  sinneg  11869  efival  11875  cosadd  11880  sinmul  11887  sinbnd  11895  cosbnd  11896  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  odd2np1lem  12013  odd2np1  12014  pythagtriplem12  12413  pockthi  12496  opprsubrngg  13707  opprdomnbg  13770  isridl  14000  zlmval  14115  zlmlemg  14116  zlmsca  14120  zlmvscag  14121  mopnex  14673  sub1cncf  14756  sub2cncf  14757  sincosq1lem  14960  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  abssinper  14981  coskpi  14983  rpcxpsqrt  15056  logsqrt  15057  2lgsoddprmlem2  15194