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  3021  ac6sfi  6968  dju0en  7297  1qec  7472  ltaddnq  7491  halfnqq  7494  1idsr  7852  pn0sr  7855  ltm1sr  7861  muleqadd  8712  halfcl  9234  rehalfcl  9235  half0  9236  2halves  9237  halfpos2  9238  halfnneg2  9240  halfaddsub  9242  nneoor  9445  zeo  9448  fztp  10170  modqfrac  10446  iexpcyc  10753  bcn2  10873  bcpasc  10875  imre  11033  reim  11034  crim  11040  addcj  11073  imval2  11076  sinf  11886  efi4p  11899  resin4p  11900  recos4p  11901  sinneg  11908  efival  11914  cosadd  11919  sinmul  11926  sinbnd  11934  cosbnd  11935  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  odd2np1lem  12054  odd2np1  12055  pythagtriplem12  12469  pockthi  12552  opprsubrngg  13843  opprdomnbg  13906  isridl  14136  zlmval  14259  zlmlemg  14260  zlmsca  14264  zlmvscag  14265  mopnex  14825  sub1cncf  14922  sub2cncf  14923  sincosq1lem  15145  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  abssinper  15166  coskpi  15168  rpcxpsqrt  15242  logsqrt  15243  2lgsoddprmlem2  15431