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

Theorem mp3an3 1287
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 1166 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
41, 3mpi 15 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  mp3an13  1289  mp3an23  1290  mp3anl3  1294  opelxp  4537  funimaexg  5175  ov  5856  ovmpoa  5867  ovmpo  5872  ovtposg  6122  oaword1  6333  th3q  6500  enrefg  6624  f1imaen  6654  mapxpen  6708  xpfi  6784  djucomen  7036  addnnnq0  7221  mulnnnq0  7222  prarloclemcalc  7274  genpelxp  7283  genpprecll  7286  genppreclu  7287  addsrpr  7517  mulsrpr  7518  gt0srpr  7520  mulid1  7727  ltneg  8188  leneg  8191  suble0  8202  div1  8423  nnaddcl  8697  nnmulcl  8698  nnge1  8700  nnsub  8716  2halves  8900  halfaddsub  8905  addltmul  8907  zleltp1  9060  nnaddm1cl  9066  zextlt  9094  peano5uzti  9110  eluzp1p1  9300  uzaddcl  9330  znq  9365  xrre  9543  xrre2  9544  fzshftral  9828  expn1ap0  10243  expadd  10275  expmul  10278  expubnd  10290  sqmul  10295  bernneq  10352  sqrecapd  10368  faclbnd2  10428  faclbnd6  10430  fihashssdif  10504  shftval3  10539  caucvgre  10693  leabs  10786  ltabs  10799  caubnd2  10829  efexp  11287  efival  11338  cos01gt0  11368  odd2np1  11466  halfleoddlt  11487  omoe  11489  opeo  11490  gcdmultiple  11604  sqgcd  11613  nn0seqcvgd  11618  phiprmpw  11793  ntrin  12188  txuni2  12320  txopn  12329  xblpnfps  12462  xblpnf  12463  bl2in  12467  unirnblps  12486  unirnbl  12487  blpnfctr  12503
  Copyright terms: Public domain W3C validator