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  7208  dju0en  7576  1qec  7761  ltaddnq  7780  halfnqq  7783  1idsr  8141  pn0sr  8144  ltm1sr  8150  muleqadd  9006  halfcl  9542  rehalfcl  9543  half0  9544  2halves  9545  halfpos2  9546  halfnneg2  9548  halfaddsub  9550  nneoor  9758  zeo  9761  fztp  10501  modqfrac  10794  iexpcyc  11101  bcn2  11223  bcpasc  11225  imre  11637  reim  11638  crim  11644  addcj  11677  imval2  11680  sinf  12495  efi4p  12508  resin4p  12509  recos4p  12510  sinneg  12517  efival  12523  cosadd  12528  sinmul  12535  sinbnd  12543  cosbnd  12544  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  odd2np1lem  12663  odd2np1  12664  pythagtriplem12  13082  pockthi  13165  prmlem0  13248  opprsubrngg  14627  opprdomnbg  14691  isridl  14949  zlmval  15070  zlmlemg  15071  zlmsca  15075  zlmvscag  15076  mopnex  15748  sub1cncf  15845  sub2cncf  15846  sincosq1lem  16069  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  abssinper  16090  coskpi  16092  sineq0re  16093  rpcxpsqrt  16174  logsqrt  16175  ppiqub  16310  chtublem  16312  chtqub  16313  bcmax  16322  bcp1ctr  16323  bposlem2  16329  bposlem6  16333  bposlem9  16336  2lgsoddprmlem2  16447