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  1419  cadan  1604  nic-dfim  1664  nic-dfneg  1665  nic-mp  1666  nic-mpALT  1667  tbw-negdf  1694  rb-imdf  1745  nfri  1784  mpgbi  1793  19.35i  1873  nfim1  2192  19.36i  2226  sbievOLD  2325  ax6  2396  sbie  2538  sbieALT  2607  datisi  2761  disamis  2762  dimatis  2769  fresison  2770  bamalip  2773  axi12  2787  axi12OLD  2788  eqcomi  2828  eqtri  2842  eleqtri  2909  neii  3016  necomi  3068  neeqtri  3086  neli  3123  nrex  3267  rexlimiv  3278  rexlimi  3313  issetiOLD  3508  vtocl2OLD  3561  eueqi  3698  euxfr2w  3709  euxfr2  3711  reuxfrd  3737  cdeqri  3755  sseqtri  4001  3sstr3i  4007  pssn2lp  4076  equncomi  4129  unssi  4159  ssini  4206  unabs  4229  inabs  4230  dfin4  4242  difid  4328  ab0orv  4333  disjdif  4419  difin0  4420  snid  4593  rabrsn  4652  iinrab2  4983  symdifv  4999  rintn0  5021  breqtri  5082  axsepgfromrep  5192  bm1.3ii  5197  ax6vsep  5198  notzfaus  5253  notzfausOLD  5254  zfpow  5258  dtru  5262  dtruALT  5279  reusv2lem4  5292  dtruALT2  5326  op1stb  5354  copsexgw  5372  copsexg  5373  uniop  5396  pwunss  5446  pwundif  5449  pwundifOLD  5450  rn0  5789  dmresi  5914  somincom  5987  cnvcnv  6042  elid  6049  rescnvcnv  6054  cnvcnvres  6055  cocnvcnv2  6104  cores2  6105  co01  6107  cnviin  6130  onunisuci  6297  iota4an  6330  fnopab  6479  mpt0  6483  fnmpti  6484  f1cnvcnv  6577  f1ovi  6646  eliman0  6698  fvco4i  6755  fmpti  6869  funiunfv  6999  oprabss  7252  relmptopab  7387  zfun  7454  tfinds2  7570  omon  7583  2nd0  7688  f1stres  7705  f2ndres  7706  cnvoprab  7750  relmpoopab  7781  df1st2  7785  df2nd2  7786  fsplit  7804  fsplitOLD  7805  reldmtpos  7892  dftpos4  7903  tpostpos  7904  tpos0  7914  wfrlem4  7950  smo0  7987  tfrlem14  8019  tfrlem16  8021  rdgsucg  8051  rdglimg  8053  frfnom  8062  oawordeulem  8172  uniixp  8477  dfdom2  8527  ssdomg  8547  xpcomf1o  8598  sbthlem5  8623  pwdom  8661  limensuci  8685  fiint  8787  fidomdm  8793  residfi  8797  pwfilem  8810  mptfi  8815  fisn  8883  dffi3  8887  ordtypelem6  8979  ordtypelem7  8980  wemaplem2  9003  wdompwdom  9034  harwdom  9046  suc11reg  9074  zfinf  9094  axinf2  9095  noinfep  9115  cantnfvalf  9120  cantnflt  9127  cantnf0  9130  cantnf  9148  tz9.1c  9164  tc2  9176  r111  9196  r1tr2  9198  r1ordg  9199  r1sssuc  9204  r1val1  9207  tz9.13  9212  r1elssi  9226  pwwf  9228  rankopb  9273  rankeq0b  9281  ranksuc  9286  rankmapu  9299  rankxplim  9300  rankxplim3  9302  rankxpsuc  9303  cp  9312  karden  9316  card0  9379  cardlim  9393  cardom  9407  infxpenlem  9431  alephsuc2  9498  alephgeom  9500  unialeph  9519  dfac4  9540  dfacacn  9559  dju1dif  9590  dju1p1e2  9591  infdju1  9607  ackbij1lem13  9646  ackbij2  9657  cf0  9665  cfsuc  9671  cfom  9678  cfslb2n  9682  ominf4  9726  fin23lem17  9752  fin23lem28  9754  fin23lem30  9756  fin23lem31  9757  fin23lem40  9765  isfin1-3  9800  dfacfin7  9813  fin1a2lem6  9819  itunitc1  9834  axcc3  9852  dcomex  9861  axdc2lem  9862  axcclem  9871  zfac  9874  ac3  9876  ackm  9879  axac2  9880  axac  9881  axaci  9882  cardeqv  9883  numth2  9885  numth  9886  dmct  9938  brdom3  9942  fin71ac  9947  cardf  9964  aleph1  9985  cfpwsdom  9998  smobeth  10000  zfcndrep  10028  zfcndpow  10030  zfcndac  10033  gch2  10089  wunex3  10155  tskpr  10184  inar1  10189  rankcf  10191  tskcard  10195  tskuni  10197  grothpw  10240  axgroth4  10246  grothprim  10248  inaprc  10250  dmaddpi  10304  dmmulpi  10305  1lt2pi  10319  addpqf  10358  mulpqf  10360  1lt2nq  10387  supsrlem  10525  ssxr  10702  gtso  10714  subf  10880  negne0i  10953  mulnzcnopr  11278  infrenegsup  11616  nnne0  11663  halflt1  11847  nn0ssz  11995  3halfnz  12053  zeo  12060  numlt  12115  numltc  12116  le9lt10  12117  decle  12124  uzf  12238  xaddf  12609  xsubge0  12646  xmulf  12657  ixxf  12740  ixxssxr  12742  iooval2  12763  ioof  12827  unirnioo  12829  dfioo2  12830  fzval2  12887  fzf  12888  0nelfz1  12918  fz10  12920  fzpreddisj  12948  4fvwrd4  13019  fzof  13027  fzo0  13053  fldiv4p1lem1div2  13197  fldiv4lem1div2  13199  om2uzoi  13315  faclbnd4lem1  13645  hashkf  13684  hashgval  13685  hashinf  13687  hashresfn  13692  hashnn0n0nn  13744  hashbclem  13802  hashge3el3dif  13836  wrdexgOLD  13864  rev0  14118  s2dm  14244  f1oun2prg  14271  trclublem  14347  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  n2dvds1OLD  15710  divalglem1  15737  divalglem5  15740  divalglem6  15741  divalglem10  15745  flodddiv4  15756  0bits  15780  sadcf  15794  sadcadd  15799  bitsshft  15816  smupf  15819  gcdf  15853  eucalgf  15919  2prm  16028  dfphi2  16103  pockthi  16235  prmrec  16250  vdwapf  16300  vdwlem6  16314  karatsuba  16412  1259lem5  16460  2503lem3  16464  4001lem4  16469  structcnvcnv  16489  structfn  16492  strleun  16583  prdsval  16720  prdsds  16729  imasvscafn  16802  xpsff1o  16832  sscpwex  17077  wunfunc  17161  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  19112  dprdval  19117  invrfval  19415  drngui  19500  rmodislmod  19694  lssintcl  19728  mplsubrglem  20211  opsrtoslem2  20257  cnfldfun  20549  cnfld0  20561  cnfld1  20562  cnfldsub  20565  xrsds  20580  psgnghm  20716  zrhpsgnmhm  20720  recrng  20757  ocv1  20815  dsmmbas2  20873  mdetralt  21209  maducoeval2  21241  eltpsi  21544  unitg  21567  fctop  21604  cctop  21606  ppttop  21607  epttop  21609  leordtvallem1  21810  leordtvallem2  21811  iccordt  21814  iscnp2  21839  discmp  21998  conncompcld  22034  1stcrestlem  22052  2ndcdisj  22056  topnlly  22091  disllycmp  22098  dis1stc  22099  txuni2  22165  xkotf  22185  dfac14lem  22217  prdstps  22229  txindis  22234  tx1stc  22250  xkohaus  22253  xkoptsub  22254  cnmpt1st  22268  cnmpt2nd  22269  ptcmpfi  22413  trfil1  22486  fin1aufil  22532  tgpconncompeqg  22712  tgpconncomp  22713  tsmsres  22744  trust  22830  met1stc  23123  dscmet  23174  retopon  23364  cnfldtopon  23383  xrsxmet  23409  xrsmopn  23412  iimulcn  23534  icopnfhmeo  23539  iccpnfhmeo  23541  xrhmeo  23542  cnheiborlem  23550  lebnumii  23562  ishtpy  23568  htpycc  23576  pco1  23611  pcohtpylem  23615  pcopt  23618  pcopt2  23619  pcoass  23620  pcorevlem  23622  cfilresi  23890  rrxcph  23987  rrx0el  23993  ovoliunlem3  24097  ovolicc1  24109  ovolicc2  24115  volf  24122  ioorf  24166  dyadf  24184  dyadmbl  24193  vitalilem5  24205  vitali  24206  mbfimaopnlem  24248  mbflimsup  24259  0plef  24265  i1fima  24271  i1fima2  24272  i1fd  24274  itg1ge0  24279  itg10  24281  i1f1lem  24282  i1fadd  24288  i1fmul  24289  i1fmulc  24296  mbfi1fseqlem5  24312  itg2addlem  24351  reldv  24460  dvbsss  24492  dvef  24569  lhop1lem  24602  deg1fvi  24671  plypf1  24794  coeeulem  24806  coeeu  24807  vieta1lem2  24892  aannenlem3  24911  aalioulem3  24915  dvradcnv  25001  pserulm  25002  pserdvlem2  25008  sinhalfpilem  25041  sincos4thpi  25091  tan4thpi  25092  sincos6thpi  25093  pige3ALT  25097  resinf1o  25112  tanord1  25113  tanregt0  25115  efabl  25126  relogrn  25137  dfrelog  25141  logneg  25163  logltb  25175  logcn  25222  logf1o2  25225  dvlog  25226  efopnlem2  25232  efopn  25233  logccv  25238  dvsqrt  25315  dvcnsqrt  25317  cxpcn3  25321  logblog  25362  angpined  25400  1cubr  25412  asinsin  25462  asin1  25464  reasinsin  25466  atan0  25478  atanbnd  25496  atan1  25498  log2cnv  25514  log2ub  25519  log2le1  25520  birthday  25524  amgmlem  25559  emcllem5  25569  emgt0  25576  harmonicbnd3  25577  ftalem3  25644  basellem4  25653  sgmf  25714  ppi1  25733  cht1  25734  vma1  25735  ppiltx  25746  sqff1o  25751  ppiublem1  25770  ppiublem2  25771  ppiub  25772  chtub  25780  dchreq  25826  bposlem7  25858  bposlem8  25859  bposlem9  25860  lgsdir2lem2  25894  lgsdir2lem3  25895  chebbnd1  26040  chto1ub  26044  chpo1ubb  26049  pntibndlem1  26157  tgldimor  26280  tglnfn  26325  axlowdimlem4  26723  axlowdimlem16  26735  axlowdim  26739  upgrfi  26868  lfgrnloop  26902  lfuhgr1v0e  27028  usgrexmplef  27033  usgrres  27082  vdegp1bi  27311  vtxdginducedm1lem2  27314  pthdlem2  27541  wpthswwlks2on  27732  0ewlk  27885  0pth  27896  konigsbergiedgw  28019  konigsberglem1  28023  konigsberglem2  28024  konigsberglem3  28025  konigsberglem4  28026  konigsberglem5  28027  ex-dif  28194  ex-un  28195  ex-in  28196  ex-fl  28218  avril1  28234  9p10ne21fool  28242  n0lplig  28252  cnidOLD  28351  cnnvm  28451  ipasslem8  28606  ipasslem10  28608  hvsubf  28784  normlem1  28879  normlem6  28884  normlem7  28885  norm-ii-i  28906  norm3adifii  28917  hilid  28930  hlimf  29006  hhssabloi  29031  hhssnv  29033  hhshsslem1  29036  shincli  29131  shsval2i  29156  shs0i  29218  chj0i  29224  chm1i  29225  chincli  29229  chdmm1i  29246  shjshsi  29261  chsup0  29317  h1de2bi  29323  spansnpji  29347  cmcmlem  29360  cmcmii  29366  cmcm2ii  29367  cmcm3ii  29368  pjidmi  29442  pjssmii  29450  pj0i  29462  pjocini  29467  mayetes3i  29498  df0op2  29521  hoaddcomi  29541  hoaddassi  29545  hocadddiri  29548  hocsubdiri  29549  hoaddid1i  29555  ho0coi  29557  hoid1i  29558  hoid1ri  29559  hodseqi  29563  honegsubi  29565  adj1o  29663  hoddii  29758  lnopunilem1  29779  lnopunilem2  29780  nmcopexi  29796  nmcopex  29798  nmcoplb  29799  nmcfnexi  29820  nmcfnex  29822  nmcfnlb  29823  adjbd1o  29854  adjcoi  29869  nmopcoadji  29870  opsqrlem6  29914  pjsdii  29924  pjddii  29925  pjidmcoi  29946  pjtoi  29948  pjin1i  29961  pjclem1  29964  stji1i  30011  reuxfrdf  30247  inindif  30270  iuninc  30304  fnresin  30363  rinvf1o  30367  suppss2f  30376  xppreima  30386  ofoprabco  30401  gtiso  30428  df1stres  30431  df2ndres  30432  snct  30441  padct  30447  fsuppcurry1  30453  fsuppcurry2  30454  ffsrn  30457  fpwrelmapffs  30462  fzodif1  30508  nnindf  30527  nn0min  30529  dp2lt  30554  dp2ltsuc  30555  dp2ltc  30556  dplti  30574  dpmul  30582  dpmul4  30583  ressplusf  30630  xrsclat  30660  xrge0base  30665  xrge00  30666  xrnarchi  30806  xrge0slmod  30910  ccfldsrarelvec  31049  ccfldextdgrr  31050  locfinreflem  31097  locfinref  31098  unicls  31139  sqsscirc1  31144  mhmhmeotmd  31163  rmulccn  31164  raddcn  31165  xrge0iifiso  31171  xrge0iifhmeo  31172  lmxrge0  31188  cnzh  31204  rezh  31205  qqh0  31218  qqh1  31219  qqhre  31254  rrhre  31255  esumnul  31300  esum0  31301  esumsnf  31316  esumpfinvallem  31326  esumpfinvalf  31328  esumpcvgval  31330  esumcvgsum  31340  esumsup  31341  esumcvgre  31343  sigaclfu2  31373  dmsigagen  31396  ldgenpisyslem1  31415  ddemeas  31488  imambfm  31513  mbfmvolf  31517  br2base  31520  omssubadd  31551  sibfof  31591  sitg0  31597  eulerpartlemt  31622  eulerpartgbij  31623  0rrv  31702  coinfliplem  31729  coinflipprob  31730  coinfliprv  31733  ballotlem2  31739  ballotlem4  31749  ballotlem5  31750  ballotlemi1  31753  ballotlem7  31786  ballotth  31788  signsplypnf  31813  signsply0  31814  signsw0g  31819  signswch  31824  signsvf0  31843  hashreprin  31884  reprfz1  31888  chtvalz  31893  hgt750lemd  31912  hgt750lem  31915  hgt750lem2  31916  bnj521  32000  bnj1098  32048  bnj1109  32051  bnj1131  32052  bnj1533  32117  bnj151  32142  bnj580  32178  bnj852  32186  bnj864  32187  bnj865  32188  bnj978  32214  bnj1021  32231  bnj907  32232  bnj1093  32245  bnj1145  32258  bnj1172  32266  bnj1174  32268  bnj1176  32270  bnj1186  32272  subfacf  32415  subfacp1lem1  32419  subfacp1lem5  32424  subfacp1lem6  32425  subfacval3  32429  erdszelem2  32432  kur14lem4  32449  ioosconn  32487  iccllysconn  32490  satfn  32595  fmlaomn0  32630  gonan0  32632  goaln0  32633  elnanelprv  32669  msrfo  32786  mthmpps  32822  problem5  32905  quad3  32906  circum  32910  axextprim  32920  axrepprim  32921  axunprim  32922  axinfprim  32925  axacprim  32926  logi  32959  bcneg1  32961  setinds  33016  dfon2lem2  33022  dfon2lem4  33024  axextdfeq  33035  poseq  33088  frrlem4  33119  nosgnn0  33158  sltsolem1  33173  bdayfo  33175  nolt02o  33192  noetalem3  33212  fobigcup  33354  snelsingles  33376  fullfunfnv  33400  fullfunfv  33401  rankaltopb  33433  rank0  33624  rankeq1o  33625  hfuni  33638  fneer  33694  neibastop1  33700  nabi1i  33735  nabi2i  33736  limsucncmpi  33786  knoppcnlem8  33832  knoppcnlem11  33835  cnndvlem1  33869  bj-consensusALT  33905  bj-dtru  34132  bj-sbidmOLD  34167  bj-n0i  34255  bj-snsetex  34268  bj-tagss  34285  bj-2upln0  34328  bj-2upln1upl  34329  bj-nuliota  34342  bj-0int  34385  bj-elid5  34453  bj-inftyexpitaufo  34476  bj-pinftyccb  34495  bj-minftyccb  34499  bj-pinftynminfty  34501  f1omptsnlem  34609  mptsnunlem  34611  topdifinffinlem  34620  relowlpssretop  34637  1oequni2o  34641  pibt2  34690  imadifss  34859  tan2h  34876  poimirlem3  34887  poimirlem9  34893  poimirlem16  34900  poimirlem17  34901  poimirlem18  34902  poimirlem19  34903  poimirlem20  34904  poimirlem22  34906  poimirlem30  34914  mblfinlem1  34921  mblfinlem2  34922  ovoliunnfl  34926  voliunnfl  34928  itg2addnclem  34935  itg2addnclem2  34936  asindmre  34969  areacirclem1  34974  fdc  35012  cntotbnd  35066  heiborlem6  35086  rrnval  35097  reheibor  35109  rngosn3  35194  ineqcomi  35497  brcnvrabga  35591  cnvresrn  35597  moantr  35608  inxp2  35611  dfxrn2  35620  cnvcosseq  35674  refrelcosslem  35694  1cosscnvxrn  35707  redundss3  35855  refrelsredund3  35861  refrelredund3  35864  prter2  36009  renegclALT  36091  mapdunirnN  38778  sn-dtru  39101  sqdeccom12  39165  resubf  39201  sn-0ne2  39226  sn-0lt1  39236  dffltz  39261  rntrclfvOAI  39278  diophrw  39346  rabren3dioph  39402  pellexlem6  39421  pellex  39422  frmx  39500  frmy  39501  jm2.23  39583  jm2.27dlem3  39598  axac10  39620  pw2f1ocnv  39624  kelac2lem  39654  lmhmlnmsplit  39677  pwfi2f1o  39686  frlmpwfi  39688  ifpbiidcor  39830  alephiso2  39907  alephiso3  39908  cnvnonrel  39938  rnnonrel  39941  resnonrel  39942  cononrel1  39944  cononrel2  39945  fvnonrel  39947  cnvcnvintabd  39950  cnvintabd  39953  rclexi  39965  rtrclex  39967  clcnvlem  39973  cnvrcl0  39975  dmtrcl  39977  rntrcl  39978  dfrtrcl5  39979  iunrelexp0  40037  dmtrclfvRP  40065  rntrclfv  40067  corcltrcl  40074  cotrclrcl  40077  0heALT  40119  frege54cor1a  40200  dssmapnvod  40356  uneqsn  40363  clsk3nimkb  40380  gneispace  40474  int-sqdefd  40524  int-sqgeq0d  40529  rr-groth  40625  rr-grothprim  40626  seff  40631  expgrowthi  40655  expgrowth  40657  binomcxplemnotnn0  40678  ee233  40843  ax6e2nd  40882  in1  40895  dfvd2ani  40907  dfvd2i  40909  dfvd3i  40916  dfvd3ani  40919  e0bi  41100  uun2221  41137  uun2221p1  41138  uun2221p2  41139  en3lpVD  41169  relopabVD  41225  ax6e2ndVD  41232  ax6e2ndALT  41254  pssnssi  41357  nnf1oxpnn  41446  icof  41471  negpilt0  41535  xrgtso  41602  supxrleubrnmptf  41716  xrpnf  41751  ioontr  41776  iccdifioo  41780  iccdifprioo  41781  uzinico2  41827  fsummulc1f  41840  fsumiunss  41845  fnlimfvre2  41947  limsupreuz  42007  limsupvaluz2  42008  limsup10ex  42043  icccncfext  42159  dvcosre  42185  dvsinax  42186  ioodvbdlimc1lem2  42206  ioodvbdlimc2lem  42208  dvmptmulf  42211  dvnmul  42217  dvmptfprodlem  42218  dvnprodlem2  42221  stoweidlem1  42276  stoweidlem26  42301  stoweidlem34  42309  stoweidlem44  42319  stoweid  42338  stirlinglem5  42353  dirkercncflem1  42378  fourierdlem44  42426  fourierdlem56  42437  fourierdlem62  42443  fourierdlem89  42470  fourierdlem91  42472  fourierdlem100  42481  fourierdlem102  42483  fourierdlem103  42484  fourierdlem104  42485  fourierdlem108  42489  fourierdlem112  42493  fourierdlem114  42495  fouriersw  42506  rrndistlt  42565  gsumge0cl  42643  sge0tsms  42652  sge0ltfirpmpt2  42698  ovn0  42838  hoidmv1le  42866  hoidmvle  42872  ovnsubadd2lem  42917  ovolval4lem1  42921  vonioolem2  42953  smflimlem3  43039  nsssmfmbf  43045  axorbtnotaiffb  43129  axorbciffatcxorb  43131  abnotbtaxb  43141  euabsneu  43253  sprval  43631  fmtnoinf  43688  1nevenALTV  43846  nfermltl8rev  43897  nfermltl2rev  43898  nnsum3primes4  43943  tgblthelfgott  43970  tgoldbachlt  43971  ldepslinc  44554  rrx2plordso  44701  alimp-no-surprise  44872  aacllem  44892  amgmwlem  44893  amgmlemALT  44894