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  8034  subf  8157  negne0i  8230  negdii  8239  ltapii  8590  sup3exmid  8912  neg1ap0  9026  halflt1  9134  nn0ssz  9269  3halfnz  9348  zeo  9356  numlt  9406  numltc  9407  le9lt10  9408  decle  9415  uzf  9529  indstr  9591  infrenegsupex  9592  xaddf  9842  ixxf  9896  iooval2  9913  ioof  9969  unirnioo  9971  fzval2  10009  fzf  10010  fz10  10043  fzpreddisj  10068  4fvwrd4  10137  fzof  10141  fldiv4p1lem1div2  10302  sqrt2gt1lt2  11053  infxrnegsupex  11266  fclim  11297  fsumrelem  11474  arisum2  11502  geo2sum2  11518  0.999...  11524  ege2le3  11674  sin0  11732  ef01bndlem  11759  cos2bnd  11763  cos01gt0  11765  sincos2sgn  11768  sin4lt0  11769  egt2lt3  11782  n2dvds1  11911  flodddiv4  11933  gcdf  11967  eucalgf  12049  2prm  12121  dfphi2  12214  pockthi  12350  znnen  12393  ennnfonelem1  12402  qnnen  12426  ctiunct  12435  ssnnctlemct  12441  structcnvcnv  12472  structfn  12475  xpsff1o  12762  cnfld0  13396  cnfld1  13397  eltpsi  13472  unitg  13493  epttop  13521  txuni2  13687  retopon  13957  dedekindicclemicc  14041  reldvg  14079  dvrecap  14108  dvef  14119  sinhalfpilem  14143  coseq00topi  14187  coseq0negpitopi  14188  sincos4thpi  14192  sincos6thpi  14194  pigt3  14196  cos02pilt1  14203  logltb  14226  rpabscxpbnd  14290  lgsdir2lem2  14361  lgsdir2lem3  14362  ex-fl  14397  ex-exp  14399  bdceqi  14515  bdcriota  14555  bdsepnfALT  14561  bdbm1.3ii  14563  bj-d0clsepcl  14597  nninfsellemeqinf  14685