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  3009  ac6sfi  6930  dju0en  7248  1qec  7422  ltaddnq  7441  halfnqq  7444  1idsr  7802  pn0sr  7805  ltm1sr  7811  muleqadd  8660  halfcl  9180  rehalfcl  9181  half0  9182  2halves  9183  halfpos2  9184  halfnneg2  9186  halfaddsub  9188  nneoor  9390  zeo  9393  fztp  10114  modqfrac  10374  iexpcyc  10665  bcn2  10785  bcpasc  10787  imre  10901  reim  10902  crim  10908  addcj  10941  imval2  10944  sinf  11753  efi4p  11766  resin4p  11767  recos4p  11768  sinneg  11775  efival  11781  cosadd  11786  sinmul  11793  sinbnd  11801  cosbnd  11802  ef01bndlem  11805  sin01bnd  11806  cos01bnd  11807  sin01gt0  11810  cos01gt0  11811  sin02gt0  11812  odd2np1lem  11918  odd2np1  11919  pythagtriplem12  12318  pockthi  12401  opprsubrngg  13583  isridl  13844  zlmval  13948  zlmlemg  13949  zlmsca  13953  zlmvscag  13954  mopnex  14490  sincosq1lem  14731  sincosq2sgn  14733  sincosq3sgn  14734  sincosq4sgn  14735  sinq12gt0  14736  abssinper  14752  coskpi  14754  rpcxpsqrt  14827  logsqrt  14828  2lgsoddprmlem2  14940