Theorem mpbi 220

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 206	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  pm5.74i  260  notbii  310  pm5.19  375  ori  390  imori  429  pm4.71i  664  pm4.71ri  665  pm5.32i  669  pm3.24  926  pm5.16  934  biluk  974  4exmidOLD  998  dn1  1008  3ori  1388  cadan  1548  nic-dfim  1594  nic-dfneg  1595  nic-mp  1596  nic-mpALT  1597  tbw-negdf  1624  rb-imdf  1675  nfri  1715  mpgbi  1725  19.35i  1806  19.36iv  1905  19.37iv  1911  nfim1  2067  19.36i  2099  ax6  2251  sbie  2408  axi12  2600  bm1.1  2607  eqcomi  2631  eqtri  2644  eleqtri  2699  neii  2796  necomi  2848  neeqtri  2866  neli  2899  nrex  3000  rexlimi  3024  rexlimiv  3027  isseti  3209  vtocl2  3261  vtocl3  3262  eueq1  3379  euxfr2  3391  cdeqri  3421  sseqtri  3637  3sstr3i  3643  pssn2lp  3708  equncomi  3759  unssi  3788  ssini  3836  unabs  3854  inabs  3855  dfin4  3867  difid  3948  ab0orv  3953  npss0OLD  4015  disjdif  4040  difin0  4041  snid  4208  rabrsn  4259  iinrab2  4583  symdifv  4598  rintn0  4619  breqtri  4678  axsep  4780  bm1.3ii  4784  ax6vsep  4785  zfnuleu  4786  notzfaus  4840  zfpow  4844  dtru  4857  reusv2lem4  4872  reuxfr2d  4891  dtruALT  4899  dtruALT2  4911  op1stb  4940  copsexg  4956  uniop  4977  pwundif  5021  rn0  5377  dmresi  5457  issref  5509  somincom  5530  cnvcnv  5586  cnvcnvOLD  5587  rescnvcnv  5597  cnvcnvres  5598  cnvsn  5618  cocnvcnv2  5647  cores2  5648  co01  5650  cnviin  5672  onunisuci  5841  iota4an  5870  fnopab  6018  mpt0  6021  fnmpti  6022  f1cnvcnv  6109  f1ovi  6175  eliman0  6223  fvco4i  6276  fmpti  6383  fvsnun2  6449  funiunfv  6506  oprabss  6746  relmptopab  6883  zfun  6950  tfinds2  7063  omon  7076  2nd0  7175  f1stres  7190  f2ndres  7191  relmpt2opab  7259  df1st2  7263  df2nd2  7264  fsplit  7282  reldmtpos  7360  dftpos4  7371  tpostpos  7372  tpos0  7382  wfrlem4  7418  smo0  7455  tfrlem14  7487  tfrlem16  7489  rdgsucg  7519  rdglimg  7521  frfnom  7530  oawordeulem  7634  uniixp  7931  dfdom2  7981  ssdomg  8001  xpcomf1o  8049  sbthlem5  8074  pwdom  8112  limensuci  8136  fiint  8237  fidomdm  8243  residfi  8247  pwfilem  8260  mptfi  8265  fisn  8333  dffi3  8337  ordtypelem6  8428  ordtypelem7  8429  wemaplem2  8452  wdompwdom  8483  harwdom  8495  suc11reg  8516  zfinf  8536  axinf2  8537  noinfep  8557  cantnfvalf  8562  cantnflt  8569  cantnf0  8572  cantnf  8590  tz9.1c  8606  tc2  8618  r111  8638  r1tr2  8640  r1ordg  8641  r1sssuc  8646  r1val1  8649  tz9.13  8654  r1elssi  8668  pwwf  8670  rankopb  8715  rankeq0b  8723  ranksuc  8728  rankmapu  8741  rankxplim  8742  rankxplim3  8744  rankxpsuc  8745  cp  8754  karden  8758  card0  8784  cardlim  8798  cardom  8812  infxpenlem  8836  alephsuc2  8903  alephgeom  8905  unialeph  8924  dfac4  8945  dfacacn  8963  cda1dif  8998  pm110.643  8999  infcda1  9015  ackbij1lem13  9054  ackbij2  9065  cf0  9073  cfsuc  9079  cfom  9086  cfslb2n  9090  ominf4  9134  fin23lem17  9160  fin23lem28  9162  fin23lem30  9164  fin23lem31  9165  fin23lem40  9173  isfin1-3  9208  dfacfin7  9221  fin1a2lem6  9227  itunitc1  9242  axcc3  9260  dcomex  9269  axdc2lem  9270  axcclem  9279  zfac  9282  ac3  9284  ackm  9287  axac2  9288  axac  9289  axaci  9290  cardeqv  9291  numth2  9293  numth  9294  dmct  9346  brdom3  9350  fin71ac  9355  cardf  9372  aleph1  9393  cfpwsdom  9406  smobeth  9408  zfcndrep  9436  zfcndpow  9438  zfcndac  9441  gch2  9497  wunex3  9563  tskpr  9592  inar1  9597  rankcf  9599  tskcard  9603  tskuni  9605  grothpw  9648  axgroth4  9654  grothprim  9656  inaprc  9658  dmaddpi  9712  dmmulpi  9713  1lt2pi  9727  addpqf  9766  mulpqf  9768  1lt2nq  9795  supsrlem  9932  ssxr  10107  gtso  10119  subf  10283  negne0i  10356  mulnzcnopr  10673  infrenegsup  11006  halflt1  11250  nn0ssz  11398  3halfnz  11456  zeo  11463  numlt  11527  numltc  11528  le9lt10  11529  decle  11540  decleOLD  11543  declecOLD  11544  uzf  11690  zgt1rpn0n1  11871  xaddf  12055  xsubge0  12091  xmulf  12102  ixxf  12185  ixxssxr  12187  iooval2  12208  ioof  12271  unirnioo  12273  dfioo2  12274  xrge0neqmnf  12276  fzval2  12329  fzf  12330  0nelfz1  12360  fz10  12362  fzpreddisj  12390  4fvwrd4  12459  fzof  12467  fzo0  12492  fldiv4p1lem1div2  12636  fldiv4lem1div2  12638  om2uzoi  12754  faclbnd4lem1  13080  hashkf  13119  hashgval  13120  hashinf  13122  hashresfn  13128  hashnn0n0nn  13180  hashbclem  13236  hashge3el3dif  13268  wrdexg  13315  rev0  13513  f1oun2prg  13662  trclublem  13734  sqrt2gt1lt2  14015  limsupgord  14203  fclim  14284  fsumrelem  14539  ackbijnn  14560  incexclem  14568  incexc  14569  arisum2  14593  georeclim  14603  geoisumr  14609  0.999...  14612  0.999...OLD  14613  geoihalfsum  14614  risefall0lem  14757  ege2le3  14820  sin0  14879  ef01bndlem  14914  cos2bnd  14918  cos01gt0  14921  sincos2sgn  14924  sin4lt0  14925  rpnnen2lem3  14945  rpnnen2lem9  14951  rexpen  14957  cnso  14976  dvdslelem  15031  n2dvds1  15104  divalglem1  15117  divalglem5  15120  divalglem6  15121  divalglem10  15125  flodddiv4  15137  0bits  15161  sadcf  15175  sadcadd  15180  bitsshft  15197  smupf  15200  gcdf  15234  eucalgf  15296  2prm  15405  dfphi2  15479  pockthi  15611  prmrec  15626  vdwapf  15676  vdwap0  15680  vdwlem6  15690  karatsuba  15792  karatsubaOLD  15793  1259lem5  15842  2503lem3  15846  4001lem4  15851  structcnvcnv  15871  structfn  15874  strlemor1OLD  15969  strleun  15972  prdsval  16115  prdsds  16124  imasvscafn  16197  xpsc0  16220  xpsc1  16221  xpsff1o  16228  sscpwex  16475  wunfunc  16559  wunnat  16616  eldmcoa  16715  coapm  16721  catcfuccl  16759  catcxpccl  16847  yonedainv  16921  plusffval  17247  grpinvfvi  17463  mulgfvi  17545  symgsssg  17887  symgfisg  17888  psgnunilem5  17914  sylow3lem2  18043  oppglsm  18057  efgmf  18126  efgval  18130  efgsf  18142  0frgp  18192  dmdprd  18397  dprdval  18402  invrfval  18673  drngui  18753  scaffval  18881  rmodislmod  18931  lssintcl  18964  mplsubrglem  19439  opsrtoslem2  19485  cnfldfun  19758  cnfld0  19770  cnfld1  19771  cnfldsub  19774  xrsds  19789  psgnghm  19926  zrhpsgnmhm  19930  recrng  19967  ipffval  19993  ocv1  20023  dsmmbas2  20081  mdetralt  20414  maducoeval2  20446  eltpsi  20748  unitg  20771  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  leordtvallem1  21014  leordtvallem2  21015  iccordt  21018  iscnp2  21043  discmp  21201  conncompcld  21237  1stcrestlem  21255  2ndcdisj  21259  topnlly  21294  disllycmp  21301  dis1stc  21302  txuni2  21368  xkotf  21388  dfac14lem  21420  prdstps  21432  txindis  21437  tx1stc  21453  xkohaus  21456  xkoptsub  21457  cnmpt1st  21471  cnmpt2nd  21472  ptcmpfi  21616  trfil1  21690  fin1aufil  21736  tgpconncompeqg  21915  tgpconncomp  21916  tsmsres  21947  trust  22033  met1stc  22326  dscmet  22377  retopon  22567  cnfldtopon  22586  xrsxmet  22612  xrsmopn  22615  iimulcn  22737  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  cnheiborlem  22753  lebnumii  22765  ishtpy  22771  htpycc  22779  pco1  22815  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  cfilresi  23093  rrxcph  23180  ovoliunlem3  23272  ovolicc1  23284  ovolicc2  23290  volf  23297  ioorf  23341  dyadf  23359  dyadmbl  23368  vitalilem5  23381  vitali  23382  mbfimaopnlem  23422  mbflimsup  23433  0plef  23439  i1fima  23445  i1fima2  23446  i1fd  23448  itg1ge0  23453  itg10  23455  i1f1lem  23456  i1fadd  23462  i1fmul  23463  i1fmulc  23470  mbfi1fseqlem5  23486  itg2addlem  23525  reldv  23634  dvbsss  23666  dvef  23743  lhop1lem  23776  deg1fvi  23845  plypf1  23968  coeeulem  23980  coeeu  23981  vieta1lem2  24066  aannenlem3  24085  aalioulem3  24089  dvradcnv  24175  pserulm  24176  pserdvlem2  24182  abelthlem6  24190  sinhalfpilem  24215  sincos4thpi  24265  tan4thpi  24266  sincos6thpi  24267  pige3  24269  resinf1o  24282  tanord1  24283  tanregt0  24285  efabl  24296  relogrn  24308  dfrelog  24312  logneg  24334  logltb  24346  logcn  24393  logf1o2  24396  dvlog  24397  efopnlem2  24403  efopn  24404  logccv  24409  dvsqrt  24483  dvcnsqrt  24485  cxpcn3  24489  logblog  24530  angpined  24557  1cubr  24569  asinsin  24619  asin1  24621  reasinsin  24623  atan0  24635  atanbnd  24653  atan1  24655  log2cnv  24671  log2ub  24676  log2le1  24677  birthday  24681  amgmlem  24716  emcllem5  24726  emgt0  24733  harmonicbnd3  24734  ftalem3  24801  basellem4  24810  sgmf  24871  ppi1  24890  cht1  24891  vma1  24892  ppiltx  24903  sqff1o  24908  ppiublem1  24927  ppiublem2  24928  ppiub  24929  chtub  24937  dchreq  24983  bposlem7  25015  bposlem8  25016  bposlem9  25017  lgsdir2lem2  25051  lgsdir2lem3  25052  chebbnd1  25161  chto1ub  25165  chpo1ubb  25170  pntibndlem1  25278  tgldimor  25397  tglnfn  25442  axlowdimlem4  25825  axlowdimlem16  25837  axlowdim  25841  upgrfi  25986  lfgrnloop  26020  lfuhgr1v0e  26146  usgrexmplef  26151  usgrres  26200  vdegp1bi  26433  vtxdginducedm1lem2  26436  pthdlem2  26664  0ewlk  26975  0pth  26986  konigsbergiedgw  27108  konigsbergiedgwOLD  27109  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  konigsberglem4  27117  konigsberglem5  27118  ex-dif  27280  ex-un  27281  ex-in  27282  ex-fl  27304  avril1  27319  n0lplig  27335  vcex  27433  cnidOLD  27437  cnnvm  27537  ipasslem8  27692  ipasslem10  27694  hvsubf  27872  normlem1  27967  normlem6  27972  normlem7  27973  norm-ii-i  27994  norm3adifii  28005  hilid  28018  hlimf  28094  hhssabloi  28119  hhssnv  28121  hhshsslem1  28124  shincli  28221  shsval2i  28246  shs0i  28308  chj0i  28314  chm1i  28315  chincli  28319  chdmm1i  28336  shjshsi  28351  chsup0  28407  h1de2bi  28413  spansnpji  28437  cmcmlem  28450  cmcmii  28456  cmcm2ii  28457  cmcm3ii  28458  pjidmi  28532  pjssmii  28540  pj0i  28552  pjocini  28557  mayetes3i  28588  df0op2  28611  hoaddcomi  28631  hoaddassi  28635  hocadddiri  28638  hocsubdiri  28639  hoaddid1i  28645  ho0coi  28647  hoid1i  28648  hoid1ri  28649  hodseqi  28653  honegsubi  28655  adj1o  28753  hoddii  28848  lnopunilem1  28869  lnopunilem2  28870  nmcopexi  28886  nmcopex  28888  nmcoplb  28889  nmcfnexi  28910  nmcfnex  28912  nmcfnlb  28913  adjbd1o  28944  adjcoi  28959  nmopcoadji  28960  opsqrlem6  29004  pjsdii  29014  pjddii  29015  pjidmcoi  29036  pjtoi  29038  pjin1i  29051  pjclem1  29054  stji1i  29101  reuxfr3d  29329  inindif  29353  iuninc  29379  fnresin  29430  rinvf1o  29432  suppss2f  29439  xppreima  29449  ofoprabco  29464  funcnvmptOLD  29467  gtiso  29478  df1stres  29481  df2ndres  29482  snct  29491  padct  29497  ffsrn  29504  fpwrelmapffs  29509  nnindf  29565  nn0min  29567  dp2lt  29592  dp2ltsuc  29593  dp2ltc  29594  dplti  29613  dpmul  29621  dpmul4  29622  ressplusf  29650  xrsclat  29680  xrge0base  29685  xrge00  29686  xrnarchi  29738  xrge0slmod  29844  locfinreflem  29907  locfinref  29908  unicls  29949  sqsscirc1  29954  mhmhmeotmd  29973  rmulccn  29974  raddcn  29975  xrge0iifiso  29981  xrge0iifhmeo  29982  lmxrge0  29998  cnzh  30014  rezh  30015  qqh0  30028  qqh1  30029  qqhre  30064  rrhre  30065  esumnul  30110  esum0  30111  esumsnf  30126  esumpfinvallem  30136  esumpfinvalf  30138  esumpcvgval  30140  esumcvgsum  30150  esumsup  30151  esumcvgre  30153  sigaclfu2  30184  dmsigagen  30207  ldgenpisyslem1  30226  ddemeas  30299  imambfm  30324  mbfmvolf  30328  br2base  30331  omssubadd  30362  sibfof  30402  sitg0  30408  eulerpartlemt  30433  eulerpartgbij  30434  0rrv  30513  coinfliplem  30540  coinflipprob  30541  coinfliprv  30544  ballotlem2  30550  ballotlem4  30560  ballotlem5  30561  ballotlemi1  30564  ballotlem7  30597  ballotth  30599  signsplypnf  30627  signsply0  30628  signsw0g  30633  signswch  30638  signsvf0  30657  hashreprin  30698  reprfz1  30702  chtvalz  30707  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  bnj521  30805  bnj1098  30854  bnj1109  30857  bnj1131  30858  bnj1533  30922  bnj151  30947  bnj580  30983  bnj852  30991  bnj864  30992  bnj865  30993  bnj978  31019  bnj1021  31034  bnj907  31035  bnj1093  31048  bnj1145  31061  bnj1172  31069  bnj1174  31071  bnj1176  31073  bnj1186  31075  subfacf  31157  subfacp1lem1  31161  subfacp1lem5  31166  subfacp1lem6  31167  subfacval3  31171  erdszelem2  31174  kur14lem4  31191  ioosconn  31229  iccllysconn  31232  msrfo  31443  mthmpps  31479  problem5  31563  quad3  31564  circum  31568  axextprim  31578  axrepprim  31579  axunprim  31580  axinfprim  31583  axacprim  31584  inffzOLD  31615  logi  31620  bcneg1  31622  setinds  31683  dfon2lem2  31689  dfon2lem4  31691  axextdfeq  31703  poseq  31750  frrlem4  31783  nosgnn0  31811  sltsolem1  31826  bdayfo  31828  nolt02o  31845  noetalem3  31865  dmscut  31918  fobigcup  32007  snelsingles  32029  fullfunfnv  32053  fullfunfv  32054  rankaltopb  32086  rank0  32277  rankeq1o  32278  hfuni  32291  fneer  32348  neibastop1  32354  nabi1i  32391  nabi2i  32392  limsucncmpi  32444  knoppcnlem8  32490  knoppcnlem11  32493  cnndvlem1  32528  bj-consensusALT  32563  bj-axsep  32793  bj-zfpow  32795  bj-dtru  32797  bj-sbidmOLD  32831  bj-n0i  32935  bj-snsetex  32951  bj-tagss  32968  bj-2upln0  33011  bj-2upln1upl  33012  bj-nuliota  33019  bj-0int  33055  bj-elid  33085  bj-pinftyccb  33108  bj-minftyccb  33112  bj-pinftynminfty  33114  f1omptsnlem  33183  mptsnunlem  33185  topdifinffinlem  33195  relowlpssretop  33212  1oequni2o  33216  imadifss  33384  tan2h  33401  poimirlem3  33412  poimirlem9  33418  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem30  33439  mblfinlem1  33446  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  itg2addnclem  33461  itg2addnclem2  33462  asindmre  33495  areacirclem1  33500  fdc  33541  cntotbnd  33595  heiborlem6  33615  rrnval  33626  reheibor  33638  rngosn3  33723  ineqcomi  34006  cnvresrn  34116  motr  34127  inxp2  34129  prter2  34166  renegclALT  34249  mapdunirnN  36939  rntrclfvOAI  37254  diophrw  37322  rabren3dioph  37379  pellexlem6  37398  pellex  37399  frmx  37478  frmy  37479  jm2.23  37563  jm2.27dlem3  37578  axac10  37600  pw2f1ocnv  37604  kelac2lem  37634  lmhmlnmsplit  37657  pwfi2f1o  37666  frlmpwfi  37668  ifpbiidcor  37819  cnvnonrel  37894  rnnonrel  37897  resnonrel  37898  cononrel1  37900  cononrel2  37901  fvnonrel  37903  cnvcnvintabd  37906  cnvintabd  37909  rclexi  37922  rtrclex  37924  clcnvlem  37930  cnvrcl0  37932  dmtrcl  37934  rntrcl  37935  dfrtrcl5  37936  iunrelexp0  37994  dmtrclfvRP  38022  rntrclfv  38024  corcltrcl  38031  cotrclrcl  38034  0heALT  38077  frege54cor1a  38158  dssmapnvod  38314  uneqsn  38321  clsk3nimkb  38338  gneispace  38432  int-sqdefd  38484  int-sqgeq0d  38489  seff  38508  expgrowthi  38532  expgrowth  38534  binomcxplemnotnn0  38555  ee233  38725  ax6e2nd  38774  in1  38787  dfvd2ani  38799  dfvd2i  38801  dfvd3i  38808  dfvd3ani  38811  e0bi  39003  uun2221  39040  uun2221p1  39041  uun2221p2  39042  en3lpVD  39080  relopabVD  39137  ax6e2ndVD  39144  ax6e2ndALT  39166  pssnssi  39283  nnf1oxpnn  39384  icof  39411  negpilt0  39492  xrgtso  39561  supxrleubrnmptf  39680  ioontr  39736  iccdifioo  39741  iccdifprioo  39742  uzinico2  39789  fsummulc1f  39802  fsumiunss  39807  fnlimfvre2  39909  limsupreuz  39969  limsupvaluz2  39970  limsup10ex  40005  icccncfext  40100  dvcosre  40126  dvsinax  40127  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvmptmulf  40152  dvnmul  40158  dvmptfprodlem  40159  dvnprodlem2  40162  stoweidlem1  40218  stoweidlem26  40243  stoweidlem34  40251  stoweidlem44  40261  stoweid  40280  stirlinglem5  40295  dirkercncflem1  40320  fourierdlem44  40368  fourierdlem56  40379  fourierdlem62  40385  fourierdlem89  40412  fourierdlem91  40414  fourierdlem100  40423  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem108  40431  fourierdlem112  40435  fourierdlem114  40437  fouriersw  40448  rrndistlt  40510  gsumge0cl  40588  sge0tsms  40597  sge0ltfirpmpt2  40643  ovn0  40780  hoidmv1le  40808  hoidmvle  40814  ovnsubadd2lem  40859  ovolval4lem1  40863  vonioolem2  40895  smflimlem3  40981  nsssmfmbf  40987  axorbtnotaiffb  41070  axorbciffatcxorb  41072  abnotbtaxb  41082  fmtnoinf  41448  1nevenALTV  41602  nnsum3primes4  41676  tgblthelfgott  41703  tgoldbachlt  41704  tgblthelfgottOLD  41709  tgoldbachltOLD  41710  sprval  41729  ldepslinc  42298  alimp-no-surprise  42527  aacllem  42547  amgmwlem  42548  amgmlemALT  42549