ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp3an23 Unicode version

Theorem mp3an23 1235
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
StepHypRef Expression
1 mp3an23.1 . 2  |-  ps
2 mp3an23.2 . . 3  |-  ch
3 mp3an23.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an3 1232 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan2 409 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  sbciegf  2817  ac6sfi  6383  1qec  6544  ltaddnq  6563  halfnqq  6566  1idsr  6911  pn0sr  6914  muleqadd  7723  halfcl  8208  rehalfcl  8209  half0  8210  2halves  8211  halfpos2  8212  halfnneg2  8214  halfaddsub  8216  nneoor  8399  zeo  8402  fztp  9042  modqfrac  9287  iexpcyc  9523  bcn2  9632  bcpasc  9634  imre  9679  reim  9680  crim  9686  addcj  9719  imval2  9722  odd2np1lem  10183  odd2np1  10184
  Copyright terms: Public domain W3C validator