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  2746  eueq1  2910  euxfr2dc  2923  cdeqri  2949  sseqtri  3190  3sstr3i  3196  equncomi  3282  unssi  3311  ssini  3359  unabs  3367  inabs  3368  ddifss  3374  inssddif  3377  rgenm  3526  snid  3624  rabrsndc  3661  rintm  3980  breqtri  4029  bm1.3ii  4125  zfnuleu  4128  zfpow  4176  undifexmid  4194  copsexg  4245  uniop  4256  pwundifss  4286  onunisuci  4433  zfun  4435  op1stb  4479  op1stbg  4480  ordtriexmidlem  4519  ordtriexmid  4521  ordtri2orexmid  4523  2ordpr  4524  ontr2exmid  4525  onsucsssucexmid  4527  onsucelsucexmid  4530  dtruex  4559  ordsoexmid  4562  0elsucexmid  4565  ordtri2or2exmid  4571  dcextest  4581  tfi  4582  relop  4778  dmxpid  4849  rn0  4884  dmresi  4963  issref  5012  cnvcnv  5082  rescnvcnv  5092  cnvcnvres  5093  cnvsn  5112  cocnvcnv2  5141  cores2  5142  co01  5144  relcoi1  5161  cnviinm  5171  fnopab  5341  mpt0  5344  fnmpti  5345  f1cnvcnv  5433  f1ovi  5501  fmpti  5669  fvsnun2  5715  oprabss  5961  2nd0  6146  f1stres  6160  f2ndres  6161  reldmtpos  6254  dftpos4  6264  tpostpos  6265  tpos0  6275  smo0  6299  frecfnom  6402  oasuc  6465  uniixp  6721  ssdomg  6778  xpcomf1o  6825  ssfilem  6875  diffitest  6887  inffiexmid  6906  fiintim  6928  caseinl  7090  caseinr  7091  eninl  7096  eninr  7097  card0  7187  dju1p1e2  7196  pw1on  7225  dmaddpi  7324  dmmulpi  7325  1lt2pi  7339  1lt2nq  7405  suplocsrlempr  7806  gtso  8036  subf  8159  negne0i  8232  negdii  8241  ltapii  8592  sup3exmid  8914  neg1ap0  9028  halflt1  9136  nn0ssz  9271  3halfnz  9350  zeo  9358  numlt  9408  numltc  9409  le9lt10  9410  decle  9417  uzf  9531  indstr  9593  infrenegsupex  9594  xaddf  9844  ixxf  9898  iooval2  9915  ioof  9971  unirnioo  9973  fzval2  10011  fzf  10012  fz10  10046  fzpreddisj  10071  4fvwrd4  10140  fzof  10144  fldiv4p1lem1div2  10305  sqrt2gt1lt2  11058  infxrnegsupex  11271  fclim  11302  fsumrelem  11479  arisum2  11507  geo2sum2  11523  0.999...  11529  ege2le3  11679  sin0  11737  ef01bndlem  11764  cos2bnd  11768  cos01gt0  11770  sincos2sgn  11773  sin4lt0  11774  egt2lt3  11787  n2dvds1  11917  flodddiv4  11939  gcdf  11973  eucalgf  12055  2prm  12127  dfphi2  12220  pockthi  12356  znnen  12399  ennnfonelem1  12408  qnnen  12432  ctiunct  12441  ssnnctlemct  12447  structcnvcnv  12478  structfn  12481  xpsff1o  12768  rmodislmod  13441  cnfld0  13468  cnfld1  13469  eltpsi  13544  unitg  13565  epttop  13593  txuni2  13759  retopon  14029  dedekindicclemicc  14113  reldvg  14151  dvrecap  14180  dvef  14191  sinhalfpilem  14215  coseq00topi  14259  coseq0negpitopi  14260  sincos4thpi  14264  sincos6thpi  14266  pigt3  14268  cos02pilt1  14275  logltb  14298  rpabscxpbnd  14362  lgsdir2lem2  14433  lgsdir2lem3  14434  ex-fl  14480  ex-exp  14482  bdceqi  14598  bdcriota  14638  bdsepnfALT  14644  bdbm1.3ii  14646  bj-d0clsepcl  14680  nninfsellemeqinf  14768