Theorem mpbiri 257

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
mpbiri.min	⊢ 𝜒
mpbiri.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbiri	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 ⊢ 𝜒
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜒)
3		mpbiri.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbird 256	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  elimh  1080  spei  2387  nfald2  2438  nfabd2  2919  raleleq  3327  dedhb  3696  sbceqalOLD  3841  csbie2df  4441  ssdifeq0  4487  r19.2zb  4496  dedth  4587  pwidg  4623  snidg  4663  rexreusng  4684  exsnrex  4685  ifpr  4696  rmosn  4724  rabrsn  4729  prid1g  4765  tpid1g  4774  tpid2g  4776  tpid3g  4777  pwpw0  4817  sssn  4830  elpreqpr  4868  unimax  4947  intmin3  4979  eqbrtrdi  5187  al0ssb  5308  intabs  5344  pwnss  5350  difelpw  5352  rabelpw  5353  0inp0  5358  intidg  5458  copsexgw  5491  copsexg  5492  euotd  5514  elopab  5528  elvvuni  5753  posn  5762  frsn  5764  eqrelriv  5790  relsnb  5803  relopabiALT  5824  opabid2  5829  ididg  5855  iss  6039  dfpo2  6300  ord0eln0  6424  sucidg  6450  nsuceq0  6452  funopg  6586  fn0  6685  f00  6777  f0bi  6778  f10d  6870  f1o00  6871  fo00  6872  brprcneu  6884  brprcneuALT  6885  dffn5  6954  fsn  7142  funop  7156  funsndifnop  7158  fnsnb  7173  eufnfv  7239  f1eqcocnv  7308  nfriotadw  7381  nfriotad  7385  riotaprop  7401  oprabidw  7448  oprabid  7449  elrnmpo  7555  ov6g  7583  ovelrn  7595  caovmo  7656  offn  7696  caofinvl  7714  fr3nr  7773  onprc  7779  ordeleqon  7783  onint0  7793  0elsuc  7837  onuninsuci  7843  orduninsuc  7846  ordzsl  7848  onzsl  7849  tfinds  7863  limomss  7874  limom  7885  peano5  7898  peano5OLD  7899  xpexr  7924  eqop2  8035  opreuopreu  8037  1stconst  8103  2ndconst  8104  frxp2  8147  frxp3  8154  funsssuppss  8193  dftpos3  8248  dftpos4  8249  wfrlem4OLD  8331  wfrlem14OLD  8341  oawordeulem  8573  omwordi  8590  nnmwordi  8654  riiner  8807  ecopover  8838  map0g  8901  mapsnd  8903  elixpsn  8954  en0  9036  en0OLD  9037  en0ALT  9038  en0r  9039  en1  9044  en1OLD  9045  fiprc  9068  sbthlem2  9107  sbthlem4  9109  sbthlem5  9110  0domg  9123  findcard  9186  findcard2  9187  nneneq  9232  nneneqOLD  9244  sdom1  9265  sdom1OLD  9266  1sdom2dom  9270  fineqvlem  9285  nfielex  9296  enp1i  9302  findcard2OLD  9307  elfiun  9453  marypha1lem  9456  oicl  9552  oif  9553  oion  9559  hartogslem1  9565  hartogs  9567  wemapso2  9576  card2on  9577  0wdom  9593  brwdom2  9596  inf3lem6  9656  cantnflem3  9714  cantnflem4  9715  wemapwe  9720  cnfcom  9723  ssttrcl  9738  ttrclselem2  9749  tctr  9763  r1tr  9799  r1rankidb  9827  r1pw  9868  scottex  9908  scott0  9909  bnd2  9916  eldju2ndl  9947  tskwe  9973  oncard  9983  cardlim  9995  harsdom  10018  en2eleq  10031  dfac8alem  10052  cardaleph  10112  iunfictbso  10137  infmap2  10241  ackbij1lem18  10260  cff  10271  cfsuc  10280  cff1  10281  cflim2  10286  cfss  10288  sdom2en01  10325  infpssrlem4  10329  fin23lem7  10339  fin23lem11  10340  isfin2-2  10342  fin23lem26  10348  fin23lem19  10359  fin23lem17  10361  isf34lem2  10396  isf34lem4  10400  fin1a2lem6  10428  fin1a2lem10  10432  fin1a2lem12  10434  itunifn  10440  hsmexlem1  10449  axcc2lem  10459  dcomex  10470  axdc3lem4  10476  ondomon  10586  konigthlem  10591  pwcfsdom  10606  cfpwsdom  10607  axpowndlem3  10622  canth4  10670  canthnumlem  10671  canthwelem  10673  canthwe  10674  canthp1lem2  10676  pwfseqlem4  10685  pwfseqlem5  10686  gchaleph  10694  gch2  10698  winainflem  10716  0tsk  10778  rankcf  10800  tskcard  10804  gruina  10841  grutsk  10845  tskmid  10863  indpi  10930  nqereu  10952  mulcanenq  10983  recmulnq  10987  archnq  11003  ltsopr  11055  1ne0sr  11119  0idsr  11120  00sr  11122  leid  11340  lelttric  11351  divcan3  11928  lemul1a  12098  nn1suc  12264  nn0n0n1ge2b  12570  xnn0xr  12579  xnn0nemnf  12585  nn0lt10b  12654  nn0ind-raph  12692  elnn1uz2  12939  indstr2  12941  uzsupss  12954  rpnnen1lem4  12994  rpnnen1lem5  12995  xrnemnf  13129  xrnepnf  13130  mnfltxr  13139  xnn0n0n1ge2b  13143  xnn0ge0  13145  xrlttri  13150  xrlttr  13151  xrleid  13162  qbtwnxr  13211  xmullem2  13276  xlemul1a  13299  xrub  13323  reltxrnmnf  13353  ixxun  13372  xnn0xrge0  13515  fztpval  13595  fseq1p1m1  13607  elfznelfzob  13770  ltweuz  13958  fzfi  13969  fsuppmapnn0fiubex  13989  ser0f  14052  0exp  14094  faclbnd4lem1  14284  bcn1  14304  hashnemnf  14335  hashv01gt1  14336  hashsnle1  14408  hashgt12el2  14414  hashpw  14427  hashf1  14450  fz1isolem  14454  hash2prb  14465  0wrd0  14522  wrdlen1  14536  ccatvalfn  14563  eqs1  14594  wrdl1exs1  14595  swrdlen  14629  swrdwrdsymb  14644  swrdspsleq  14647  cats1un  14703  wrdind  14704  wrd2ind  14705  swrdccatin1  14707  repswsymballbi  14762  cshw1  14804  scshwfzeqfzo  14809  wrdl2exs2  14929  trclfvcotr  14988  relexp1g  15005  relexp0rel  15016  relexprelg  15017  relexpreld  15019  sqrt0  15220  sqrtsq  15248  mptfzshft  15756  prodf1f  15870  egt2lt3  16182  0dvds  16253  nn0onn  16356  nn0o  16359  divalgmod  16382  flodddiv4  16389  bitsp1o  16407  gcddvds  16477  bezout  16518  lcmdvds  16578  rpdvds  16630  1nprm  16649  prmind2  16655  dvdszzq  16692  nnoddn2prmb  16781  pcpre1  16810  vdwapf  16940  vdwapid1  16943  ram0  16990  ramz  16993  prmolefac  17014  cshws0  17070  prmlem0  17074  strle1  17126  restsspw  17412  prdsdsfn  17446  imasdsfn  17495  imasaddfnlem  17509  imasvscafn  17518  xpsfrnel  17543  isacs1i  17636  cidfn  17658  fnhomeqhomf  17670  comffn  17684  isoval  17747  sscres  17805  cofucl  17873  idffth  17921  ressffth  17926  cat1lem  18084  catcoppccl  18105  catcoppcclOLD  18106  estrchomfn  18124  funcestrcsetclem4  18133  funcestrcsetclem7  18136  equivestrcsetc  18142  funcsetcestrclem4  18148  funcsetcestrclem7  18151  1stfcl  18187  2ndfcl  18188  prfcl  18193  evlfcl  18213  curf1cl  18219  curfcl  18223  hofcl  18250  yonedainv  18272  pospo  18336  lubfun  18343  glbfun  18356  joindmss  18370  meetdmss  18384  ipopos  18527  acsficl2d  18543  dirref  18592  mgmidcl  18625  mgmlrid  18626  ielefmnd  18843  smndex1basss  18861  smndex1n0mnd  18868  cntzssv  19283  idresperm  19344  symgvalstruct  19355  symgvalstructOLD  19356  pmtrfmvdn0  19421  symggen  19429  psgnunilem1  19452  psgnprfval  19480  slwpgp  19572  frgpmhm  19724  frgpuptinv  19730  frgpup3lem  19736  gsumzoppg  19903  gsumcom2  19934  c0snmhm  20406  srhmsubc  20617  rhmsubclem1  20622  abv0  20715  rrgsupp  21242  zrhrhm  21441  psgnodpmr  21526  frlmphllem  21718  ellspd  21740  psrvscafval  21897  psrridm  21912  ltbwe  21989  psrbag0  22013  psrbagsn  22014  subrgascl  22017  psdmul  22098  mattpostpos  22386  mavmul0  22484  mavmul0g  22485  mdet0f1o  22525  m1detdiag  22529  m2detleiblem5  22557  m2detleiblem6  22558  m2detleiblem3  22561  m2detleiblem4  22562  maducoeval2  22572  d1mat2pmat  22671  chpmat1dlem  22767  chpmat1d  22768  baspartn  22887  eltg3  22895  topnex  22929  fctop  22937  cctop  22939  discld  23023  mretopd  23026  neipeltop  23063  neitr  23114  restcls  23115  ordtbaslem  23122  ordtuni  23124  idcn  23191  cnrmi  23294  cmpsublem  23333  cmpsub  23334  tgcmp  23335  uncmp  23337  hauscmplem  23340  cmpfi  23342  bwth  23344  1stcrestlem  23386  disllycmp  23432  dis1stc  23433  refref  23447  kgeni  23471  1stckgenlem  23487  kqffn  23659  snfil  23798  filconn  23817  cfinfil  23827  ufileu  23853  filufint  23854  fixufil  23856  cfinufil  23862  ufilen  23864  fin1aufil  23866  fmf  23879  rnelfm  23887  flimclslem  23918  hauspwpwf1  23921  supnfcls  23954  flimfnfcls  23962  fclscmp  23964  alexsubALTlem2  23982  alexsubALTlem3  23983  alexsubALT  23985  ptcmplem1  23986  cnextrel  23997  tsmsfbas  24062  ustref  24153  trust  24164  restutop  24172  isusp  24196  xmet0  24278  imasdsf1olem  24309  blfvalps  24319  blfps  24342  blf  24343  restmetu  24509  dscmet  24511  isngp2  24536  nm0  24568  nrginvrcn  24639  nmoix  24676  qdensere  24716  iccconn  24776  iccpnfcnv  24899  xrhmeo  24901  lebnumlem3  24919  metsscmetcld  25273  bcthlem5  25286  csschl  25334  rrxmfval  25364  minveclem3b  25386  cniccbdd  25420  ovolicc2lem4  25479  iunmbl  25512  ioorinv  25535  ioorcl  25536  i1f1lem  25648  limcvallem  25830  ellimc2  25836  limccnp  25850  limccnp2  25851  limcco  25852  perfdvf  25862  recnprss  25863  fncpn  25893  dvcmulf  25906  c1lip1  25960  lhop2  25978  q1pcl  26122  r1pdeglt  26125  ply1remlem  26129  plyssc  26164  ulm0  26357  cxpeq0  26642  cxplea  26660  cxplogb  26748  asinlem  26830  isppw2  27077  muval2  27096  dchrfi  27218  dchrpt  27230  bposlem6  27252  lgsdir2lem2  27289  lgsqr  27314  gausslemma2dlem4  27332  2lgslem2  27358  2lgslem3  27367  2lgs  27370  2sqlem7  27387  2sqlem11  27392  chtppilim  27438  nosgnn0i  27622  nolesgn2ores  27635  nogesgn1ores  27637  nosepnelem  27642  nosepdmlem  27646  nosupbnd1lem3  27673  nosupbnd1lem5  27675  nosupbnd2lem1  27678  noinfbnd1lem3  27688  noinfbnd1lem5  27690  noinfbnd2lem1  27693  oldval  27811  made0  27830  lrrecpo  27888  pncan2s  28014  abssor  28174  om2noseqfo  28205  noseqrdglem  28212  noseqrdgfn  28213  noseqrdg0  28214  n0scut  28239  tgldimor  28362  tgcgr4  28391  tglnfn  28407  tglnunirn  28408  mirne  28527  mircinv  28528  perpln1  28570  perpln2  28571  lmiisolem  28656  xmstrkgc  28752  axcgrtr  28782  axsegconlem9  28792  axlowdimlem5  28813  axlowdimlem17  28825  axlowdim1  28826  uhgr0e  28940  edglnl  29012  uhgr0edgfi  29109  issubgr2  29141  subgrprop2  29143  egrsubgr  29146  0grsubgr  29147  0uhgrsubgr  29148  uhgrsubgrself  29149  nbgr1vtx  29227  nbgrssovtx  29230  nb3grprlem1  29249  uvtx01vtx  29266  cplgr1vlem  29298  cplgr1v  29299  usgrexilem  29309  wlkcomp  29501  wlk1walk  29509  wlkp1lem5  29547  uhgrwkspthlem1  29623  pthdlem1  29636  clwlkcomp  29649  lfgrn1cycl  29672  uspgrn2crct  29675  wwlksn0s  29728  umgrwwlks2on  29824  clwwlkn  29892  clwwlkn1  29907  0ewlk  29980  1ewlk  29981  0spth  29992  upgr1wlkdlem2  30012  wlk2v2e  30023  upgr3v3e3cycl  30046  upgr4cycl4dv4e  30051  eupth0  30080  frgr0v  30128  frgr1v  30137  1vwmgr  30142  ex-opab  30298  grpoinvf  30398  nvmid  30525  nmlnoubi  30662  hiidrcl  30961  hsn0elch  31114  shjshseli  31359  cmbr4i  31467  dfiop2  31619  kbpj  31822  nmopun  31880  adjeq0  31957  kbass2  31983  pjssdif1i  32041  pjinvari  32057  pjcmul2i  32068  pj3i  32074  stge1i  32104  stle0i  32105  sumdmdlem2  32285  dmdbr6ati  32289  dmdbr7ati  32290  rabsnel  32355  unidifsnel  32388  unidifsnne  32389  disjdifprg  32422  ofoprabco  32507  padct  32558  fpwrelmapffslem  32571  xrlelttric  32579  xnn0gt0  32596  iundisj2cnt  32624  f1ocnt  32627  fz1nnct  32628  fz1nntr  32629  hashxpe  32633  nn0min  32640  wrdt2ind  32731  xrge0tsmsbi  32829  opprabs  33255  0ringufd  33310  locfinref  33512  dispcmp  33530  zartopn  33546  zarcmplem  33552  pstmxmet  33568  xrge0iifcnv  33604  xrge0iif1  33609  qqhre  33691  esumcl  33719  esumpr2  33756  esumpinfval  33762  esumpcvgval  33767  ofcfn  33789  pwsiga  33819  prsiga  33820  sigainb  33825  ldgenpisyslem1  33852  measiuns  33906  relfae  33936  pmeasmono  34014  sitgf  34037  eulerpartgbij  34062  sgnmulsgn  34239  sgnmulsgp  34240  signswch  34263  signslema  34264  signstlen  34269  signstfvn  34271  circlevma  34344  bnj216  34433  bnj151  34578  bnj517  34586  bnj970  34648  bnj1145  34694  bnj1498  34762  fineqvrep  34785  fineqvac  34787  0nn0m1nnn0  34792  pthhashvtx  34807  acycgr0v  34828  prclisacycgr  34831  umgracycusgr  34834  cusgracyclt3v  34836  subfacp1lem5  34864  erdszelem8  34878  kur14lem1  34886  indispconn  34914  cvmsss2  34954  satfvsuclem2  35040  satfrel  35047  satfrnmapom  35050  satfv0fun  35051  satf00  35054  satf0suclem  35055  fmlasuc0  35064  msubrn  35209  dfon2lem7  35455  brbigcup  35564  elsingles  35584  fnimage  35595  funpartlem  35608  dfrdg4  35617  imagesset  35619  altopthsn  35627  elaltxp  35641  ellines  35818  linethru  35819  rankeq1o  35837  elhf2  35841  hfninf  35852  nn0prpwlem  35876  fneref  35904  neibastop2lem  35914  limsucncmpi  35999  bj-exlimmpbir  36462  curryset  36495  bj-snglex  36522  bj-restpw  36641  bj-inftyexpidisj  36759  topdifinffinlem  36896  relowlssretop  36912  rdgeqoa  36919  finxpreclem6  36945  fvineqsneq  36961  pibt2  36966  poimirlem23  37186  poimirlem29  37192  poimirlem31  37194  volsupnfl  37208  cnambfre  37211  dvasin  37247  dvacos  37248  sdclem2  37285  sstotbnd2  37317  ssbnd  37331  ismgmOLD  37393  grpokerinj  37436  rngomndo  37478  isdrngo1  37499  ac6s6  37715  iss2  37885  cnvelrels  38036  cosselrels  38037  brssrid  38043  brcnvssrid  38048  dfdisjs5  38253  eldisjs5  38267  mpets2  38382  pets  38393  prtlem12  38408  riotasv2d  38498  lkrscss  38639  islshpkrN  38661  isline  39281  ispointN  39284  0psubN  39291  linepsubN  39294  atpsubN  39295  cdlemk36  40455  diafn  40576  dibfna  40696  dibvalrel  40705  dicvalrelN  40727  diclspsn  40736  dihvalrel  40821  dih1  40828  lclkrlem1  41048  lclkr  41075  mapd1o  41190  mapdin  41204  hdmapfnN  41371  hgmapfnN  41430  lcmineqlem10  41578  sticksstones9  41695  sn-iotalem  41778  repncan2  42002  sn-inelr  42085  elrfirn  42180  ismrcd1  42183  istopclsd  42185  rabren3dioph  42300  jm2.17b  42447  jm2.22  42481  jm2.23  42482  ttac  42522  pw2f1ocnv  42523  dnnumch1  42533  hbtlem5  42617  mncn0  42628  aaitgo  42651  rngunsnply  42662  unielss  42711  onexlimgt  42736  cantnfresb  42818  dflim5  42823  naddwordnexlem4  42896  safesnsupfiss  42910  safesnsupfidom1o  42912  safesnsupfilb  42913  ensucne0OLD  43025  clcnvlem  43118  relexp01min  43208  ntrf  43618  ssrecnpr  43810  seff  43811  sblpnf  43812  nzss  43819  dvconstbi  43836  ipo0  43951  ifr0  43952  addrfn  43974  subrfn  43975  mulvfn  43976  refsum2cnlem1  44464  rn1st  44713  ellimciota  45065  dvmptconst  45366  dvmptidg  45368  dvmulcncf  45376  dvdivcncf  45378  stoweidlem26  45477  stoweidlem50  45501  stoweidlem57  45508  aiotaval  46538  ndfatafv2nrn  46664  afv2ndefb  46667  funop1  46726  fun2dmnopgexmpl  46727  2ffzoeq  46771  iccpartiltu  46825  iccpartigtl  46826  zofldiv2ALTV  47065  evenprm2  47117  9fppr8  47140  stgoldbwt  47179  nnsum3primesle9  47197  nnsum4primeseven  47203  nnsum4primesevenALTV  47204  tgblthelfgott  47218  dfclnbgr6  47254  uspgrex  47324  0mgm  47340  nnsgrpmgm  47350  rngchomffvalALTV  47452  rhmsubcALTVlem1  47455  funcringcsetcALTV2lem4  47467  funcringcsetclem4ALTV  47490  srhmsubcALTV  47499  mapsnop  47520  zlmodzxzldeplem4  47683  zofldiv2  47716  fdivval  47724  nnlog2ge0lt1  47751  dig1  47793  itcoval2  47849  itcoval3  47850  mosn  47995  mo0  47996  mof02  48003  mofeu  48012  f102g  48016  f1mo  48017  f1omo  48025  intubeu  48107  unilbeu  48108  functhinclem1  48159  fullthinc  48164  thincciso  48167  indthinc  48170  indthincALT  48171