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

Theorem mp3an1 1230
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an1.1  |-  ph
mp3an1.2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an1  |-  ( ( ps  /\  ch )  ->  th )

Proof of Theorem mp3an1
StepHypRef Expression
1 mp3an1.1 . 2  |-  ph
2 mp3an1.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expb 1116 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
41, 3mpan 408 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ 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:  mp3an12  1233  mp3an1i  1236  mp3anl1  1237  mp3an  1243  mp3an2i  1248  mp3an3an  1249  tfrlem9  5966  rdgexgg  5996  oaexg  6059  omexg  6062  oeiexg  6064  oav2  6074  nnaordex  6131  mulidnq  6545  1idpru  6747  addgt0sr  6918  muladd11  7207  cnegex  7252  negsubdi  7330  renegcl  7335  mulneg1  7464  ltaddpos  7521  addge01  7541  rimul  7650  recclap  7732  recidap  7739  recidap2  7740  recdivap2  7776  divdiv23apzi  7816  ltmul12a  7901  lemul12a  7903  mulgt1  7904  ltmulgt11  7905  gt0div  7911  ge0div  7912  ltdiv23i  7967  8th4div3  8201  gtndiv  8393  nn0ind  8411  fnn0ind  8413  xrre2  8835  ioorebasg  8945  fzen  9009  elfz0ubfz0  9084  frec2uzzd  9350  frec2uzsucd  9351  expubnd  9477  le2sq2  9495  bernneq  9537  expnbnd  9540  faclbnd6  9612  bccl  9635  shftfval  9650  mulreap  9692  caucvgrelemrec  9806  odd2np1  10184  opoe  10207  omoe  10208  opeo  10209  omeo  10210  algcvgblem  10271  ialgcvga  10273
  Copyright terms: Public domain W3C validator