Theorem mp3an23 1329

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  sbciegf  2996  ac6sfi  6900  dju0en  7215  1qec  7389  ltaddnq  7408  halfnqq  7411  1idsr  7769  pn0sr  7772  ltm1sr  7778  muleqadd  8627  halfcl  9147  rehalfcl  9148  half0  9149  2halves  9150  halfpos2  9151  halfnneg2  9153  halfaddsub  9155  nneoor  9357  zeo  9360  fztp  10080  modqfrac  10339  iexpcyc  10627  bcn2  10746  bcpasc  10748  imre  10862  reim  10863  crim  10869  addcj  10902  imval2  10905  sinf  11714  efi4p  11727  resin4p  11728  recos4p  11729  sinneg  11736  efival  11742  cosadd  11747  sinmul  11754  sinbnd  11762  cosbnd  11763  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  cos01gt0  11772  sin02gt0  11773  odd2np1lem  11879  odd2np1  11880  pythagtriplem12  12277  pockthi  12358  mopnex  14090  sincosq1lem  14331  sincosq2sgn  14333  sincosq3sgn  14334  sincosq4sgn  14335  sinq12gt0  14336  abssinper  14352  coskpi  14354  rpcxpsqrt  14427  logsqrt  14428  2lgsoddprmlem2  14539