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  662  olc  667  orc  668  dn1dc  906  3ori  1236  mptxor  1360  mpgbi  1386  dveeq2  1743  dveeq2or  1744  sbequilem  1766  nfsb  1870  sbco  1890  sbcocom  1892  elsb3  1900  elsb4  1901  hbsbd  1906  dvelimALT  1934  dvelimfv  1935  dvelimor  1942  eqcomi  2092  eqtri  2108  eleqtri  2162  neii  2257  neeqtri  2282  nesymi  2301  necomi  2340  nemtbir  2344  neli  2352  nrex  2465  rexlimi  2482  isseti  2627  eueq1  2785  euxfr2dc  2798  cdeqri  2824  sseqtri  3056  3sstr3i  3062  equncomi  3144  unssi  3173  ssini  3221  unabs  3228  inabs  3229  ddifss  3235  inssddif  3238  rgenm  3380  snid  3470  rabrsndc  3505  rintm  3813  breqtri  3860  bm1.3ii  3952  zfnuleu  3955  zfpow  4002  undifexmid  4019  copsexg  4062  uniop  4073  pwundifss  4103  onunisuci  4250  zfun  4252  op1stb  4290  op1stbg  4291  ordtriexmidlem  4326  ordtriexmid  4328  ordtri2orexmid  4329  2ordpr  4330  ontr2exmid  4331  onsucsssucexmid  4333  onsucelsucexmid  4336  dtruex  4365  ordsoexmid  4368  0elsucexmid  4371  ordtri2or2exmid  4377  dcextest  4386  tfi  4387  relop  4574  rn0  4677  dmresi  4754  issref  4801  cnvcnv  4870  rescnvcnv  4880  cnvcnvres  4881  cnvsn  4900  cocnvcnv2  4929  cores2  4930  co01  4932  relcoi1  4949  cnviinm  4959  fnopab  5124  mpt0  5127  fnmpti  5128  f1cnvcnv  5211  f1ovi  5276  fmpti  5435  fvsnun2  5479  oprabss  5716  2nd0  5898  f1stres  5912  f2ndres  5913  reldmtpos  6000  dftpos4  6010  tpostpos  6011  tpos0  6021  smo0  6045  frecfnom  6148  oasuc  6207  ssdomg  6475  xpcomf1o  6521  ssfilem  6571  diffitest  6583  inffiexmid  6602  card0  6795  dju1p1e2  6802  dmaddpi  6863  dmmulpi  6864  1lt2pi  6878  1lt2nq  6944  gtso  7543  subf  7663  negne0i  7736  negdii  7745  ltapii  8086  neg1ap0  8502  halflt1  8603  nn0ssz  8738  3halfnz  8813  zeo  8821  numlt  8870  numltc  8871  le9lt10  8872  decle  8879  uzf  8991  indstr  9050  infrenegsupex  9051  ixxf  9285  iooval2  9302  ioof  9358  unirnioo  9360  fzval2  9396  fzf  9397  fz10  9429  fzpreddisj  9452  4fvwrd4  9516  fzof  9520  fldiv4p1lem1div2  9677  sqrt2gt1lt2  10447  fclim  10646  fsumrelem  10828  arisum2  10854  geo2sum2  10870  0.999...  10876  n2dvds1  11005  flodddiv4  11027  gcdf  11057  eucalgf  11130  2prm  11202  dfphi2  11289  znnen  11304  ex-fl  11309  ex-exp  11311  bdceqi  11391  bdcriota  11431  bdsepnfALT  11437  bdbm1.3ii  11439  bj-d0clsepcl  11477  nninfsellemeqinf  11565
  Copyright terms: Public domain W3C validator