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

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 |- ph
2		mpbi.maj	. . 3 |- ( ph <-> ps )
3	2	biimpi 119	. 2 |- ( ph -> ps )
4	1, 3	ax-mp 5	1 |- ps

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  602  pm3.24  682  olc  700  orc  701  dcnn  833  dn1dc  944  3ori  1278  mptxor  1402  mpgbi  1428  dveeq2  1787  dveeq2or  1788  sbequilem  1810  nfsb  1919  sbco  1941  sbcocom  1943  elsb3  1951  elsb4  1952  hbsbd  1957  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  eqcomi  2143  eqtri  2160  eleqtri  2214  neii  2310  neeqtri  2335  nesymi  2354  necomi  2393  nemtbir  2397  neli  2405  nrex  2524  rexlimi  2542  isseti  2694  eueq1  2856  euxfr2dc  2869  cdeqri  2895  sseqtri  3131  3sstr3i  3137  equncomi  3222  unssi  3251  ssini  3299  unabs  3307  inabs  3308  ddifss  3314  inssddif  3317  rgenm  3465  snid  3556  rabrsndc  3591  rintm  3905  breqtri  3953  bm1.3ii  4049  zfnuleu  4052  zfpow  4099  undifexmid  4117  copsexg  4166  uniop  4177  pwundifss  4207  onunisuci  4354  zfun  4356  op1stb  4399  op1stbg  4400  ordtriexmidlem  4435  ordtriexmid  4437  ordtri2orexmid  4438  2ordpr  4439  ontr2exmid  4440  onsucsssucexmid  4442  onsucelsucexmid  4445  dtruex  4474  ordsoexmid  4477  0elsucexmid  4480  ordtri2or2exmid  4486  dcextest  4495  tfi  4496  relop  4689  dmxpid  4760  rn0  4795  dmresi  4874  issref  4921  cnvcnv  4991  rescnvcnv  5001  cnvcnvres  5002  cnvsn  5021  cocnvcnv2  5050  cores2  5051  co01  5053  relcoi1  5070  cnviinm  5080  fnopab  5247  mpt0  5250  fnmpti  5251  f1cnvcnv  5339  f1ovi  5406  fmpti  5572  fvsnun2  5618  oprabss  5857  2nd0  6043  f1stres  6057  f2ndres  6058  reldmtpos  6150  dftpos4  6160  tpostpos  6161  tpos0  6171  smo0  6195  frecfnom  6298  oasuc  6360  uniixp  6615  ssdomg  6672  xpcomf1o  6719  ssfilem  6769  diffitest  6781  inffiexmid  6800  fiintim  6817  caseinl  6976  caseinr  6977  eninl  6982  eninr  6983  card0  7044  dju1p1e2  7053  dmaddpi  7133  dmmulpi  7134  1lt2pi  7148  1lt2nq  7214  suplocsrlempr  7615  gtso  7843  subf  7964  negne0i  8037  negdii  8046  ltapii  8397  sup3exmid  8715  neg1ap0  8829  halflt1  8937  nn0ssz  9072  3halfnz  9148  zeo  9156  numlt  9206  numltc  9207  le9lt10  9208  decle  9215  uzf  9329  indstr  9388  infrenegsupex  9389  xaddf  9627  ixxf  9681  iooval2  9698  ioof  9754  unirnioo  9756  fzval2  9793  fzf  9794  fz10  9826  fzpreddisj  9851  4fvwrd4  9917  fzof  9921  fldiv4p1lem1div2  10078  sqrt2gt1lt2  10821  infxrnegsupex  11032  fclim  11063  fsumrelem  11240  arisum2  11268  geo2sum2  11284  0.999...  11290  ege2le3  11377  sin0  11436  ef01bndlem  11463  cos2bnd  11467  cos01gt0  11469  sincos2sgn  11472  sin4lt0  11473  egt2lt3  11486  n2dvds1  11609  flodddiv4  11631  gcdf  11661  eucalgf  11736  2prm  11808  dfphi2  11896  znnen  11911  ennnfonelem1  11920  qnnen  11944  ctiunct  11953  structcnvcnv  11975  structfn  11978  eltpsi  12208  unitg  12231  epttop  12259  txuni2  12425  retopon  12695  dedekindicclemicc  12779  reldvg  12817  dvrecap  12846  dvef  12856  sinhalfpilem  12872  coseq00topi  12916  coseq0negpitopi  12917  sincos4thpi  12921  sincos6thpi  12923  pigt3  12925  cos02pilt1  12932  ex-fl  12937  ex-exp  12939  bdceqi  13041  bdcriota  13081  bdsepnfALT  13087  bdbm1.3ii  13089  bj-d0clsepcl  13123  nninfsellemeqinf  13212