Theorem mpbi 145

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 120	. 2 |- ( ph -> ps )
4	1, 3	ax-mp 5	1 |- ps

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74i  180  pm4.71i  391  pm4.71ri  392  pm5.32i  454  biadanii  613  pm3.24  693  olc  711  orc  712  dcnn  848  dn1dc  960  3ori  1300  mptxor  1424  mpgbi  1452  dveeq2  1815  dveeq2or  1816  sbequilem  1838  nfsb  1946  sbco  1968  sbcocom  1970  hbsbd  1982  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  hbe1a  2023  elsb1  2155  elsb2  2156  eqcomi  2181  eqtri  2198  eleqtri  2252  neii  2349  neeqtri  2374  nesymi  2393  necomi  2432  nemtbir  2436  neli  2444  nrex  2569  rexlimi  2587  isseti  2745  eueq1  2909  euxfr2dc  2922  cdeqri  2948  sseqtri  3189  3sstr3i  3195  equncomi  3281  unssi  3310  ssini  3358  unabs  3366  inabs  3367  ddifss  3373  inssddif  3376  rgenm  3525  snid  3623  rabrsndc  3660  rintm  3979  breqtri  4028  bm1.3ii  4124  zfnuleu  4127  zfpow  4175  undifexmid  4193  copsexg  4244  uniop  4255  pwundifss  4285  onunisuci  4432  zfun  4434  op1stb  4478  op1stbg  4479  ordtriexmidlem  4518  ordtriexmid  4520  ordtri2orexmid  4522  2ordpr  4523  ontr2exmid  4524  onsucsssucexmid  4526  onsucelsucexmid  4529  dtruex  4558  ordsoexmid  4561  0elsucexmid  4564  ordtri2or2exmid  4570  dcextest  4580  tfi  4581  relop  4777  dmxpid  4848  rn0  4883  dmresi  4962  issref  5011  cnvcnv  5081  rescnvcnv  5091  cnvcnvres  5092  cnvsn  5111  cocnvcnv2  5140  cores2  5141  co01  5143  relcoi1  5160  cnviinm  5170  fnopab  5340  mpt0  5343  fnmpti  5344  f1cnvcnv  5432  f1ovi  5500  fmpti  5668  fvsnun2  5714  oprabss  5960  2nd0  6145  f1stres  6159  f2ndres  6160  reldmtpos  6253  dftpos4  6263  tpostpos  6264  tpos0  6274  smo0  6298  frecfnom  6401  oasuc  6464  uniixp  6720  ssdomg  6777  xpcomf1o  6824  ssfilem  6874  diffitest  6886  inffiexmid  6905  fiintim  6927  caseinl  7089  caseinr  7090  eninl  7095  eninr  7096  card0  7186  dju1p1e2  7195  pw1on  7224  dmaddpi  7323  dmmulpi  7324  1lt2pi  7338  1lt2nq  7404  suplocsrlempr  7805  gtso  8035  subf  8158  negne0i  8231  negdii  8240  ltapii  8591  sup3exmid  8913  neg1ap0  9027  halflt1  9135  nn0ssz  9270  3halfnz  9349  zeo  9357  numlt  9407  numltc  9408  le9lt10  9409  decle  9416  uzf  9530  indstr  9592  infrenegsupex  9593  xaddf  9843  ixxf  9897  iooval2  9914  ioof  9970  unirnioo  9972  fzval2  10010  fzf  10011  fz10  10045  fzpreddisj  10070  4fvwrd4  10139  fzof  10143  fldiv4p1lem1div2  10304  sqrt2gt1lt2  11057  infxrnegsupex  11270  fclim  11301  fsumrelem  11478  arisum2  11506  geo2sum2  11522  0.999...  11528  ege2le3  11678  sin0  11736  ef01bndlem  11763  cos2bnd  11767  cos01gt0  11769  sincos2sgn  11772  sin4lt0  11773  egt2lt3  11786  n2dvds1  11916  flodddiv4  11938  gcdf  11972  eucalgf  12054  2prm  12126  dfphi2  12219  pockthi  12355  znnen  12398  ennnfonelem1  12407  qnnen  12431  ctiunct  12440  ssnnctlemct  12446  structcnvcnv  12477  structfn  12480  xpsff1o  12767  cnfld0  13435  cnfld1  13436  eltpsi  13511  unitg  13532  epttop  13560  txuni2  13726  retopon  13996  dedekindicclemicc  14080  reldvg  14118  dvrecap  14147  dvef  14158  sinhalfpilem  14182  coseq00topi  14226  coseq0negpitopi  14227  sincos4thpi  14231  sincos6thpi  14233  pigt3  14235  cos02pilt1  14242  logltb  14265  rpabscxpbnd  14329  lgsdir2lem2  14400  lgsdir2lem3  14401  ex-fl  14447  ex-exp  14449  bdceqi  14565  bdcriota  14605  bdsepnfALT  14611  bdbm1.3ii  14613  bj-d0clsepcl  14647  nninfsellemeqinf  14735