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

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

Proof of Theorem mp3an3
StepHypRef Expression
1 mp3an3.1 . 2  |-  ch
2 mp3an3.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expia 1117 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
41, 3mpi 15 1  |-  ( (
ph  /\  ps )  ->  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:  mp3an13  1234  mp3an23  1235  mp3anl3  1239  opelxp  4402  funimaexg  5011  ov  5648  ovmpt2a  5659  ovmpt2  5664  ovtposg  5905  oaword1  6081  th3q  6242  enrefg  6275  f1imaen  6305  addnnnq0  6605  mulnnnq0  6606  prarloclemcalc  6658  genpelxp  6667  genpprecll  6670  genppreclu  6671  addsrpr  6888  mulsrpr  6889  gt0srpr  6891  mulid1  7082  ltneg  7531  leneg  7534  suble0  7545  div1  7754  nnaddcl  8010  nnmulcl  8011  nnge1  8013  nnsub  8028  2halves  8211  halfaddsub  8216  addltmul  8218  zleltp1  8357  nnaddm1cl  8363  zextlt  8390  peano5uzti  8405  eluzp1p1  8594  uzaddcl  8625  znq  8656  xrre  8834  xrre2  8835  fzshftral  9072  expn1ap0  9430  expadd  9462  expmul  9465  expubnd  9477  sqmul  9482  bernneq  9537  sqrecapd  9553  faclbnd2  9610  faclbnd6  9612  shftval3  9656  caucvgre  9808  leabs  9901  ltabs  9914  caubnd2  9944  odd2np1  10184  halfleoddlt  10206  omoe  10208  opeo  10209  nn0seqcvgd  10263
  Copyright terms: Public domain W3C validator