Theorem mp3an23 1370

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  sbciegf  3083  ac6sfi  7202  dju0en  7570  1qec  7755  ltaddnq  7774  halfnqq  7777  1idsr  8135  pn0sr  8138  ltm1sr  8144  muleqadd  9000  halfcl  9535  rehalfcl  9536  half0  9537  2halves  9538  halfpos2  9539  halfnneg2  9541  halfaddsub  9543  nneoor  9752  zeo  9755  fztp  10495  modqfrac  10787  iexpcyc  11094  bcn2  11216  bcpasc  11218  imre  11630  reim  11631  crim  11637  addcj  11670  imval2  11673  sinf  12487  efi4p  12500  resin4p  12501  recos4p  12502  sinneg  12509  efival  12515  cosadd  12520  sinmul  12527  sinbnd  12535  cosbnd  12536  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  odd2np1lem  12655  odd2np1  12656  pythagtriplem12  13074  pockthi  13157  prmlem0  13240  opprsubrngg  14568  opprdomnbg  14632  isridl  14890  zlmval  15011  zlmlemg  15012  zlmsca  15016  zlmvscag  15017  mopnex  15655  sub1cncf  15752  sub2cncf  15753  sincosq1lem  15976  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  abssinper  15997  coskpi  15999  rpcxpsqrt  16077  logsqrt  16078  ppiqub  16194  bcmax  16203  bcp1ctr  16204  bposlem2  16210  2lgsoddprmlem2  16323