Theorem mpbi 232

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-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 218	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  pm5.74i  273  notbii  322  biluk  389  pm5.19  390  pm3.24  405  dfbi  478  pm4.71i  562  pm5.32i  577  biadani  818  biadanii  820  imori  850  ori  857  pm5.16  1010  dn1  1052  3ori  1420  cadan  1606  nic-dfim  1666  nic-dfneg  1667  nic-mp  1668  nic-mpALT  1669  tbw-negdf  1696  rb-imdf  1747  nfri  1786  mpgbi  1795  19.35i  1875  nfim1  2195  19.36i  2229  sbievOLD  2327  ax6  2398  sbie  2540  sbieALT  2609  datisi  2763  disamis  2764  dimatis  2771  fresison  2772  bamalip  2775  axi12  2789  axi12OLD  2790  eqcomi  2830  eqtri  2844  eleqtri  2911  neii  3018  necomi  3070  neeqtri  3088  neli  3125  nrex  3269  rexlimiv  3280  rexlimi  3315  issetiOLD  3509  vtocl2OLD  3562  eueqi  3699  euxfr2w  3710  euxfr2  3712  reuxfrd  3738  cdeqri  3756  sseqtri  4002  3sstr3i  4008  pssn2lp  4077  equncomi  4130  unssi  4160  ssini  4207  unabs  4230  inabs  4231  dfin4  4243  difid  4329  ab0orv  4334  disjdif  4420  difin0  4421  snid  4594  rabrsn  4653  iinrab2  4984  symdifv  5000  rintn0  5022  breqtri  5083  axsepgfromrep  5193  bm1.3ii  5198  ax6vsep  5199  notzfaus  5254  notzfausOLD  5255  zfpow  5259  dtru  5263  dtruALT  5280  reusv2lem4  5293  dtruALT2  5327  op1stb  5355  copsexgw  5373  copsexg  5374  uniop  5397  pwunss  5447  pwundif  5450  pwundifOLD  5451  rn0  5790  dmresi  5915  somincom  5988  cnvcnv  6043  elid  6050  rescnvcnv  6055  cnvcnvres  6056  cocnvcnv2  6105  cores2  6106  co01  6108  cnviin  6131  onunisuci  6298  iota4an  6331  fnopab  6480  mpt0  6484  fnmpti  6485  f1cnvcnv  6578  f1ovi  6647  eliman0  6699  fvco4i  6756  fmpti  6870  funiunfv  7001  oprabss  7254  relmptopab  7389  zfun  7456  tfinds2  7572  omon  7585  2nd0  7690  f1stres  7707  f2ndres  7708  cnvoprab  7752  relmpoopab  7783  df1st2  7787  df2nd2  7788  fsplit  7806  fsplitOLD  7807  reldmtpos  7894  dftpos4  7905  tpostpos  7906  tpos0  7916  wfrlem4  7952  smo0  7989  tfrlem14  8021  tfrlem16  8023  rdgsucg  8053  rdglimg  8055  frfnom  8064  oawordeulem  8174  uniixp  8479  dfdom2  8529  ssdomg  8549  xpcomf1o  8600  sbthlem5  8625  pwdom  8663  limensuci  8687  fiint  8789  fidomdm  8795  residfi  8799  pwfilem  8812  mptfi  8817  fisn  8885  dffi3  8889  ordtypelem6  8981  ordtypelem7  8982  wemaplem2  9005  wdompwdom  9036  harwdom  9048  suc11reg  9076  zfinf  9096  axinf2  9097  noinfep  9117  cantnfvalf  9122  cantnflt  9129  cantnf0  9132  cantnf  9150  tz9.1c  9166  tc2  9178  r111  9198  r1tr2  9200  r1ordg  9201  r1sssuc  9206  r1val1  9209  tz9.13  9214  r1elssi  9228  pwwf  9230  rankopb  9275  rankeq0b  9283  ranksuc  9288  rankmapu  9301  rankxplim  9302  rankxplim3  9304  rankxpsuc  9305  cp  9314  karden  9318  card0  9381  cardlim  9395  cardom  9409  infxpenlem  9433  alephsuc2  9500  alephgeom  9502  unialeph  9521  dfac4  9542  dfacacn  9561  dju1dif  9592  dju1p1e2  9593  infdju1  9609  ackbij1lem13  9648  ackbij2  9659  cf0  9667  cfsuc  9673  cfom  9680  cfslb2n  9684  ominf4  9728  fin23lem17  9754  fin23lem28  9756  fin23lem30  9758  fin23lem31  9759  fin23lem40  9767  isfin1-3  9802  dfacfin7  9815  fin1a2lem6  9821  itunitc1  9836  axcc3  9854  dcomex  9863  axdc2lem  9864  axcclem  9873  zfac  9876  ac3  9878  ackm  9881  axac2  9882  axac  9883  axaci  9884  cardeqv  9885  numth2  9887  numth  9888  dmct  9940  brdom3  9944  fin71ac  9949  cardf  9966  aleph1  9987  cfpwsdom  10000  smobeth  10002  zfcndrep  10030  zfcndpow  10032  zfcndac  10035  gch2  10091  wunex3  10157  tskpr  10186  inar1  10191  rankcf  10193  tskcard  10197  tskuni  10199  grothpw  10242  axgroth4  10248  grothprim  10250  inaprc  10252  dmaddpi  10306  dmmulpi  10307  1lt2pi  10321  addpqf  10360  mulpqf  10362  1lt2nq  10389  supsrlem  10527  ssxr  10704  gtso  10716  subf  10882  negne0i  10955  mulnzcnopr  11280  infrenegsup  11618  nnne0  11665  halflt1  11849  nn0ssz  11997  3halfnz  12055  zeo  12062  numlt  12117  numltc  12118  le9lt10  12119  decle  12126  uzf  12240  xaddf  12611  xsubge0  12648  xmulf  12659  ixxf  12742  ixxssxr  12744  iooval2  12765  ioof  12829  unirnioo  12831  dfioo2  12832  fzval2  12889  fzf  12890  0nelfz1  12920  fz10  12922  fzpreddisj  12950  4fvwrd4  13021  fzof  13029  fzo0  13055  fldiv4p1lem1div2  13199  fldiv4lem1div2  13201  om2uzoi  13317  faclbnd4lem1  13647  hashkf  13686  hashgval  13687  hashinf  13689  hashresfn  13694  hashnn0n0nn  13746  hashbclem  13804  hashge3el3dif  13838  wrdexgOLD  13866  rev0  14120  s2dm  14246  f1oun2prg  14273  trclublem  14349  sqrt2gt1lt2  14628  limsupgord  14823  fclim  14904  fsumrelem  15156  ackbijnn  15177  incexclem  15185  incexc  15186  arisum2  15210  georeclim  15222  geoisumr  15228  0.999...  15231  risefall0lem  15374  ege2le3  15437  sin0  15496  ef01bndlem  15531  cos2bnd  15535  cos01gt0  15538  sincos2sgn  15541  sin4lt0  15542  rpnnen2lem3  15563  rpnnen2lem9  15569  rexpen  15575  cnso  15594  dvdslelem  15653  n2dvds1OLD  15712  divalglem1  15739  divalglem5  15742  divalglem6  15743  divalglem10  15747  flodddiv4  15758  0bits  15782  sadcf  15796  sadcadd  15801  bitsshft  15818  smupf  15821  gcdf  15855  eucalgf  15921  2prm  16030  dfphi2  16105  pockthi  16237  prmrec  16252  vdwapf  16302  vdwlem6  16316  karatsuba  16414  1259lem5  16462  2503lem3  16466  4001lem4  16471  structcnvcnv  16491  structfn  16494  strleun  16585  prdsval  16722  prdsds  16731  imasvscafn  16804  xpsff1o  16834  sscpwex  17079  wunfunc  17163  wunnat  17220  eldmcoa  17319  coapm  17325  catcfuccl  17363  catcxpccl  17451  yonedainv  17525  smndex1bas  18065  smndex1n0mnd  18071  grpinvfvi  18140  mulgfvi  18224  symgsssg  18589  symgfisg  18590  psgnunilem5  18616  sylow3lem2  18747  oppglsm  18761  efgmf  18833  efgval  18837  efgsf  18849  0frgp  18899  dmdprd  19114  dprdval  19119  invrfval  19417  drngui  19502  rmodislmod  19696  lssintcl  19730  mplsubrglem  20213  opsrtoslem2  20259  cnfldfun  20551  cnfld0  20563  cnfld1  20564  cnfldsub  20567  xrsds  20582  psgnghm  20718  zrhpsgnmhm  20722  recrng  20759  ocv1  20817  dsmmbas2  20875  mdetralt  21211  maducoeval2  21243  eltpsi  21546  unitg  21569  fctop  21606  cctop  21608  ppttop  21609  epttop  21611  leordtvallem1  21812  leordtvallem2  21813  iccordt  21816  iscnp2  21841  discmp  22000  conncompcld  22036  1stcrestlem  22054  2ndcdisj  22058  topnlly  22093  disllycmp  22100  dis1stc  22101  txuni2  22167  xkotf  22187  dfac14lem  22219  prdstps  22231  txindis  22236  tx1stc  22252  xkohaus  22255  xkoptsub  22256  cnmpt1st  22270  cnmpt2nd  22271  ptcmpfi  22415  trfil1  22488  fin1aufil  22534  tgpconncompeqg  22714  tgpconncomp  22715  tsmsres  22746  trust  22832  met1stc  23125  dscmet  23176  retopon  23366  cnfldtopon  23385  xrsxmet  23411  xrsmopn  23414  iimulcn  23536  icopnfhmeo  23541  iccpnfhmeo  23543  xrhmeo  23544  cnheiborlem  23552  lebnumii  23564  ishtpy  23570  htpycc  23578  pco1  23613  pcohtpylem  23617  pcopt  23620  pcopt2  23621  pcoass  23622  pcorevlem  23624  cfilresi  23892  rrxcph  23989  rrx0el  23995  ovoliunlem3  24099  ovolicc1  24111  ovolicc2  24117  volf  24124  ioorf  24168  dyadf  24186  dyadmbl  24195  vitalilem5  24207  vitali  24208  mbfimaopnlem  24250  mbflimsup  24261  0plef  24267  i1fima  24273  i1fima2  24274  i1fd  24276  itg1ge0  24281  itg10  24283  i1f1lem  24284  i1fadd  24290  i1fmul  24291  i1fmulc  24298  mbfi1fseqlem5  24314  itg2addlem  24353  reldv  24462  dvbsss  24494  dvef  24571  lhop1lem  24604  deg1fvi  24673  plypf1  24796  coeeulem  24808  coeeu  24809  vieta1lem2  24894  aannenlem3  24913  aalioulem3  24917  dvradcnv  25003  pserulm  25004  pserdvlem2  25010  sinhalfpilem  25043  sincos4thpi  25093  tan4thpi  25094  sincos6thpi  25095  pige3ALT  25099  resinf1o  25114  tanord1  25115  tanregt0  25117  efabl  25128  relogrn  25139  dfrelog  25143  logneg  25165  logltb  25177  logcn  25224  logf1o2  25227  dvlog  25228  efopnlem2  25234  efopn  25235  logccv  25240  dvsqrt  25317  dvcnsqrt  25319  cxpcn3  25323  logblog  25364  angpined  25402  1cubr  25414  asinsin  25464  asin1  25466  reasinsin  25468  atan0  25480  atanbnd  25498  atan1  25500  log2cnv  25516  log2ub  25521  log2le1  25522  birthday  25526  amgmlem  25561  emcllem5  25571  emgt0  25578  harmonicbnd3  25579  ftalem3  25646  basellem4  25655  sgmf  25716  ppi1  25735  cht1  25736  vma1  25737  ppiltx  25748  sqff1o  25753  ppiublem1  25772  ppiublem2  25773  ppiub  25774  chtub  25782  dchreq  25828  bposlem7  25860  bposlem8  25861  bposlem9  25862  lgsdir2lem2  25896  lgsdir2lem3  25897  chebbnd1  26042  chto1ub  26046  chpo1ubb  26051  pntibndlem1  26159  tgldimor  26282  tglnfn  26327  axlowdimlem4  26725  axlowdimlem16  26737  axlowdim  26741  upgrfi  26870  lfgrnloop  26904  lfuhgr1v0e  27030  usgrexmplef  27035  usgrres  27084  vdegp1bi  27313  vtxdginducedm1lem2  27316  pthdlem2  27543  wpthswwlks2on  27734  0ewlk  27887  0pth  27898  konigsbergiedgw  28021  konigsberglem1  28025  konigsberglem2  28026  konigsberglem3  28027  konigsberglem4  28028  konigsberglem5  28029  ex-dif  28196  ex-un  28197  ex-in  28198  ex-fl  28220  avril1  28236  9p10ne21fool  28244  n0lplig  28254  cnidOLD  28353  cnnvm  28453  ipasslem8  28608  ipasslem10  28610  hvsubf  28786  normlem1  28881  normlem6  28886  normlem7  28887  norm-ii-i  28908  norm3adifii  28919  hilid  28932  hlimf  29008  hhssabloi  29033  hhssnv  29035  hhshsslem1  29038  shincli  29133  shsval2i  29158  shs0i  29220  chj0i  29226  chm1i  29227  chincli  29231  chdmm1i  29248  shjshsi  29263  chsup0  29319  h1de2bi  29325  spansnpji  29349  cmcmlem  29362  cmcmii  29368  cmcm2ii  29369  cmcm3ii  29370  pjidmi  29444  pjssmii  29452  pj0i  29464  pjocini  29469  mayetes3i  29500  df0op2  29523  hoaddcomi  29543  hoaddassi  29547  hocadddiri  29550  hocsubdiri  29551  hoaddid1i  29557  ho0coi  29559  hoid1i  29560  hoid1ri  29561  hodseqi  29565  honegsubi  29567  adj1o  29665  hoddii  29760  lnopunilem1  29781  lnopunilem2  29782  nmcopexi  29798  nmcopex  29800  nmcoplb  29801  nmcfnexi  29822  nmcfnex  29824  nmcfnlb  29825  adjbd1o  29856  adjcoi  29871  nmopcoadji  29872  opsqrlem6  29916  pjsdii  29926  pjddii  29927  pjidmcoi  29948  pjtoi  29950  pjin1i  29963  pjclem1  29966  stji1i  30013  reuxfrdf  30249  inindif  30272  iuninc  30306  fnresin  30365  rinvf1o  30369  suppss2f  30378  xppreima  30388  ofoprabco  30403  gtiso  30430  df1stres  30433  df2ndres  30434  snct  30443  padct  30449  fsuppcurry1  30455  fsuppcurry2  30456  ffsrn  30459  fpwrelmapffs  30464  fzodif1  30510  nnindf  30529  nn0min  30531  dp2lt  30556  dp2ltsuc  30557  dp2ltc  30558  dplti  30576  dpmul  30584  dpmul4  30585  ressplusf  30632  xrsclat  30662  xrge0base  30667  xrge00  30668  xrnarchi  30808  xrge0slmod  30912  ccfldsrarelvec  31051  ccfldextdgrr  31052  locfinreflem  31099  locfinref  31100  unicls  31141  sqsscirc1  31146  mhmhmeotmd  31165  rmulccn  31166  raddcn  31167  xrge0iifiso  31173  xrge0iifhmeo  31174  lmxrge0  31190  cnzh  31206  rezh  31207  qqh0  31220  qqh1  31221  qqhre  31256  rrhre  31257  esumnul  31302  esum0  31303  esumsnf  31318  esumpfinvallem  31328  esumpfinvalf  31330  esumpcvgval  31332  esumcvgsum  31342  esumsup  31343  esumcvgre  31345  sigaclfu2  31375  dmsigagen  31398  ldgenpisyslem1  31417  ddemeas  31490  imambfm  31515  mbfmvolf  31519  br2base  31522  omssubadd  31553  sibfof  31593  sitg0  31599  eulerpartlemt  31624  eulerpartgbij  31625  0rrv  31704  coinfliplem  31731  coinflipprob  31732  coinfliprv  31735  ballotlem2  31741  ballotlem4  31751  ballotlem5  31752  ballotlemi1  31755  ballotlem7  31788  ballotth  31790  signsplypnf  31815  signsply0  31816  signsw0g  31821  signswch  31826  signsvf0  31845  hashreprin  31886  reprfz1  31890  chtvalz  31895  hgt750lemd  31914  hgt750lem  31917  hgt750lem2  31918  bnj521  32002  bnj1098  32050  bnj1109  32053  bnj1131  32054  bnj1533  32119  bnj151  32144  bnj580  32180  bnj852  32188  bnj864  32189  bnj865  32190  bnj978  32216  bnj1021  32233  bnj907  32234  bnj1093  32247  bnj1145  32260  bnj1172  32268  bnj1174  32270  bnj1176  32272  bnj1186  32274  subfacf  32417  subfacp1lem1  32421  subfacp1lem5  32426  subfacp1lem6  32427  subfacval3  32431  erdszelem2  32434  kur14lem4  32451  ioosconn  32489  iccllysconn  32492  satfn  32597  fmlaomn0  32632  gonan0  32634  goaln0  32635  elnanelprv  32671  msrfo  32788  mthmpps  32824  problem5  32907  quad3  32908  circum  32912  axextprim  32922  axrepprim  32923  axunprim  32924  axinfprim  32927  axacprim  32928  logi  32961  bcneg1  32963  setinds  33018  dfon2lem2  33024  dfon2lem4  33026  axextdfeq  33037  poseq  33090  frrlem4  33121  nosgnn0  33160  sltsolem1  33175  bdayfo  33177  nolt02o  33194  noetalem3  33214  fobigcup  33356  snelsingles  33378  fullfunfnv  33402  fullfunfv  33403  rankaltopb  33435  rank0  33626  rankeq1o  33627  hfuni  33640  fneer  33696  neibastop1  33702  nabi1i  33737  nabi2i  33738  limsucncmpi  33788  knoppcnlem8  33834  knoppcnlem11  33837  cnndvlem1  33871  bj-consensusALT  33907  bj-dtru  34134  bj-sbidmOLD  34169  bj-n0i  34257  bj-snsetex  34270  bj-tagss  34287  bj-2upln0  34330  bj-2upln1upl  34331  bj-nuliota  34344  bj-0int  34387  bj-elid5  34455  bj-inftyexpitaufo  34478  bj-pinftyccb  34497  bj-minftyccb  34501  bj-pinftynminfty  34503  f1omptsnlem  34611  mptsnunlem  34613  topdifinffinlem  34622  relowlpssretop  34639  1oequni2o  34643  pibt2  34692  imadifss  34861  tan2h  34878  poimirlem3  34889  poimirlem9  34895  poimirlem16  34902  poimirlem17  34903  poimirlem18  34904  poimirlem19  34905  poimirlem20  34906  poimirlem22  34908  poimirlem30  34916  mblfinlem1  34923  mblfinlem2  34924  ovoliunnfl  34928  voliunnfl  34930  itg2addnclem  34937  itg2addnclem2  34938  asindmre  34971  areacirclem1  34976  fdc  35014  cntotbnd  35068  heiborlem6  35088  rrnval  35099  reheibor  35111  rngosn3  35196  ineqcomi  35499  brcnvrabga  35593  cnvresrn  35599  moantr  35610  inxp2  35613  dfxrn2  35622  cnvcosseq  35676  refrelcosslem  35696  1cosscnvxrn  35709  redundss3  35857  refrelsredund3  35863  refrelredund3  35866  prter2  36011  renegclALT  36093  mapdunirnN  38780  sn-dtru  39104  sqdeccom12  39168  resubf  39204  sn-0ne2  39229  sn-0lt1  39239  dffltz  39264  rntrclfvOAI  39281  diophrw  39349  rabren3dioph  39405  pellexlem6  39424  pellex  39425  frmx  39503  frmy  39504  jm2.23  39586  jm2.27dlem3  39601  axac10  39623  pw2f1ocnv  39627  kelac2lem  39657  lmhmlnmsplit  39680  pwfi2f1o  39689  frlmpwfi  39691  ifpbiidcor  39833  alephiso2  39910  alephiso3  39911  cnvnonrel  39941  rnnonrel  39944  resnonrel  39945  cononrel1  39947  cononrel2  39948  fvnonrel  39950  cnvcnvintabd  39953  cnvintabd  39956  rclexi  39968  rtrclex  39970  clcnvlem  39976  cnvrcl0  39978  dmtrcl  39980  rntrcl  39981  dfrtrcl5  39982  iunrelexp0  40040  dmtrclfvRP  40068  rntrclfv  40070  corcltrcl  40077  cotrclrcl  40080  0heALT  40122  frege54cor1a  40203  dssmapnvod  40359  uneqsn  40366  clsk3nimkb  40383  gneispace  40477  int-sqdefd  40527  int-sqgeq0d  40532  rr-groth  40628  rr-grothprim  40629  seff  40634  expgrowthi  40658  expgrowth  40660  binomcxplemnotnn0  40681  ee233  40846  ax6e2nd  40885  in1  40898  dfvd2ani  40910  dfvd2i  40912  dfvd3i  40919  dfvd3ani  40922  e0bi  41103  uun2221  41140  uun2221p1  41141  uun2221p2  41142  en3lpVD  41172  relopabVD  41228  ax6e2ndVD  41235  ax6e2ndALT  41257  pssnssi  41360  nnf1oxpnn  41450  icof  41475  negpilt0  41539  xrgtso  41606  supxrleubrnmptf  41720  xrpnf  41755  ioontr  41780  iccdifioo  41784  iccdifprioo  41785  uzinico2  41831  fsummulc1f  41844  fsumiunss  41849  fnlimfvre2  41951  limsupreuz  42011  limsupvaluz2  42012  limsup10ex  42047  icccncfext  42163  dvcosre  42189  dvsinax  42190  ioodvbdlimc1lem2  42210  ioodvbdlimc2lem  42212  dvmptmulf  42215  dvnmul  42221  dvmptfprodlem  42222  dvnprodlem2  42225  stoweidlem1  42280  stoweidlem26  42305  stoweidlem34  42313  stoweidlem44  42323  stoweid  42342  stirlinglem5  42357  dirkercncflem1  42382  fourierdlem44  42430  fourierdlem56  42441  fourierdlem62  42447  fourierdlem89  42474  fourierdlem91  42476  fourierdlem100  42485  fourierdlem102  42487  fourierdlem103  42488  fourierdlem104  42489  fourierdlem108  42493  fourierdlem112  42497  fourierdlem114  42499  fouriersw  42510  rrndistlt  42569  gsumge0cl  42647  sge0tsms  42656  sge0ltfirpmpt2  42702  ovn0  42842  hoidmv1le  42870  hoidmvle  42876  ovnsubadd2lem  42921  ovolval4lem1  42925  vonioolem2  42957  smflimlem3  43043  nsssmfmbf  43049  axorbtnotaiffb  43133  axorbciffatcxorb  43135  abnotbtaxb  43145  euabsneu  43257  sprval  43635  fmtnoinf  43692  1nevenALTV  43850  nfermltl8rev  43901  nfermltl2rev  43902  nnsum3primes4  43947  tgblthelfgott  43974  tgoldbachlt  43975  ldepslinc  44558  rrx2plordso  44705  alimp-no-surprise  44876  aacllem  44896  amgmwlem  44897  amgmlemALT  44898