ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbi GIF 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 𝜑
mpbi.maj (𝜑𝜓)
Assertion
Ref Expression
mpbi 𝜓

Proof of Theorem mpbi
StepHypRef Expression
1 mpbi.min . 2 𝜑
2 mpbi.maj . . 3 (𝜑𝜓)
32biimpi 119 . 2 (𝜑𝜓)
41, 3ax-mp 5 1 𝜓
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  388  pm4.71ri  389  pm5.32i  449  biadanii  587  pm3.24  667  olc  685  orc  686  dcnn  818  dn1dc  929  3ori  1263  mptxor  1387  mpgbi  1413  dveeq2  1771  dveeq2or  1772  sbequilem  1794  nfsb  1899  sbco  1919  sbcocom  1921  elsb3  1929  elsb4  1930  hbsbd  1935  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  eqcomi  2121  eqtri  2138  eleqtri  2192  neii  2287  neeqtri  2312  nesymi  2331  necomi  2370  nemtbir  2374  neli  2382  nrex  2501  rexlimi  2519  isseti  2668  eueq1  2829  euxfr2dc  2842  cdeqri  2868  sseqtri  3101  3sstr3i  3107  equncomi  3192  unssi  3221  ssini  3269  unabs  3277  inabs  3278  ddifss  3284  inssddif  3287  rgenm  3435  snid  3526  rabrsndc  3561  rintm  3875  breqtri  3923  bm1.3ii  4019  zfnuleu  4022  zfpow  4069  undifexmid  4087  copsexg  4136  uniop  4147  pwundifss  4177  onunisuci  4324  zfun  4326  op1stb  4369  op1stbg  4370  ordtriexmidlem  4405  ordtriexmid  4407  ordtri2orexmid  4408  2ordpr  4409  ontr2exmid  4410  onsucsssucexmid  4412  onsucelsucexmid  4415  dtruex  4444  ordsoexmid  4447  0elsucexmid  4450  ordtri2or2exmid  4456  dcextest  4465  tfi  4466  relop  4659  dmxpid  4730  rn0  4765  dmresi  4844  issref  4891  cnvcnv  4961  rescnvcnv  4971  cnvcnvres  4972  cnvsn  4991  cocnvcnv2  5020  cores2  5021  co01  5023  relcoi1  5040  cnviinm  5050  fnopab  5217  mpt0  5220  fnmpti  5221  f1cnvcnv  5309  f1ovi  5374  fmpti  5540  fvsnun2  5586  oprabss  5825  2nd0  6011  f1stres  6025  f2ndres  6026  reldmtpos  6118  dftpos4  6128  tpostpos  6129  tpos0  6139  smo0  6163  frecfnom  6266  oasuc  6328  uniixp  6583  ssdomg  6640  xpcomf1o  6687  ssfilem  6737  diffitest  6749  inffiexmid  6768  fiintim  6785  caseinl  6944  caseinr  6945  eninl  6950  eninr  6951  card0  7012  dju1p1e2  7021  dmaddpi  7101  dmmulpi  7102  1lt2pi  7116  1lt2nq  7182  suplocsrlempr  7583  gtso  7811  subf  7932  negne0i  8005  negdii  8014  ltapii  8364  sup3exmid  8679  neg1ap0  8793  halflt1  8895  nn0ssz  9030  3halfnz  9106  zeo  9114  numlt  9164  numltc  9165  le9lt10  9166  decle  9173  uzf  9285  indstr  9344  infrenegsupex  9345  xaddf  9582  ixxf  9636  iooval2  9653  ioof  9709  unirnioo  9711  fzval2  9748  fzf  9749  fz10  9781  fzpreddisj  9806  4fvwrd4  9872  fzof  9876  fldiv4p1lem1div2  10033  sqrt2gt1lt2  10776  infxrnegsupex  10987  fclim  11018  fsumrelem  11195  arisum2  11223  geo2sum2  11239  0.999...  11245  ege2le3  11291  sin0  11350  ef01bndlem  11377  cos2bnd  11381  cos01gt0  11383  sincos2sgn  11386  sin4lt0  11387  egt2lt3  11398  n2dvds1  11521  flodddiv4  11543  gcdf  11573  eucalgf  11648  2prm  11720  dfphi2  11807  znnen  11822  ennnfonelem1  11831  qnnen  11855  ctiunct  11864  structcnvcnv  11886  structfn  11889  eltpsi  12119  unitg  12142  epttop  12170  txuni2  12336  retopon  12606  dedekindicclemicc  12690  reldvg  12728  dvrecap  12757  dvef  12767  sinhalfpilem  12783  coseq00topi  12827  coseq0negpitopi  12828  ex-fl  12833  ex-exp  12835  bdceqi  12937  bdcriota  12977  bdsepnfALT  12983  bdbm1.3ii  12985  bj-d0clsepcl  13019  nninfsellemeqinf  13108
  Copyright terms: Public domain W3C validator