Theorem mp3an23 1363

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  sbciegf  3060  ac6sfi  7060  dju0en  7396  1qec  7575  ltaddnq  7594  halfnqq  7597  1idsr  7955  pn0sr  7958  ltm1sr  7964  muleqadd  8815  halfcl  9337  rehalfcl  9338  half0  9339  2halves  9340  halfpos2  9341  halfnneg2  9343  halfaddsub  9345  nneoor  9549  zeo  9552  fztp  10274  modqfrac  10559  iexpcyc  10866  bcn2  10986  bcpasc  10988  imre  11362  reim  11363  crim  11369  addcj  11402  imval2  11405  sinf  12215  efi4p  12228  resin4p  12229  recos4p  12230  sinneg  12237  efival  12243  cosadd  12248  sinmul  12255  sinbnd  12263  cosbnd  12264  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  sin01gt0  12273  cos01gt0  12274  sin02gt0  12275  odd2np1lem  12383  odd2np1  12384  pythagtriplem12  12798  pockthi  12881  opprsubrngg  14175  opprdomnbg  14238  isridl  14468  zlmval  14591  zlmlemg  14592  zlmsca  14596  zlmvscag  14597  mopnex  15179  sub1cncf  15276  sub2cncf  15277  sincosq1lem  15499  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  sinq12gt0  15504  abssinper  15520  coskpi  15522  rpcxpsqrt  15596  logsqrt  15597  2lgsoddprmlem2  15785