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  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  2821  eueq1  2988  euxfr2dc  3001  cdeqri  3027  sseqtri  3271  3sstr3i  3277  equncomi  3364  unssi  3393  ssini  3443  unabs  3451  inabs  3452  ddifss  3458  inssddif  3461  snid  3719  rabrsndc  3758  rintm  4083  breqtri  4133  bm1.3ii  4230  zfnuleu  4233  zfpow  4287  undifexmid  4305  copsexg  4359  uniop  4371  pwundifss  4405  onunisuci  4552  zfun  4554  op1stb  4598  op1stbg  4599  ordtriexmidlem  4640  ordtriexmid  4642  ordtri2orexmid  4644  2ordpr  4645  ontr2exmid  4646  onsucsssucexmid  4648  onsucelsucexmid  4651  dtruex  4680  ordsoexmid  4683  0elsucexmid  4686  ordtri2or2exmid  4692  dcextest  4702  tfi  4703  relop  4904  dmxpid  4977  rn0  5012  dmresi  5092  issref  5144  cnvcnv  5214  rescnvcnv  5224  cnvcnvres  5225  cnvsn  5244  cocnvcnv2  5273  cores2  5274  co01  5276  relcoi1  5293  cnviinm  5303  fnopab  5482  mpt0  5485  fnmpti  5486  f1cnvcnv  5583  f1ovi  5654  fmpti  5828  fvsnun2  5881  oprabss  6138  relmptopab  6255  2nd0  6338  f1stres  6352  f2ndres  6353  reldmtpos  6483  dftpos4  6493  tpostpos  6494  tpos0  6504  smo0  6528  frecfnom  6631  oasuc  6696  uniixp  6955  ssdomg  7017  xpcomf1o  7075  ssfilem  7129  diffitest  7143  inffiexmid  7165  fiintim  7190  caseinl  7381  caseinr  7382  eninl  7387  eninr  7388  card0  7483  dju1p1e2  7499  pw1on  7535  dmaddpi  7636  dmmulpi  7637  1lt2pi  7651  1lt2nq  7717  suplocsrlempr  8118  gtso  8348  subf  8471  negne0i  8544  negdii  8553  ltapii  8905  sup3exmid  9227  neg1ap0  9342  halflt1  9451  nn0ssz  9591  3halfnz  9671  zeo  9679  numlt  9729  numltc  9730  le9lt10  9731  decle  9738  uzf  9852  indstr  9921  infrenegsupex  9922  xaddf  10173  ixxf  10227  iooval2  10244  ioof  10300  unirnioo  10302  fzval2  10341  fzf  10342  fz10  10376  fzpreddisj  10401  4fvwrd4  10470  fzof  10474  fldiv4p1lem1div2  10661  fldiv4lem1div2  10663  xnn0nnen  10795  hashfibc  11200  sqrt2gt1lt2  11727  infxrnegsupex  11941  fclim  11972  fsumrelem  12150  arisum2  12178  geo2sum2  12194  0.999...  12200  ege2le3  12350  sin0  12408  ef01bndlem  12435  cos2bnd  12439  cos01gt0  12442  sincos2sgn  12445  sin4lt0  12446  egt2lt3  12459  n2dvds1  12591  flodddiv4  12615  0bits  12638  gcdf  12661  nninfct  12730  eucalgf  12745  2prm  12817  dfphi2  12910  pockthi  13049  karatsuba  13121  znnen  13138  ennnfonelem1  13147  qnnen  13171  ctiunct  13180  ssnnctlemct  13186  structcnvcnv  13217  structfn  13220  relelbasov  13264  xpsff1o  13551  rmodislmod  14486  cnfld0  14706  cnfld1  14707  eltpsi  14893  unitg  14914  epttop  14942  txuni2  15108  retopon  15378  cnfldtopon  15392  dedekindicclemicc  15484  reldvg  15531  dvrecap  15565  dvef  15579  plyrecj  15615  sinhalfpilem  15643  coseq00topi  15687  coseq0negpitopi  15688  sincos4thpi  15692  sincos6thpi  15694  pigt3  15696  cos02pilt1  15703  logltb  15726  rpabscxpbnd  15792  sgmf  15841  1sgm2ppw  15850  lgsdir2lem2  15889  lgsdir2lem3  15890  konigsbergiedgwen  16466  konigsberglem1  16470  konigsberglem2  16471  konigsberglem3  16472  konigsberglem4  16473  konigsberglem5  16474  konigsberg  16475  ex-fl  16480  ex-exp  16482  bdceqi  16600  bdcriota  16640  bdsepnfALT  16646  bdbm1.3ii  16648  bj-d0clsepcl  16682  nninfsellemeqinf  16781