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  3018  ac6sfi  6956  dju0en  7276  1qec  7450  ltaddnq  7469  halfnqq  7472  1idsr  7830  pn0sr  7833  ltm1sr  7839  muleqadd  8689  halfcl  9211  rehalfcl  9212  half0  9213  2halves  9214  halfpos2  9215  halfnneg2  9217  halfaddsub  9219  nneoor  9422  zeo  9425  fztp  10147  modqfrac  10411  iexpcyc  10718  bcn2  10838  bcpasc  10840  imre  10998  reim  10999  crim  11005  addcj  11038  imval2  11041  sinf  11850  efi4p  11863  resin4p  11864  recos4p  11865  sinneg  11872  efival  11878  cosadd  11883  sinmul  11890  sinbnd  11898  cosbnd  11899  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  odd2np1lem  12016  odd2np1  12017  pythagtriplem12  12416  pockthi  12499  opprsubrngg  13710  opprdomnbg  13773  isridl  14003  zlmval  14126  zlmlemg  14127  zlmsca  14131  zlmvscag  14132  mopnex  14684  sub1cncf  14781  sub2cncf  14782  sincosq1lem  15001  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  abssinper  15022  coskpi  15024  rpcxpsqrt  15097  logsqrt  15098  2lgsoddprmlem2  15263