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  3076  ac6sfi  7157  dju0en  7523  1qec  7705  ltaddnq  7724  halfnqq  7727  1idsr  8085  pn0sr  8088  ltm1sr  8094  muleqadd  8944  halfcl  9466  rehalfcl  9467  half0  9468  2halves  9469  halfpos2  9470  halfnneg2  9472  halfaddsub  9474  nneoor  9683  zeo  9686  fztp  10416  modqfrac  10703  iexpcyc  11010  bcn2  11130  bcpasc  11132  imre  11540  reim  11541  crim  11547  addcj  11580  imval2  11583  sinf  12394  efi4p  12407  resin4p  12408  recos4p  12409  sinneg  12416  efival  12422  cosadd  12427  sinmul  12434  sinbnd  12442  cosbnd  12443  ef01bndlem  12446  sin01bnd  12447  cos01bnd  12448  sin01gt0  12452  cos01gt0  12453  sin02gt0  12454  odd2np1lem  12562  odd2np1  12563  pythagtriplem12  12977  pockthi  13060  opprsubrngg  14373  opprdomnbg  14437  isridl  14669  zlmval  14792  zlmlemg  14793  zlmsca  14797  zlmvscag  14798  mopnex  15387  sub1cncf  15484  sub2cncf  15485  sincosq1lem  15707  sincosq2sgn  15709  sincosq3sgn  15710  sincosq4sgn  15711  sinq12gt0  15712  abssinper  15728  coskpi  15730  rpcxpsqrt  15804  logsqrt  15805  2lgsoddprmlem2  15996