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  389  pm4.71ri  390  pm5.32i  450  biadanii  603  pm3.24  683  olc  701  orc  702  dcnn  838  dn1dc  950  3ori  1290  mptxor  1414  mpgbi  1440  dveeq2  1803  dveeq2or  1804  sbequilem  1826  nfsb  1934  sbco  1956  sbcocom  1958  hbsbd  1970  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  hbe1a  2011  elsb1  2143  elsb2  2144  eqcomi  2169  eqtri  2186  eleqtri  2240  neii  2337  neeqtri  2362  nesymi  2381  necomi  2420  nemtbir  2424  neli  2432  nrex  2557  rexlimi  2575  isseti  2733  eueq1  2897  euxfr2dc  2910  cdeqri  2936  sseqtri  3175  3sstr3i  3181  equncomi  3267  unssi  3296  ssini  3344  unabs  3352  inabs  3353  ddifss  3359  inssddif  3362  rgenm  3510  snid  3606  rabrsndc  3643  rintm  3957  breqtri  4006  bm1.3ii  4102  zfnuleu  4105  zfpow  4153  undifexmid  4171  copsexg  4221  uniop  4232  pwundifss  4262  onunisuci  4409  zfun  4411  op1stb  4455  op1stbg  4456  ordtriexmidlem  4495  ordtriexmid  4497  ordtri2orexmid  4499  2ordpr  4500  ontr2exmid  4501  onsucsssucexmid  4503  onsucelsucexmid  4506  dtruex  4535  ordsoexmid  4538  0elsucexmid  4541  ordtri2or2exmid  4547  dcextest  4557  tfi  4558  relop  4753  dmxpid  4824  rn0  4859  dmresi  4938  issref  4985  cnvcnv  5055  rescnvcnv  5065  cnvcnvres  5066  cnvsn  5085  cocnvcnv2  5114  cores2  5115  co01  5117  relcoi1  5134  cnviinm  5144  fnopab  5311  mpt0  5314  fnmpti  5315  f1cnvcnv  5403  f1ovi  5470  fmpti  5636  fvsnun2  5682  oprabss  5924  2nd0  6110  f1stres  6124  f2ndres  6125  reldmtpos  6217  dftpos4  6227  tpostpos  6228  tpos0  6238  smo0  6262  frecfnom  6365  oasuc  6428  uniixp  6683  ssdomg  6740  xpcomf1o  6787  ssfilem  6837  diffitest  6849  inffiexmid  6868  fiintim  6890  caseinl  7052  caseinr  7053  eninl  7058  eninr  7059  card0  7140  dju1p1e2  7149  pw1on  7178  dmaddpi  7262  dmmulpi  7263  1lt2pi  7277  1lt2nq  7343  suplocsrlempr  7744  gtso  7973  subf  8096  negne0i  8169  negdii  8178  ltapii  8529  sup3exmid  8848  neg1ap0  8962  halflt1  9070  nn0ssz  9205  3halfnz  9284  zeo  9292  numlt  9342  numltc  9343  le9lt10  9344  decle  9351  uzf  9465  indstr  9527  infrenegsupex  9528  xaddf  9776  ixxf  9830  iooval2  9847  ioof  9903  unirnioo  9905  fzval2  9943  fzf  9944  fz10  9977  fzpreddisj  10002  4fvwrd4  10071  fzof  10075  fldiv4p1lem1div2  10236  sqrt2gt1lt2  10987  infxrnegsupex  11200  fclim  11231  fsumrelem  11408  arisum2  11436  geo2sum2  11452  0.999...  11458  ege2le3  11608  sin0  11666  ef01bndlem  11693  cos2bnd  11697  cos01gt0  11699  sincos2sgn  11702  sin4lt0  11703  egt2lt3  11716  n2dvds1  11845  flodddiv4  11867  gcdf  11901  eucalgf  11983  2prm  12055  dfphi2  12148  pockthi  12284  znnen  12327  ennnfonelem1  12336  qnnen  12360  ctiunct  12369  ssnnctlemct  12375  structcnvcnv  12406  structfn  12409  eltpsi  12639  unitg  12662  epttop  12690  txuni2  12856  retopon  13126  dedekindicclemicc  13210  reldvg  13248  dvrecap  13277  dvef  13288  sinhalfpilem  13312  coseq00topi  13356  coseq0negpitopi  13357  sincos4thpi  13361  sincos6thpi  13363  pigt3  13365  cos02pilt1  13372  logltb  13395  rpabscxpbnd  13459  lgsdir2lem2  13530  lgsdir2lem3  13531  ex-fl  13566  ex-exp  13568  bdceqi  13685  bdcriota  13725  bdsepnfALT  13731  bdbm1.3ii  13733  bj-d0clsepcl  13767  nninfsellemeqinf  13856