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  694  olc  712  orc  713  dcnn  849  dn1dc  962  3ori  1311  mptxor  1435  mpgbi  1463  dveeq2  1826  dveeq2or  1827  sbequilem  1849  nfsb  1962  sbco  1984  sbcocom  1986  hbsbd  1998  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  hbe1a  2039  elsb1  2171  elsb2  2172  eqcomi  2197  eqtri  2214  eleqtri  2268  neii  2366  neeqtri  2391  nesymi  2410  necomi  2449  nemtbir  2453  neli  2461  nrex  2586  rexlimi  2604  isseti  2768  eueq1  2932  euxfr2dc  2945  cdeqri  2971  sseqtri  3213  3sstr3i  3219  equncomi  3305  unssi  3334  ssini  3382  unabs  3390  inabs  3391  ddifss  3397  inssddif  3400  snid  3649  rabrsndc  3686  rintm  4005  breqtri  4054  bm1.3ii  4150  zfnuleu  4153  zfpow  4204  undifexmid  4222  copsexg  4273  uniop  4284  pwundifss  4316  onunisuci  4463  zfun  4465  op1stb  4509  op1stbg  4510  ordtriexmidlem  4551  ordtriexmid  4553  ordtri2orexmid  4555  2ordpr  4556  ontr2exmid  4557  onsucsssucexmid  4559  onsucelsucexmid  4562  dtruex  4591  ordsoexmid  4594  0elsucexmid  4597  ordtri2or2exmid  4603  dcextest  4613  tfi  4614  relop  4812  dmxpid  4883  rn0  4918  dmresi  4997  issref  5048  cnvcnv  5118  rescnvcnv  5128  cnvcnvres  5129  cnvsn  5148  cocnvcnv2  5177  cores2  5178  co01  5180  relcoi1  5197  cnviinm  5207  fnopab  5378  mpt0  5381  fnmpti  5382  f1cnvcnv  5470  f1ovi  5539  fmpti  5710  fvsnun2  5756  oprabss  6004  2nd0  6198  f1stres  6212  f2ndres  6213  reldmtpos  6306  dftpos4  6316  tpostpos  6317  tpos0  6327  smo0  6351  frecfnom  6454  oasuc  6517  uniixp  6775  ssdomg  6832  xpcomf1o  6879  ssfilem  6931  diffitest  6943  inffiexmid  6962  fiintim  6985  caseinl  7150  caseinr  7151  eninl  7156  eninr  7157  card0  7248  dju1p1e2  7257  pw1on  7286  dmaddpi  7385  dmmulpi  7386  1lt2pi  7400  1lt2nq  7466  suplocsrlempr  7867  gtso  8098  subf  8221  negne0i  8294  negdii  8303  ltapii  8654  sup3exmid  8976  neg1ap0  9091  halflt1  9199  nn0ssz  9335  3halfnz  9414  zeo  9422  numlt  9472  numltc  9473  le9lt10  9474  decle  9481  uzf  9595  indstr  9658  infrenegsupex  9659  xaddf  9910  ixxf  9964  iooval2  9981  ioof  10037  unirnioo  10039  fzval2  10077  fzf  10078  fz10  10112  fzpreddisj  10137  4fvwrd4  10206  fzof  10210  fldiv4p1lem1div2  10374  fldiv4lem1div2  10376  xnn0nnen  10508  sqrt2gt1lt2  11193  infxrnegsupex  11406  fclim  11437  fsumrelem  11614  arisum2  11642  geo2sum2  11658  0.999...  11664  ege2le3  11814  sin0  11872  ef01bndlem  11899  cos2bnd  11903  cos01gt0  11906  sincos2sgn  11909  sin4lt0  11910  egt2lt3  11923  n2dvds1  12053  flodddiv4  12075  gcdf  12109  nninfct  12178  eucalgf  12193  2prm  12265  dfphi2  12358  pockthi  12496  znnen  12555  ennnfonelem1  12564  qnnen  12588  ctiunct  12597  ssnnctlemct  12603  structcnvcnv  12634  structfn  12637  relelbasov  12680  xpsff1o  12932  rmodislmod  13847  cnfld0  14059  cnfld1  14060  eltpsi  14209  unitg  14230  epttop  14258  txuni2  14424  retopon  14694  dedekindicclemicc  14786  reldvg  14833  dvrecap  14862  dvef  14873  sinhalfpilem  14926  coseq00topi  14970  coseq0negpitopi  14971  sincos4thpi  14975  sincos6thpi  14977  pigt3  14979  cos02pilt1  14986  logltb  15009  rpabscxpbnd  15073  lgsdir2lem2  15145  lgsdir2lem3  15146  ex-fl  15217  ex-exp  15219  bdceqi  15335  bdcriota  15375  bdsepnfALT  15381  bdbm1.3ii  15383  bj-d0clsepcl  15417  nninfsellemeqinf  15506