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  617  pm3.24  701  olc  719  orc  720  dcnn  856  dn1dc  969  3ori  1337  mptxor  1469  mpgbi  1501  dveeq2  1864  dveeq2or  1865  sbequilem  1887  nfsb  2000  sbco  2022  sbcocom  2024  hbsbd  2036  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  hbe1a  2077  elsb1  2210  elsb2  2211  eqcomi  2236  eqtri  2253  eleqtri  2307  neii  2414  neeqtri  2439  nesymi  2458  necomi  2497  nemtbir  2501  neli  2509  nrex  2634  rexlimi  2653  isseti  2822  eueq1  2989  euxfr2dc  3002  cdeqri  3028  sseqtri  3272  3sstr3i  3278  equncomi  3365  unssi  3394  ssini  3444  unabs  3452  inabs  3453  ddifss  3459  inssddif  3462  snid  3720  rabrsndc  3759  rintm  4084  breqtri  4134  bm1.3ii  4231  zfnuleu  4234  zfpow  4288  undifexmid  4306  copsexg  4360  uniop  4372  pwundifss  4406  onunisuci  4553  zfun  4555  op1stb  4599  op1stbg  4600  ordtriexmidlem  4641  ordtriexmid  4643  ordtri2orexmid  4645  2ordpr  4646  ontr2exmid  4647  onsucsssucexmid  4649  onsucelsucexmid  4652  dtruex  4681  ordsoexmid  4684  0elsucexmid  4687  ordtri2or2exmid  4693  dcextest  4703  tfi  4704  relop  4905  dmxpid  4978  rn0  5013  dmresi  5093  issref  5145  cnvcnv  5215  rescnvcnv  5225  cnvcnvres  5226  cnvsn  5245  cocnvcnv2  5274  cores2  5275  co01  5277  relcoi1  5294  cnviinm  5304  fnopab  5483  mpt0  5486  fnmpti  5487  f1cnvcnv  5584  f1ovi  5655  fmpti  5829  fvsnun2  5882  oprabss  6139  relmptopab  6256  2nd0  6339  f1stres  6353  f2ndres  6354  reldmtpos  6484  dftpos4  6494  tpostpos  6495  tpos0  6505  smo0  6529  frecfnom  6632  oasuc  6697  uniixp  6956  ssdomg  7018  xpcomf1o  7076  ssfilem  7130  diffitest  7144  inffiexmid  7166  fiintim  7191  caseinl  7382  caseinr  7383  eninl  7388  eninr  7389  card0  7484  dju1p1e2  7500  pw1on  7536  dmaddpi  7640  dmmulpi  7641  1lt2pi  7655  1lt2nq  7721  suplocsrlempr  8122  gtso  8352  subf  8475  negne0i  8548  negdii  8557  ltapii  8909  sup3exmid  9231  neg1ap0  9346  halflt1  9455  nn0ssz  9595  3halfnz  9675  zeo  9683  numlt  9733  numltc  9734  le9lt10  9735  decle  9742  uzf  9856  indstr  9925  infrenegsupex  9926  xaddf  10177  ixxf  10231  iooval2  10248  ioof  10304  unirnioo  10306  fzval2  10345  fzf  10346  fz10  10380  fzpreddisj  10405  4fvwrd4  10474  fzof  10478  fldiv4p1lem1div2  10665  fldiv4lem1div2  10667  xnn0nnen  10799  hashfibc  11207  sqrt2gt1lt2  11734  infxrnegsupex  11948  fclim  11979  fsumrelem  12157  arisum2  12185  geo2sum2  12201  0.999...  12207  ege2le3  12357  sin0  12415  ef01bndlem  12442  cos2bnd  12446  cos01gt0  12449  sincos2sgn  12452  sin4lt0  12453  egt2lt3  12466  n2dvds1  12598  flodddiv4  12622  0bits  12645  gcdf  12668  nninfct  12737  eucalgf  12752  2prm  12824  dfphi2  12917  pockthi  13056  karatsuba  13128  ballotfilem2  13142  znnen  13149  ennnfonelem1  13158  qnnen  13182  ctiunct  13191  ssnnctlemct  13197  structcnvcnv  13228  structfn  13231  relelbasov  13275  xpsff1o  13562  rmodislmod  14499  cnfld0  14719  cnfld1  14720  eltpsi  14906  unitg  14927  epttop  14955  txuni2  15121  retopon  15391  cnfldtopon  15405  dedekindicclemicc  15497  reldvg  15544  dvrecap  15578  dvef  15592  plyrecj  15628  sinhalfpilem  15656  coseq00topi  15700  coseq0negpitopi  15701  sincos4thpi  15705  sincos6thpi  15707  pigt3  15709  cos02pilt1  15716  logltb  15739  rpabscxpbnd  15805  sgmf  15854  1sgm2ppw  15863  lgsdir2lem2  15902  lgsdir2lem3  15903  konigsbergiedgwen  16479  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem4  16486  konigsberglem5  16487  konigsberg  16488  ex-fl  16493  ex-exp  16495  bdceqi  16613  bdcriota  16653  bdsepnfALT  16659  bdbm1.3ii  16661  bj-d0clsepcl  16695  nninfsellemeqinf  16794