Theorem mpbi 145

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbi.min	⊢ 𝜑
mpbi.maj	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mpbi	⊢ 𝜓

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 ⊢ 𝜑
2		mpbi.maj	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpi 120	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

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  693  olc  711  orc  712  dcnn  848  dn1dc  960  3ori  1300  mptxor  1424  mpgbi  1452  dveeq2  1815  dveeq2or  1816  sbequilem  1838  nfsb  1946  sbco  1968  sbcocom  1970  hbsbd  1982  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  hbe1a  2023  elsb1  2155  elsb2  2156  eqcomi  2181  eqtri  2198  eleqtri  2252  neii  2349  neeqtri  2374  nesymi  2393  necomi  2432  nemtbir  2436  neli  2444  nrex  2569  rexlimi  2587  isseti  2745  eueq1  2909  euxfr2dc  2922  cdeqri  2948  sseqtri  3189  3sstr3i  3195  equncomi  3281  unssi  3310  ssini  3358  unabs  3366  inabs  3367  ddifss  3373  inssddif  3376  rgenm  3525  snid  3623  rabrsndc  3660  rintm  3978  breqtri  4027  bm1.3ii  4123  zfnuleu  4126  zfpow  4174  undifexmid  4192  copsexg  4243  uniop  4254  pwundifss  4284  onunisuci  4431  zfun  4433  op1stb  4477  op1stbg  4478  ordtriexmidlem  4517  ordtriexmid  4519  ordtri2orexmid  4521  2ordpr  4522  ontr2exmid  4523  onsucsssucexmid  4525  onsucelsucexmid  4528  dtruex  4557  ordsoexmid  4560  0elsucexmid  4563  ordtri2or2exmid  4569  dcextest  4579  tfi  4580  relop  4776  dmxpid  4847  rn0  4882  dmresi  4961  issref  5010  cnvcnv  5080  rescnvcnv  5090  cnvcnvres  5091  cnvsn  5110  cocnvcnv2  5139  cores2  5140  co01  5142  relcoi1  5159  cnviinm  5169  fnopab  5339  mpt0  5342  fnmpti  5343  f1cnvcnv  5431  f1ovi  5499  fmpti  5667  fvsnun2  5713  oprabss  5958  2nd0  6143  f1stres  6157  f2ndres  6158  reldmtpos  6251  dftpos4  6261  tpostpos  6262  tpos0  6272  smo0  6296  frecfnom  6399  oasuc  6462  uniixp  6718  ssdomg  6775  xpcomf1o  6822  ssfilem  6872  diffitest  6884  inffiexmid  6903  fiintim  6925  caseinl  7087  caseinr  7088  eninl  7093  eninr  7094  card0  7184  dju1p1e2  7193  pw1on  7222  dmaddpi  7321  dmmulpi  7322  1lt2pi  7336  1lt2nq  7402  suplocsrlempr  7803  gtso  8032  subf  8155  negne0i  8228  negdii  8237  ltapii  8588  sup3exmid  8910  neg1ap0  9024  halflt1  9132  nn0ssz  9267  3halfnz  9346  zeo  9354  numlt  9404  numltc  9405  le9lt10  9406  decle  9413  uzf  9527  indstr  9589  infrenegsupex  9590  xaddf  9840  ixxf  9894  iooval2  9911  ioof  9967  unirnioo  9969  fzval2  10007  fzf  10008  fz10  10041  fzpreddisj  10066  4fvwrd4  10135  fzof  10139  fldiv4p1lem1div2  10300  sqrt2gt1lt2  11051  infxrnegsupex  11264  fclim  11295  fsumrelem  11472  arisum2  11500  geo2sum2  11516  0.999...  11522  ege2le3  11672  sin0  11730  ef01bndlem  11757  cos2bnd  11761  cos01gt0  11763  sincos2sgn  11766  sin4lt0  11767  egt2lt3  11780  n2dvds1  11909  flodddiv4  11931  gcdf  11965  eucalgf  12047  2prm  12119  dfphi2  12212  pockthi  12348  znnen  12391  ennnfonelem1  12400  qnnen  12424  ctiunct  12433  ssnnctlemct  12439  structcnvcnv  12470  structfn  12473  cnfld0  13334  cnfld1  13335  eltpsi  13410  unitg  13433  epttop  13461  txuni2  13627  retopon  13897  dedekindicclemicc  13981  reldvg  14019  dvrecap  14048  dvef  14059  sinhalfpilem  14083  coseq00topi  14127  coseq0negpitopi  14128  sincos4thpi  14132  sincos6thpi  14134  pigt3  14136  cos02pilt1  14143  logltb  14166  rpabscxpbnd  14230  lgsdir2lem2  14301  lgsdir2lem3  14302  ex-fl  14337  ex-exp  14339  bdceqi  14455  bdcriota  14495  bdsepnfALT  14501  bdbm1.3ii  14503  bj-d0clsepcl  14537  nninfsellemeqinf  14625