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  7068  dju0en  7407  1qec  7586  ltaddnq  7605  halfnqq  7608  1idsr  7966  pn0sr  7969  ltm1sr  7975  muleqadd  8826  halfcl  9348  rehalfcl  9349  half0  9350  2halves  9351  halfpos2  9352  halfnneg2  9354  halfaddsub  9356  nneoor  9560  zeo  9563  fztp  10286  modqfrac  10571  iexpcyc  10878  bcn2  10998  bcpasc  11000  imre  11378  reim  11379  crim  11385  addcj  11418  imval2  11421  sinf  12231  efi4p  12244  resin4p  12245  recos4p  12246  sinneg  12253  efival  12259  cosadd  12264  sinmul  12271  sinbnd  12279  cosbnd  12280  ef01bndlem  12283  sin01bnd  12284  cos01bnd  12285  sin01gt0  12289  cos01gt0  12290  sin02gt0  12291  odd2np1lem  12399  odd2np1  12400  pythagtriplem12  12814  pockthi  12897  opprsubrngg  14191  opprdomnbg  14254  isridl  14484  zlmval  14607  zlmlemg  14608  zlmsca  14612  zlmvscag  14613  mopnex  15195  sub1cncf  15292  sub2cncf  15293  sincosq1lem  15515  sincosq2sgn  15517  sincosq3sgn  15518  sincosq4sgn  15519  sinq12gt0  15520  abssinper  15536  coskpi  15538  rpcxpsqrt  15612  logsqrt  15613  2lgsoddprmlem2  15801