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  834  dn1dc  945  3ori  1279  mptxor  1403  mpgbi  1429  dveeq2  1792  dveeq2or  1793  sbequilem  1815  nfsb  1923  sbco  1945  sbcocom  1947  hbsbd  1959  dvelimALT  1987  dvelimfv  1988  dvelimor  1995  hbe1a  2000  elsb3  2132  elsb4  2133  eqcomi  2158  eqtri  2175  eleqtri  2229  neii  2326  neeqtri  2351  nesymi  2370  necomi  2409  nemtbir  2413  neli  2421  nrex  2546  rexlimi  2564  isseti  2717  eueq1  2880  euxfr2dc  2893  cdeqri  2919  sseqtri  3158  3sstr3i  3164  equncomi  3249  unssi  3278  ssini  3326  unabs  3334  inabs  3335  ddifss  3341  inssddif  3344  rgenm  3492  snid  3587  rabrsndc  3623  rintm  3937  breqtri  3985  bm1.3ii  4081  zfnuleu  4084  zfpow  4131  undifexmid  4149  copsexg  4199  uniop  4210  pwundifss  4240  onunisuci  4387  zfun  4389  op1stb  4432  op1stbg  4433  ordtriexmidlem  4472  ordtriexmid  4474  ordtri2orexmid  4476  2ordpr  4477  ontr2exmid  4478  onsucsssucexmid  4480  onsucelsucexmid  4483  dtruex  4512  ordsoexmid  4515  0elsucexmid  4518  ordtri2or2exmid  4524  dcextest  4534  tfi  4535  relop  4729  dmxpid  4800  rn0  4835  dmresi  4914  issref  4961  cnvcnv  5031  rescnvcnv  5041  cnvcnvres  5042  cnvsn  5061  cocnvcnv2  5090  cores2  5091  co01  5093  relcoi1  5110  cnviinm  5120  fnopab  5287  mpt0  5290  fnmpti  5291  f1cnvcnv  5379  f1ovi  5446  fmpti  5612  fvsnun2  5658  oprabss  5897  2nd0  6083  f1stres  6097  f2ndres  6098  reldmtpos  6190  dftpos4  6200  tpostpos  6201  tpos0  6211  smo0  6235  frecfnom  6338  oasuc  6400  uniixp  6655  ssdomg  6712  xpcomf1o  6759  ssfilem  6809  diffitest  6821  inffiexmid  6840  fiintim  6862  caseinl  7021  caseinr  7022  eninl  7027  eninr  7028  card0  7102  dju1p1e2  7111  pw1on  7140  dmaddpi  7224  dmmulpi  7225  1lt2pi  7239  1lt2nq  7305  suplocsrlempr  7706  gtso  7935  subf  8056  negne0i  8129  negdii  8138  ltapii  8489  sup3exmid  8807  neg1ap0  8921  halflt1  9029  nn0ssz  9164  3halfnz  9240  zeo  9248  numlt  9298  numltc  9299  le9lt10  9300  decle  9307  uzf  9421  indstr  9483  infrenegsupex  9484  xaddf  9726  ixxf  9780  iooval2  9797  ioof  9853  unirnioo  9855  fzval2  9893  fzf  9894  fz10  9926  fzpreddisj  9951  4fvwrd4  10017  fzof  10021  fldiv4p1lem1div2  10182  sqrt2gt1lt2  10926  infxrnegsupex  11137  fclim  11168  fsumrelem  11345  arisum2  11373  geo2sum2  11389  0.999...  11395  ege2le3  11545  sin0  11603  ef01bndlem  11630  cos2bnd  11634  cos01gt0  11636  sincos2sgn  11639  sin4lt0  11640  egt2lt3  11653  n2dvds1  11776  flodddiv4  11798  gcdf  11828  eucalgf  11904  2prm  11976  dfphi2  12064  znnen  12086  ennnfonelem1  12095  qnnen  12119  ctiunct  12128  structcnvcnv  12153  structfn  12156  eltpsi  12386  unitg  12409  epttop  12437  txuni2  12603  retopon  12873  dedekindicclemicc  12957  reldvg  12995  dvrecap  13024  dvef  13035  sinhalfpilem  13059  coseq00topi  13103  coseq0negpitopi  13104  sincos4thpi  13108  sincos6thpi  13110  pigt3  13112  cos02pilt1  13119  logltb  13142  rpabscxpbnd  13206  ex-fl  13247  ex-exp  13249  bdceqi  13364  bdcriota  13404  bdsepnfALT  13410  bdbm1.3ii  13412  bj-d0clsepcl  13446  nninfsellemeqinf  13537