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

Theorem mp3an3 1326
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 1205 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
41, 3mpi 15 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
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 980
This theorem is referenced by:  mp3an13  1328  mp3an23  1329  mp3anl3  1333  opelxp  4653  funimaexg  5296  ov  5988  ovmpoa  5999  ovmpo  6004  ovtposg  6254  oaword1  6466  th3q  6634  enrefg  6758  f1imaen  6788  mapxpen  6842  pw1fin  6904  xpfi  6923  djucomen  7209  addnnnq0  7439  mulnnnq0  7440  prarloclemcalc  7492  genpelxp  7501  genpprecll  7504  genppreclu  7505  addsrpr  7735  mulsrpr  7736  gt0srpr  7738  mulid1  7945  ltneg  8409  leneg  8412  suble0  8423  div1  8649  nnaddcl  8928  nnmulcl  8929  nnge1  8931  nnsub  8947  2halves  9137  halfaddsub  9142  addltmul  9144  zleltp1  9297  nnaddm1cl  9303  zextlt  9334  peano5uzti  9350  eluzp1p1  9542  uzaddcl  9575  znq  9613  xrre  9807  xrre2  9808  fzshftral  10094  expn1ap0  10516  expadd  10548  expmul  10551  expubnd  10563  sqmul  10568  bernneq  10626  sqrecapd  10643  faclbnd2  10706  faclbnd6  10708  fihashssdif  10782  shftval3  10820  caucvgre  10974  leabs  11067  ltabs  11080  caubnd2  11110  efexp  11674  efival  11724  cos01gt0  11754  odd2np1  11861  halfleoddlt  11882  omoe  11884  opeo  11885  gcdmultiple  12004  sqgcd  12013  nn0seqcvgd  12024  phiprmpw  12205  eulerthlemth  12215  odzcllem  12225  pcelnn  12303  4sqlem3  12371  ntrin  13291  txuni2  13423  txopn  13432  xblpnfps  13565  xblpnf  13566  bl2in  13570  unirnblps  13589  unirnbl  13590  blpnfctr  13606  sincosq1eq  13927  rpcxpp1  13994  rplogb1  14033
  Copyright terms: Public domain W3C validator