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  1788  dveeq2or  1789  sbequilem  1811  nfsb  1920  sbco  1942  sbcocom  1944  elsb3  1952  elsb4  1953  hbsbd  1958  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  eqcomi  2144  eqtri  2161  eleqtri  2215  neii  2311  neeqtri  2336  nesymi  2355  necomi  2394  nemtbir  2398  neli  2406  nrex  2527  rexlimi  2545  isseti  2697  eueq1  2860  euxfr2dc  2873  cdeqri  2899  sseqtri  3136  3sstr3i  3142  equncomi  3227  unssi  3256  ssini  3304  unabs  3312  inabs  3313  ddifss  3319  inssddif  3322  rgenm  3470  snid  3563  rabrsndc  3599  rintm  3913  breqtri  3961  bm1.3ii  4057  zfnuleu  4060  zfpow  4107  undifexmid  4125  copsexg  4174  uniop  4185  pwundifss  4215  onunisuci  4362  zfun  4364  op1stb  4407  op1stbg  4408  ordtriexmidlem  4443  ordtriexmid  4445  ordtri2orexmid  4446  2ordpr  4447  ontr2exmid  4448  onsucsssucexmid  4450  onsucelsucexmid  4453  dtruex  4482  ordsoexmid  4485  0elsucexmid  4488  ordtri2or2exmid  4494  dcextest  4503  tfi  4504  relop  4697  dmxpid  4768  rn0  4803  dmresi  4882  issref  4929  cnvcnv  4999  rescnvcnv  5009  cnvcnvres  5010  cnvsn  5029  cocnvcnv2  5058  cores2  5059  co01  5061  relcoi1  5078  cnviinm  5088  fnopab  5255  mpt0  5258  fnmpti  5259  f1cnvcnv  5347  f1ovi  5414  fmpti  5580  fvsnun2  5626  oprabss  5865  2nd0  6051  f1stres  6065  f2ndres  6066  reldmtpos  6158  dftpos4  6168  tpostpos  6169  tpos0  6179  smo0  6203  frecfnom  6306  oasuc  6368  uniixp  6623  ssdomg  6680  xpcomf1o  6727  ssfilem  6777  diffitest  6789  inffiexmid  6808  fiintim  6825  caseinl  6984  caseinr  6985  eninl  6990  eninr  6991  card0  7061  dju1p1e2  7070  dmaddpi  7157  dmmulpi  7158  1lt2pi  7172  1lt2nq  7238  suplocsrlempr  7639  gtso  7867  subf  7988  negne0i  8061  negdii  8070  ltapii  8421  sup3exmid  8739  neg1ap0  8853  halflt1  8961  nn0ssz  9096  3halfnz  9172  zeo  9180  numlt  9230  numltc  9231  le9lt10  9232  decle  9239  uzf  9353  indstr  9415  infrenegsupex  9416  xaddf  9657  ixxf  9711  iooval2  9728  ioof  9784  unirnioo  9786  fzval2  9824  fzf  9825  fz10  9857  fzpreddisj  9882  4fvwrd4  9948  fzof  9952  fldiv4p1lem1div2  10109  sqrt2gt1lt2  10853  infxrnegsupex  11064  fclim  11095  fsumrelem  11272  arisum2  11300  geo2sum2  11316  0.999...  11322  ege2le3  11414  sin0  11472  ef01bndlem  11499  cos2bnd  11503  cos01gt0  11505  sincos2sgn  11508  sin4lt0  11509  egt2lt3  11522  n2dvds1  11645  flodddiv4  11667  gcdf  11697  eucalgf  11772  2prm  11844  dfphi2  11932  znnen  11947  ennnfonelem1  11956  qnnen  11980  ctiunct  11989  structcnvcnv  12014  structfn  12017  eltpsi  12247  unitg  12270  epttop  12298  txuni2  12464  retopon  12734  dedekindicclemicc  12818  reldvg  12856  dvrecap  12885  dvef  12896  sinhalfpilem  12920  coseq00topi  12964  coseq0negpitopi  12965  sincos4thpi  12969  sincos6thpi  12971  pigt3  12973  cos02pilt1  12980  logltb  13003  rpabscxpbnd  13067  ex-fl  13108  ex-exp  13110  bdceqi  13212  bdcriota  13252  bdsepnfALT  13258  bdbm1.3ii  13260  bj-d0clsepcl  13294  nninfsellemeqinf  13387