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

Theorem mpbi 143
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbi.min  |-  ph
mpbi.maj  |-  ( ph  <->  ps )
Assertion
Ref Expression
mpbi  |-  ps

Proof of Theorem mpbi
StepHypRef Expression
1 mpbi.min . 2  |-  ph
2 mpbi.maj . . 3  |-  ( ph  <->  ps )
32biimpi 118 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 7 1  |-  ps
Colors of variables: wff set class
Syntax hints:    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.74i  178  pm4.71i  383  pm4.71ri  384  pm5.32i  442  pm3.24  660  olc  665  orc  666  dn1dc  902  3ori  1232  mptxor  1356  mpgbi  1382  dveeq2  1737  dveeq2or  1738  sbequilem  1760  nfsb  1864  sbco  1884  sbcocom  1886  elsb3  1894  elsb4  1895  hbsbd  1900  dvelimALT  1928  dvelimfv  1929  dvelimor  1936  eqcomi  2086  eqtri  2102  eleqtri  2154  neii  2248  neeqtri  2273  nesymi  2292  necomi  2331  nemtbir  2335  neli  2342  nrex  2454  rexlimi  2471  isseti  2608  eueq1  2765  euxfr2dc  2778  cdeqri  2802  sseqtri  3032  3sstr3i  3038  equncomi  3119  unssi  3148  ssini  3196  unabs  3203  inabs  3204  ddifss  3209  inssddif  3212  rgenm  3351  snid  3433  rabrsndc  3468  rintm  3773  breqtri  3816  bm1.3ii  3907  zfnuleu  3910  zfpow  3957  copsexg  4007  uniop  4018  pwundifss  4048  onunisuci  4195  zfun  4197  op1stb  4235  op1stbg  4236  ordtriexmidlem  4271  ordtriexmid  4273  ordtri2orexmid  4274  2ordpr  4275  ontr2exmid  4276  onsucsssucexmid  4278  onsucelsucexmid  4281  dtruex  4310  ordsoexmid  4313  0elsucexmid  4316  ordtri2or2exmid  4322  tfi  4331  relop  4514  rn0  4616  dmresi  4691  issref  4737  cnvcnv  4803  rescnvcnv  4813  cnvcnvres  4814  cnvsn  4833  cocnvcnv2  4862  cores2  4863  co01  4865  relcoi1  4879  cnviinm  4889  fnopab  5054  mpt0  5057  fnmpti  5058  f1cnvcnv  5131  f1ovi  5196  fmpti  5353  fvsnun2  5393  oprabss  5621  2nd0  5803  f1stres  5817  f2ndres  5818  reldmtpos  5902  dftpos4  5912  tpostpos  5913  tpos0  5923  smo0  5947  frecfnom  6050  oasuc  6108  ssdomg  6325  xpcomf1o  6369  ssfilem  6410  diffitest  6421  card0  6516  dmaddpi  6577  dmmulpi  6578  1lt2pi  6592  1lt2nq  6658  gtso  7257  subf  7377  negne0i  7450  negdii  7459  ltapii  7800  neg1ap0  8215  halflt1  8315  nn0ssz  8450  3halfnz  8525  zeo  8533  numlt  8582  numltc  8583  le9lt10  8584  decle  8591  uzf  8703  indstr  8762  infrenegsupex  8763  ixxf  8997  iooval2  9014  ioof  9070  unirnioo  9072  fzval2  9108  fzf  9109  fz10  9141  fzpreddisj  9164  4fvwrd4  9227  fzof  9231  fldiv4p1lem1div2  9387  sqrt2gt1lt2  10073  fclim  10271  n2dvds1  10456  flodddiv4  10478  gcdf  10508  eucalgf  10581  2prm  10653  znnen  10709  ex-fl  10714  bdceqi  10792  bdcriota  10832  bdsepnfALT  10838  bdbm1.3ii  10840  bj-d0clsepcl  10878
  Copyright terms: Public domain W3C validator