Theorem mpbi 233

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  pm5.74i  274  notbii  323  biluk  390  pm5.19  391  pm3.24  406  dfbi  479  pm4.71i  563  pm5.32i  578  biadani  819  biadanii  821  imori  851  ori  858  pm5.16  1011  dn1  1053  3ori  1421  cadan  1611  nic-dfim  1671  nic-dfneg  1672  nic-mp  1673  nic-mpALT  1674  tbw-negdf  1701  rb-imdf  1752  nfri  1791  mpgbi  1800  19.35i  1879  nfim1  2197  19.36i  2231  ax6  2391  sbie  2521  sbieALT  2589  datisi  2742  disamis  2743  dimatis  2750  fresison  2751  bamalip  2754  axi12  2768  eqcomi  2807  eqtri  2821  eleqtri  2888  nfnfc  2967  neii  2989  necomi  3041  neeqtri  3059  neli  3093  nrex  3228  rexlimiv  3239  rexlimi  3274  issetiOLD  3456  vtocl2OLD  3510  eueqi  3648  euxfr2w  3659  euxfr2  3661  reuxfrd  3687  cdeqri  3705  sseqtri  3951  3sstr3i  3957  pssn2lp  4029  equncomi  4082  unssi  4112  ssini  4158  unabs  4181  inabs  4182  dfin4  4194  difid  4284  ab0orv  4289  disjdif  4379  difin0  4380  pwundif  4523  snid  4561  rabrsn  4620  iinrab2  4955  symdifv  4971  rintn0  4994  breqtri  5055  axsepgfromrep  5165  bm1.3ii  5170  ax6vsep  5171  notzfaus  5227  notzfausOLD  5228  zfpow  5232  dtru  5236  dtruALT  5254  reusv2lem4  5267  dtruALT2  5301  op1stb  5328  copsexgw  5346  copsexg  5347  uniop  5370  pwundifOLD  5422  rn0  5760  dmresi  5888  somincom  5961  cnvcnv  6016  elid  6023  rescnvcnv  6028  cnvcnvres  6029  cocnvcnv2  6078  cores2  6079  co01  6081  cnviin  6105  onunisuci  6272  iota4an  6306  fnopab  6458  mpt0  6462  fnmpti  6463  f1cnvcnv  6559  f1ovi  6628  eliman0  6680  fvco4i  6739  fmpti  6853  funiunfv  6985  oprabss  7239  relmptopab  7375  zfun  7442  tfinds2  7558  omon  7571  2nd0  7678  f1stres  7695  f2ndres  7696  cnvoprab  7740  relmpoopab  7772  df1st2  7776  df2nd2  7777  fsplit  7795  fsplitOLD  7796  reldmtpos  7883  dftpos4  7894  tpostpos  7895  tpos0  7905  wfrlem4  7941  smo0  7978  tfrlem14  8010  tfrlem16  8012  rdgsucg  8042  rdglimg  8044  frfnom  8053  oawordeulem  8163  uniixp  8468  dfdom2  8518  ssdomg  8538  xpcomf1o  8589  sbthlem5  8615  limensuci  8677  fiint  8779  fidomdm  8785  residfi  8789  pwfilem  8802  mptfi  8807  fisn  8875  dffi3  8879  ordtypelem6  8971  ordtypelem7  8972  wemaplem2  8995  harwdom  9039  suc11reg  9066  zfinf  9086  axinf2  9087  noinfep  9107  cantnfvalf  9112  cantnflt  9119  cantnf0  9122  cantnf  9140  tz9.1c  9156  tc2  9168  r111  9188  r1tr2  9190  r1ordg  9191  r1sssuc  9196  r1val1  9199  tz9.13  9204  r1elssi  9218  pwwf  9220  rankopb  9265  rankeq0b  9273  ranksuc  9278  rankmapu  9291  rankxplim3  9294  rankxpsuc  9295  cp  9304  karden  9308  card0  9371  cardlim  9385  cardom  9399  infxpenlem  9424  alephsuc2  9491  alephgeom  9493  unialeph  9512  dfac4  9533  dfacacn  9552  dju1dif  9583  dju1p1e2  9584  infdju1  9600  ackbij1lem13  9643  ackbij2  9654  cf0  9662  cfsuc  9668  cfom  9675  cfslb2n  9679  ominf4  9723  fin23lem17  9749  fin23lem28  9751  fin23lem30  9753  fin23lem31  9754  fin23lem40  9762  isfin1-3  9797  dfacfin7  9810  fin1a2lem6  9816  itunitc1  9831  axcc3  9849  dcomex  9858  axdc2lem  9859  axcclem  9868  zfac  9871  ac3  9873  ackm  9876  axac2  9877  axac  9878  axaci  9879  cardeqv  9880  numth2  9882  numth  9883  dmct  9935  brdom3  9939  fin71ac  9944  cardf  9961  aleph1  9982  cfpwsdom  9995  smobeth  9997  zfcndrep  10025  zfcndpow  10027  zfcndac  10030  gch2  10086  wunex3  10152  tskpr  10181  inar1  10186  rankcf  10188  tskcard  10192  tskuni  10194  grothpw  10237  axgroth4  10243  grothprim  10245  inaprc  10247  dmaddpi  10301  dmmulpi  10302  1lt2pi  10316  addpqf  10355  mulpqf  10357  1lt2nq  10384  supsrlem  10522  ssxr  10699  gtso  10711  subf  10877  negne0i  10950  mulnzcnopr  11275  infrenegsup  11611  nnne0  11659  halflt1  11843  nn0ssz  11991  3halfnz  12049  zeo  12056  numlt  12111  numltc  12112  le9lt10  12113  decle  12120  uzf  12234  xaddf  12605  xsubge0  12642  xmulf  12653  ixxf  12736  ixxssxr  12738  iooval2  12759  ioof  12825  unirnioo  12827  dfioo2  12828  fzval2  12888  fzf  12889  0nelfz1  12921  fz10  12923  fzpreddisj  12951  4fvwrd4  13022  fzof  13030  fzo0  13056  fldiv4p1lem1div2  13200  fldiv4lem1div2  13202  om2uzoi  13318  faclbnd4lem1  13649  hashkf  13688  hashgval  13689  hashinf  13691  hashresfn  13696  hashnn0n0nn  13748  hashge3el3dif  13840  rev0  14117  s2dm  14243  f1oun2prg  14270  trclublem  14346  sqrt2gt1lt2  14626  limsupgord  14821  fclim  14902  fsumrelem  15154  ackbijnn  15175  incexclem  15183  incexc  15184  arisum2  15208  georeclim  15220  geoisumr  15226  0.999...  15229  risefall0lem  15372  ege2le3  15435  sin0  15494  ef01bndlem  15529  cos2bnd  15533  cos01gt0  15536  sincos2sgn  15539  sin4lt0  15540  rpnnen2lem3  15561  rpnnen2lem9  15567  rexpen  15573  cnso  15592  dvdslelem  15651  divalglem1  15735  divalglem5  15738  divalglem6  15739  divalglem10  15743  flodddiv4  15754  0bits  15778  sadcf  15792  sadcadd  15797  bitsshft  15814  smupf  15817  gcdf  15851  eucalgf  15917  2prm  16026  dfphi2  16101  pockthi  16233  prmrec  16248  vdwapf  16298  vdwlem6  16312  karatsuba  16410  1259lem5  16460  2503lem3  16464  4001lem4  16469  structcnvcnv  16489  structfn  16492  strleun  16583  prdsval  16720  imasvscafn  16802  xpsff1o  16832  wunnat  17218  eldmcoa  17317  coapm  17323  catcfuccl  17361  catcxpccl  17449  yonedainv  17523  smndex1bas  18063  smndex1n0mnd  18069  grpinvfvi  18138  mulgfvi  18222  symgsssg  18587  symgfisg  18588  psgnunilem5  18614  sylow3lem2  18745  oppglsm  18759  efgmf  18831  efgval  18835  efgsf  18847  0frgp  18897  dmdprd  19113  dprdval  19118  invrfval  19419  drngui  19501  rmodislmod  19695  lssintcl  19729  cnfldfun  20103  cnfld0  20115  cnfld1  20116  cnfldsub  20119  xrsds  20134  psgnghm  20269  zrhpsgnmhm  20273  recrng  20310  ocv1  20368  dsmmbas2  20426  mplsubrglem  20677  opsrtoslem2  20724  mdetralt  21213  maducoeval2  21245  eltpsi  21549  unitg  21572  fctop  21609  cctop  21611  ppttop  21612  epttop  21614  leordtvallem1  21815  leordtvallem2  21816  iccordt  21819  iscnp2  21844  discmp  22003  conncompcld  22039  1stcrestlem  22057  2ndcdisj  22061  topnlly  22096  disllycmp  22103  dis1stc  22104  txuni2  22170  xkotf  22190  dfac14lem  22222  prdstps  22234  txindis  22239  tx1stc  22255  xkohaus  22258  xkoptsub  22259  cnmpt1st  22273  cnmpt2nd  22274  ptcmpfi  22418  trfil1  22491  fin1aufil  22537  tgpconncompeqg  22717  tgpconncomp  22718  trust  22835  met1stc  23128  dscmet  23179  retopon  23369  cnfldtopon  23388  xrsxmet  23414  xrsmopn  23417  iimulcn  23543  icopnfhmeo  23548  iccpnfhmeo  23550  xrhmeo  23551  cnheiborlem  23559  lebnumii  23571  ishtpy  23577  htpycc  23585  pco1  23620  pcohtpylem  23624  pcopt  23627  pcopt2  23628  pcoass  23629  pcorevlem  23631  rrxcph  23996  rrx0el  24002  ovoliunlem3  24108  ovolicc1  24120  ovolicc2  24126  volf  24133  ioorf  24177  dyadf  24195  dyadmbl  24204  vitalilem5  24216  vitali  24217  mbfimaopnlem  24259  mbflimsup  24270  0plef  24276  i1fima  24282  i1fima2  24283  i1fd  24285  itg1ge0  24290  itg10  24292  i1f1lem  24293  i1fadd  24299  i1fmul  24300  i1fmulc  24307  mbfi1fseqlem5  24323  itg2addlem  24362  reldv  24473  dvbsss  24505  dvef  24583  lhop1lem  24616  deg1fvi  24686  plypf1  24809  coeeulem  24821  coeeu  24822  vieta1lem2  24907  aannenlem3  24926  aalioulem3  24930  dvradcnv  25016  pserulm  25017  pserdvlem2  25023  sinhalfpilem  25056  sincos4thpi  25106  tan4thpi  25107  sincos6thpi  25108  pige3ALT  25112  resinf1o  25128  tanord1  25129  tanregt0  25131  efabl  25142  relogrn  25153  dfrelog  25157  logneg  25179  logltb  25191  logcn  25238  logf1o2  25241  dvlog  25242  efopnlem2  25248  efopn  25249  logccv  25254  dvsqrt  25331  dvcnsqrt  25333  cxpcn3  25337  logblog  25378  angpined  25416  1cubr  25428  asinsin  25478  asin1  25480  reasinsin  25482  atan0  25494  atanbnd  25512  atan1  25514  log2cnv  25530  log2ub  25535  log2le1  25536  birthday  25540  amgmlem  25575  emcllem5  25585  emgt0  25592  harmonicbnd3  25593  ftalem3  25660  basellem4  25669  sgmf  25730  ppi1  25749  cht1  25750  vma1  25751  ppiltx  25762  sqff1o  25767  ppiublem1  25786  ppiublem2  25787  ppiub  25788  chtub  25796  dchreq  25842  bposlem7  25874  bposlem8  25875  bposlem9  25876  lgsdir2lem2  25910  lgsdir2lem3  25911  chebbnd1  26056  chto1ub  26060  chpo1ubb  26065  pntibndlem1  26173  tgldimor  26296  tglnfn  26341  axlowdimlem4  26739  axlowdimlem16  26751  axlowdim  26755  upgrfi  26884  lfgrnloop  26918  lfuhgr1v0e  27044  usgrexmplef  27049  usgrres  27098  vdegp1bi  27327  vtxdginducedm1lem2  27330  pthdlem2  27557  wpthswwlks2on  27747  0ewlk  27899  0pth  27910  konigsbergiedgw  28033  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  konigsberglem4  28040  konigsberglem5  28041  ex-dif  28208  ex-un  28209  ex-in  28210  ex-fl  28232  avril1  28248  9p10ne21fool  28256  n0lplig  28266  cnidOLD  28365  cnnvm  28465  ipasslem8  28620  ipasslem10  28622  hvsubf  28798  normlem1  28893  normlem6  28898  normlem7  28899  norm-ii-i  28920  norm3adifii  28931  hilid  28944  hlimf  29020  hhssabloi  29045  hhssnv  29047  hhshsslem1  29050  shincli  29145  shsval2i  29170  shs0i  29232  chj0i  29238  chm1i  29239  chincli  29243  chdmm1i  29260  shjshsi  29275  chsup0  29331  h1de2bi  29337  spansnpji  29361  cmcmlem  29374  cmcmii  29380  cmcm2ii  29381  cmcm3ii  29382  pjidmi  29456  pjssmii  29464  pj0i  29476  pjocini  29481  mayetes3i  29512  df0op2  29535  hoaddcomi  29555  hoaddassi  29559  hocadddiri  29562  hocsubdiri  29563  hoaddid1i  29569  ho0coi  29571  hoid1i  29572  hoid1ri  29573  hodseqi  29577  honegsubi  29579  adj1o  29677  hoddii  29772  lnopunilem1  29793  lnopunilem2  29794  nmcopexi  29810  nmcopex  29812  nmcoplb  29813  nmcfnexi  29834  nmcfnex  29836  nmcfnlb  29837  adjbd1o  29868  adjcoi  29883  nmopcoadji  29884  opsqrlem6  29928  pjsdii  29938  pjddii  29939  pjidmcoi  29960  pjtoi  29962  pjin1i  29975  pjclem1  29978  stji1i  30025  reuxfrdf  30262  inindif  30287  iuninc  30324  fnresin  30385  rinvf1o  30389  suppss2f  30398  xppreima  30408  ofoprabco  30427  fressupp  30448  supppreima  30451  fsupprnfi  30452  gtiso  30460  df1stres  30463  df2ndres  30464  snct  30475  padct  30481  fsuppcurry1  30487  fsuppcurry2  30488  ffsrn  30491  fpwrelmapffs  30496  fzodif1  30542  nnindf  30561  nn0min  30562  dp2lt  30587  dp2ltsuc  30588  dp2ltc  30589  dplti  30607  dpmul  30615  dpmul4  30616  ressplusf  30663  xrsclat  30714  xrge0base  30719  xrge00  30720  xrnarchi  30863  xrge0slmod  30968  ccfldsrarelvec  31144  ccfldextdgrr  31145  locfinreflem  31193  locfinref  31194  unicls  31256  sqsscirc1  31261  mhmhmeotmd  31280  rmulccn  31281  raddcn  31282  xrge0iifiso  31288  xrge0iifhmeo  31289  lmxrge0  31305  cnzh  31321  rezh  31322  qqh0  31335  qqh1  31336  qqhre  31371  rrhre  31372  esumnul  31417  esum0  31418  esumsnf  31433  esumpfinvallem  31443  esumpfinvalf  31445  esumpcvgval  31447  esumcvgsum  31457  esumsup  31458  esumcvgre  31460  sigaclfu2  31490  dmsigagen  31513  ddemeas  31605  mbfmvolf  31634  br2base  31637  omssubadd  31668  sibfof  31708  sitg0  31714  eulerpartlemt  31739  eulerpartgbij  31740  0rrv  31819  coinfliplem  31846  coinflipprob  31847  coinfliprv  31850  ballotlem2  31856  ballotlem4  31866  ballotlem5  31867  ballotlemi1  31870  ballotlem7  31903  ballotth  31905  signsplypnf  31930  signsply0  31931  signsw0g  31936  signswch  31941  signsvf0  31960  hashreprin  32001  reprfz1  32005  chtvalz  32010  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  bnj521  32117  bnj1098  32165  bnj1109  32168  bnj1131  32169  bnj1533  32234  bnj151  32259  bnj580  32295  bnj852  32303  bnj864  32304  bnj865  32305  bnj978  32331  bnj1021  32348  bnj907  32349  bnj1093  32362  bnj1145  32375  bnj1172  32383  bnj1174  32385  bnj1176  32387  bnj1186  32389  subfacf  32535  subfacp1lem1  32539  subfacp1lem5  32544  subfacp1lem6  32545  subfacval3  32549  erdszelem2  32552  kur14lem4  32569  ioosconn  32607  iccllysconn  32610  satfn  32715  fmlaomn0  32750  gonan0  32752  goaln0  32753  elnanelprv  32789  msrfo  32906  mthmpps  32942  problem5  33025  quad3  33026  circum  33030  axextprim  33040  axrepprim  33041  axunprim  33042  axinfprim  33045  axacprim  33046  logi  33079  bcneg1  33081  setinds  33136  dfon2lem2  33142  dfon2lem4  33144  axextdfeq  33155  poseq  33208  frrlem4  33239  nosgnn0  33278  sltsolem1  33293  bdayfo  33295  nolt02o  33312  noetalem3  33332  fobigcup  33474  snelsingles  33496  fullfunfnv  33520  fullfunfv  33521  rankaltopb  33553  rank0  33744  rankeq1o  33745  hfuni  33758  fneer  33814  neibastop1  33820  nabi1i  33855  nabi2i  33856  limsucncmpi  33906  knoppcnlem8  33952  knoppcnlem11  33955  cnndvlem1  33989  bj-consensusALT  34025  bj-dtru  34254  bj-sbidmOLD  34289  bj-n0i  34386  bj-snsetex  34399  bj-tagss  34416  bj-2upln0  34459  bj-2upln1upl  34460  bj-nuliota  34474  bj-0int  34516  bj-elid5  34584  bj-inftyexpitaufo  34617  bj-pinftyccb  34636  bj-minftyccb  34640  bj-pinftynminfty  34642  iccioo01  34741  f1omptsnlem  34753  mptsnunlem  34755  topdifinffinlem  34764  relowlpssretop  34781  1oequni2o  34785  pibt2  34834  imadifss  35032  tan2h  35049  poimirlem3  35060  poimirlem9  35066  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem30  35087  mblfinlem1  35094  mblfinlem2  35095  ovoliunnfl  35099  voliunnfl  35101  itg2addnclem  35108  itg2addnclem2  35109  asindmre  35140  areacirclem1  35145  fdc  35183  cntotbnd  35234  heiborlem6  35254  rrnval  35265  reheibor  35277  rngosn3  35362  ineqcomi  35665  brcnvrabga  35759  cnvresrn  35765  moantr  35776  inxp2  35779  dfxrn2  35788  cnvcosseq  35842  refrelcosslem  35862  1cosscnvxrn  35875  redundss3  36023  refrelsredund3  36029  refrelredund3  36032  prter2  36177  renegclALT  36259  mapdunirnN  38946  lcmeprodgcdi  39295  3factsumint2  39310  3factsumint3  39311  3factsumint4  39312  3factsumint  39313  lcmineqlem4  39320  3lexlogpow5ineq1  39341  2ap1caineq  39349  metakunt6  39355  metakunt24  39373  sn-dtru  39403  sqdeccom12  39483  resubf  39519  sn-0ne2  39544  sn-subf  39565  sn-0lt1  39587  reneg1lt0  39589  dffltz  39615  rntrclfvOAI  39632  diophrw  39700  rabren3dioph  39756  pellexlem6  39775  pellex  39776  frmx  39854  frmy  39855  jm2.23  39937  jm2.27dlem3  39952  axac10  39974  pw2f1ocnv  39978  kelac2lem  40008  lmhmlnmsplit  40031  pwfi2f1o  40040  frlmpwfi  40042  ifpbiidcor  40182  alephiso2  40257  alephiso3  40258  cnvnonrel  40288  rnnonrel  40291  resnonrel  40292  cononrel1  40294  cononrel2  40295  fvnonrel  40297  cnvcnvintabd  40300  cnvintabd  40303  rclexi  40315  rtrclex  40317  clcnvlem  40323  cnvrcl0  40325  dmtrcl  40327  rntrcl  40328  dfrtrcl5  40329  iunrelexp0  40403  dmtrclfvRP  40431  rntrclfv  40433  corcltrcl  40440  cotrclrcl  40443  0heALT  40484  frege54cor1a  40565  uneqsn  40726  clsk3nimkb  40743  int-sqdefd  40887  int-sqgeq0d  40892  rr-groth  41007  rr-grothprim  41008  seff  41013  expgrowthi  41037  expgrowth  41039  binomcxplemnotnn0  41060  ee233  41225  ax6e2nd  41264  in1  41277  dfvd2ani  41289  dfvd2i  41291  dfvd3i  41298  dfvd3ani  41301  e0bi  41482  uun2221  41519  uun2221p1  41520  uun2221p2  41521  en3lpVD  41551  relopabVD  41607  ax6e2ndVD  41614  ax6e2ndALT  41636  pssnssi  41737  nnf1oxpnn  41823  icof  41848  negpilt0  41911  xrgtso  41977  supxrleubrnmptf  42090  xrpnf  42125  ioontr  42148  iccdifioo  42152  iccdifprioo  42153  uzinico2  42199  fsummulc1f  42212  fsumiunss  42217  fnlimfvre2  42319  limsupreuz  42379  limsupvaluz2  42380  limsup10ex  42415  icccncfext  42529  dvcosre  42554  dvsinax  42555  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvmptmulf  42579  dvnmul  42585  dvmptfprodlem  42586  dvnprodlem2  42589  stoweidlem1  42643  stoweidlem26  42668  stoweidlem34  42676  stoweidlem44  42686  stoweid  42705  stirlinglem5  42720  dirkercncflem1  42745  fourierdlem44  42793  fourierdlem56  42804  fourierdlem62  42810  fourierdlem89  42837  fourierdlem91  42839  fourierdlem100  42848  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem108  42856  fourierdlem112  42860  fourierdlem114  42862  fouriersw  42873  rrndistlt  42932  gsumge0cl  43010  sge0tsms  43019  sge0ltfirpmpt2  43065  ovn0  43205  hoidmv1le  43233  hoidmvle  43239  ovnsubadd2lem  43284  ovolval4lem1  43288  vonioolem2  43320  smflimlem3  43406  nsssmfmbf  43412  axorbtnotaiffb  43496  axorbciffatcxorb  43498  abnotbtaxb  43508  euabsneu  43620  sprval  43996  fmtnoinf  44053  1nevenALTV  44209  nfermltl8rev  44260  nfermltl2rev  44261  nnsum3primes4  44306  tgblthelfgott  44333  tgoldbachlt  44334  ldepslinc  44918  ackval42  45110  rrx2plordso  45138  alimp-no-surprise  45309  aacllem  45329  amgmwlem  45330  amgmlemALT  45331