Theorem mp3an23 1366

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  sbciegf  3077  ac6sfi  7169  dju0en  7535  1qec  7720  ltaddnq  7739  halfnqq  7742  1idsr  8100  pn0sr  8103  ltm1sr  8109  muleqadd  8963  halfcl  9485  rehalfcl  9486  half0  9487  2halves  9488  halfpos2  9489  halfnneg2  9491  halfaddsub  9493  nneoor  9702  zeo  9705  fztp  10438  modqfrac  10727  iexpcyc  11034  bcn2  11155  bcpasc  11157  imre  11565  reim  11566  crim  11572  addcj  11605  imval2  11608  sinf  12420  efi4p  12433  resin4p  12434  recos4p  12435  sinneg  12442  efival  12448  cosadd  12453  sinmul  12460  sinbnd  12468  cosbnd  12469  ef01bndlem  12472  sin01bnd  12473  cos01bnd  12474  sin01gt0  12478  cos01gt0  12479  sin02gt0  12480  odd2np1lem  12588  odd2np1  12589  pythagtriplem12  13003  pockthi  13086  opprsubrngg  14462  opprdomnbg  14526  isridl  14783  zlmval  14906  zlmlemg  14907  zlmsca  14911  zlmvscag  14912  mopnex  15501  sub1cncf  15598  sub2cncf  15599  sincosq1lem  15821  sincosq2sgn  15823  sincosq3sgn  15824  sincosq4sgn  15825  sinq12gt0  15826  abssinper  15842  coskpi  15844  rpcxpsqrt  15918  logsqrt  15919  2lgsoddprmlem2  16110