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

Theorem mpbi 144
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 119 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 5 1  |-  ps
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.74i  179  pm4.71i  386  pm4.71ri  387  pm5.32i  447  biadanii  585  pm3.24  665  olc  683  orc  684  dcnn  816  dn1dc  927  3ori  1261  mptxor  1385  mpgbi  1411  dveeq2  1769  dveeq2or  1770  sbequilem  1792  nfsb  1897  sbco  1917  sbcocom  1919  elsb3  1927  elsb4  1928  hbsbd  1933  dvelimALT  1961  dvelimfv  1962  dvelimor  1969  eqcomi  2119  eqtri  2136  eleqtri  2190  neii  2285  neeqtri  2310  nesymi  2329  necomi  2368  nemtbir  2372  neli  2380  nrex  2499  rexlimi  2517  isseti  2666  eueq1  2827  euxfr2dc  2840  cdeqri  2866  sseqtri  3099  3sstr3i  3105  equncomi  3190  unssi  3219  ssini  3267  unabs  3275  inabs  3276  ddifss  3282  inssddif  3285  rgenm  3433  snid  3524  rabrsndc  3559  rintm  3873  breqtri  3921  bm1.3ii  4017  zfnuleu  4020  zfpow  4067  undifexmid  4085  copsexg  4134  uniop  4145  pwundifss  4175  onunisuci  4322  zfun  4324  op1stb  4367  op1stbg  4368  ordtriexmidlem  4403  ordtriexmid  4405  ordtri2orexmid  4406  2ordpr  4407  ontr2exmid  4408  onsucsssucexmid  4410  onsucelsucexmid  4413  dtruex  4442  ordsoexmid  4445  0elsucexmid  4448  ordtri2or2exmid  4454  dcextest  4463  tfi  4464  relop  4657  dmxpid  4728  rn0  4763  dmresi  4842  issref  4889  cnvcnv  4959  rescnvcnv  4969  cnvcnvres  4970  cnvsn  4989  cocnvcnv2  5018  cores2  5019  co01  5021  relcoi1  5038  cnviinm  5048  fnopab  5215  mpt0  5218  fnmpti  5219  f1cnvcnv  5307  f1ovi  5372  fmpti  5538  fvsnun2  5584  oprabss  5823  2nd0  6009  f1stres  6023  f2ndres  6024  reldmtpos  6116  dftpos4  6126  tpostpos  6127  tpos0  6137  smo0  6161  frecfnom  6264  oasuc  6326  uniixp  6581  ssdomg  6638  xpcomf1o  6685  ssfilem  6735  diffitest  6747  inffiexmid  6766  fiintim  6783  caseinl  6942  caseinr  6943  eninl  6948  eninr  6949  card0  7010  dju1p1e2  7017  dmaddpi  7097  dmmulpi  7098  1lt2pi  7112  1lt2nq  7178  suplocsrlempr  7579  gtso  7807  subf  7928  negne0i  8001  negdii  8010  ltapii  8359  sup3exmid  8672  neg1ap0  8786  halflt1  8888  nn0ssz  9023  3halfnz  9099  zeo  9107  numlt  9157  numltc  9158  le9lt10  9159  decle  9166  uzf  9278  indstr  9337  infrenegsupex  9338  xaddf  9567  ixxf  9621  iooval2  9638  ioof  9694  unirnioo  9696  fzval2  9733  fzf  9734  fz10  9766  fzpreddisj  9791  4fvwrd4  9857  fzof  9861  fldiv4p1lem1div2  10018  sqrt2gt1lt2  10761  infxrnegsupex  10972  fclim  11003  fsumrelem  11180  arisum2  11208  geo2sum2  11224  0.999...  11230  ege2le3  11276  sin0  11335  ef01bndlem  11362  cos2bnd  11366  cos01gt0  11368  sincos2sgn  11371  sin4lt0  11372  egt2lt3  11382  n2dvds1  11505  flodddiv4  11527  gcdf  11557  eucalgf  11632  2prm  11704  dfphi2  11791  znnen  11806  ennnfonelem1  11815  qnnen  11839  ctiunct  11848  structcnvcnv  11870  structfn  11873  eltpsi  12103  unitg  12126  epttop  12154  txuni2  12320  retopon  12590  reldvg  12691  dvrecap  12720  dvef  12730  ex-fl  12739  ex-exp  12741  bdceqi  12843  bdcriota  12883  bdsepnfALT  12889  bdbm1.3ii  12891  bj-d0clsepcl  12925  nninfsellemeqinf  13014
  Copyright terms: Public domain W3C validator