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 )

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  sbciegf  3083  ac6sfi  7192  dju0en  7560  1qec  7745  ltaddnq  7764  halfnqq  7767  1idsr  8125  pn0sr  8128  ltm1sr  8134  muleqadd  8988  halfcl  9510  rehalfcl  9511  half0  9512  2halves  9513  halfpos2  9514  halfnneg2  9516  halfaddsub  9518  nneoor  9727  zeo  9730  fztp  10463  modqfrac  10752  iexpcyc  11059  bcn2  11180  bcpasc  11182  imre  11594  reim  11595  crim  11601  addcj  11634  imval2  11637  sinf  12449  efi4p  12462  resin4p  12463  recos4p  12464  sinneg  12471  efival  12477  cosadd  12482  sinmul  12489  sinbnd  12497  cosbnd  12498  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  odd2np1lem  12617  odd2np1  12618  pythagtriplem12  13032  pockthi  13115  opprsubrngg  14492  opprdomnbg  14556  isridl  14813  zlmval  14934  zlmlemg  14935  zlmsca  14939  zlmvscag  14940  mopnex  15529  sub1cncf  15626  sub2cncf  15627  sincosq1lem  15849  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  abssinper  15870  coskpi  15872  rpcxpsqrt  15947  logsqrt  15948  2lgsoddprmlem2  16139