Theorem mp3an23 1342

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  sbciegf  3037  ac6sfi  7021  dju0en  7357  1qec  7536  ltaddnq  7555  halfnqq  7558  1idsr  7916  pn0sr  7919  ltm1sr  7925  muleqadd  8776  halfcl  9298  rehalfcl  9299  half0  9300  2halves  9301  halfpos2  9302  halfnneg2  9304  halfaddsub  9306  nneoor  9510  zeo  9513  fztp  10235  modqfrac  10519  iexpcyc  10826  bcn2  10946  bcpasc  10948  imre  11277  reim  11278  crim  11284  addcj  11317  imval2  11320  sinf  12130  efi4p  12143  resin4p  12144  recos4p  12145  sinneg  12152  efival  12158  cosadd  12163  sinmul  12170  sinbnd  12178  cosbnd  12179  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  sin01gt0  12188  cos01gt0  12189  sin02gt0  12190  odd2np1lem  12298  odd2np1  12299  pythagtriplem12  12713  pockthi  12796  opprsubrngg  14088  opprdomnbg  14151  isridl  14381  zlmval  14504  zlmlemg  14505  zlmsca  14509  zlmvscag  14510  mopnex  15092  sub1cncf  15189  sub2cncf  15190  sincosq1lem  15412  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  sinq12gt0  15417  abssinper  15433  coskpi  15435  rpcxpsqrt  15509  logsqrt  15510  2lgsoddprmlem2  15698