Theorem mp3an23 1340

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  sbciegf  3021  ac6sfi  6959  dju0en  7281  1qec  7455  ltaddnq  7474  halfnqq  7477  1idsr  7835  pn0sr  7838  ltm1sr  7844  muleqadd  8695  halfcl  9217  rehalfcl  9218  half0  9219  2halves  9220  halfpos2  9221  halfnneg2  9223  halfaddsub  9225  nneoor  9428  zeo  9431  fztp  10153  modqfrac  10429  iexpcyc  10736  bcn2  10856  bcpasc  10858  imre  11016  reim  11017  crim  11023  addcj  11056  imval2  11059  sinf  11869  efi4p  11882  resin4p  11883  recos4p  11884  sinneg  11891  efival  11897  cosadd  11902  sinmul  11909  sinbnd  11917  cosbnd  11918  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  odd2np1lem  12037  odd2np1  12038  pythagtriplem12  12444  pockthi  12527  opprsubrngg  13767  opprdomnbg  13830  isridl  14060  zlmval  14183  zlmlemg  14184  zlmsca  14188  zlmvscag  14189  mopnex  14741  sub1cncf  14838  sub2cncf  14839  sincosq1lem  15061  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  abssinper  15082  coskpi  15084  rpcxpsqrt  15158  logsqrt  15159  2lgsoddprmlem2  15347