Theorem mpbiri 261

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 260	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  elimh  1099  spei  2426  nfald2  2477  nfabd2  2949  raleleq  3335  ceqsexv2d  3503  dedhb  3664  csbie2df  4404  ssdifeq0  4445  dedth  4544  pwidgOLD  4582  snidg  4621  rexreusng  4640  exsnrex  4641  ifpr  4654  rmosn  4680  rabrsn  4685  prid1g  4721  tpid1g  4730  tpid2g  4732  tpid3g  4733  sssn  4785  elpreqpr  4825  pwpw0  4834  unimax  4908  intmin3  4939  eqbrtrdi  5147  al0ssb  5265  vneqv  5273  rabelpw  5302  intabs  5314  difelpw  5319  0inp0  5324  axpr  5393  intidg  5429  copsexgw  5464  copsexgwOLD  5465  copsexg  5466  cotsexgw  5467  euotd  5490  elopab  5505  elvvuni  5733  posn  5742  frsn  5744  eqrelriv  5770  relsnb  5785  relopabiALT  5807  opabid2  5812  ididg  5837  iss  6039  cnveq0b  6204  dfpo2  6317  ord0eln0  6437  sucidg  6464  nsuceq0  6466  iotan0  6547  funopg  6594  fn0  6692  f00  6786  f0bi  6787  f10d  6882  f1o00  6883  fo00  6884  brprcneu  6898  brprcneuALT  6899  dffn5  6966  fsn  7160  funop  7177  funsndifnop  7179  eufnfv  7258  f1ounsn  7303  f1eqcocnv  7332  nfriotadw  7408  nfriotad  7411  riotaprop  7427  oprabidw  7474  oprabid  7475  elrnmpo  7580  ov6g  7608  ovelrn  7621  caovmo  7682  offn  7730  caofinvl  7749  fr3nr  7810  onprc  7816  ordeleqon  7820  onint0  7829  0elsuc  7870  onuninsuci  7875  orduninsuc  7878  ordzsl  7880  onzsl  7881  tfinds  7895  limomss  7906  limom  7917  peano5  7929  xpexr  7954  eqop2  8068  opreuopreu  8070  1stconst  8138  2ndconst  8139  frxp2  8188  frxp3  8195  funsssuppss  8235  dftpos3  8289  dftpos4  8290  oawordeulem  8590  omwordi  8607  nnmwordi  8672  riiner  8839  ecopover  8870  map0g  8940  mapsnd  8942  elixpsn  8993  en0  9073  en0ALT  9074  en0r  9075  en1  9079  snfi  9099  fiprc  9100  sbthlem2  9135  sbthlem4  9137  sbthlem5  9138  0domg  9151  findcard  9207  findcard2  9208  nneneq  9249  sdom1  9269  1sdom2dom  9273  fineqvlem  9285  nfielex  9293  enp1i  9298  elfiun  9449  marypha1lem  9452  oicl  9550  oif  9551  oion  9557  hartogslem1  9563  hartogs  9565  wemapso2  9574  card2on  9575  0wdom  9591  brwdom2  9594  elirrv  9618  inf3lem6  9661  cantnflem3  9719  cantnflem4  9720  wemapwe  9725  cnfcom  9728  ssttrcl  9743  ttrclselem2  9754  tctr  9766  r1tr  9810  r1rankidb  9839  r1pw  9886  elhf2  9937  scottex  9960  scottexOLD  9961  scott0b  9964  scott0OLD  9965  bnd2  9983  eldju2ndl  10032  tskwe  10058  oncard  10068  cardlim  10080  harsdom  10103  en2eleq  10114  dfac8alem  10135  dfac8b  10137  cardaleph  10195  iunfictbso  10220  infmap2  10322  ackbij1lem18  10341  cff  10352  cfsuc  10362  cff1  10363  cflim2  10368  cfss  10370  sdom2en01  10407  infpssrlem4  10411  fin23lem7  10421  fin23lem11  10422  isfin2-2  10424  fin23lem26  10430  fin23lem19  10441  fin23lem17  10443  isf34lem2  10478  isf34lem4  10482  fin1a2lem6  10510  fin1a2lem10  10514  fin1a2lem12  10516  itunifn  10522  hsmexlem1  10531  axcc2lem  10541  dcomex  10552  axdc3lem4  10558  ondomon  10674  konigthlem  10680  pwcfsdom  10695  cfpwsdom  10696  axpowndlem3  10711  canth4  10759  canthnumlem  10760  canthwelem  10762  canthwe  10763  canthp1lem2  10765  pwfseqlem4  10774  pwfseqlem5  10775  gchaleph  10783  gch2  10787  winainflem  10805  0tsk  10867  rankcf  10889  tskcard  10893  gruina  10930  grutsk  10934  tskmid  10952  indpi  11019  nqereu  11041  mulcanenq  11072  recmulnq  11076  archnq  11092  ltsopr  11144  1ne0sr  11208  0idsr  11209  00sr  11211  leid  11433  lelttric  11444  divcan3  12027  divid  12031  div0  12032  lemul1a  12198  nn1suc  12384  nn0n0n1ge2b  12702  xnn0xr  12711  xnn0nemnf  12717  0nn0m1nnn0  12780  nn0lt10b  12788  nn0ind-raph  12826  elnn1uz2  13079  indstr2  13081  uzsupss  13094  rpnnen1lem4  13135  rpnnen1lem5  13136  xrnemnf  13273  xrnepnf  13274  mnfltxr  13283  xnn0n0n1ge2b  13288  xnn0ge0  13290  xrlttri  13295  xrlttr  13296  xrleid  13307  qbtwnxr  13357  xmullem2  13422  xlemul1a  13445  xrub  13469  reltxrnmnf  13500  ixxun  13519  xnn0xrge0  13664  fztpval  13747  fseq1p1m1  13759  elfznelfzob  13936  ltweuz  14131  fzfi  14142  fsuppmapnn0fiubex  14162  ser0f  14225  0exp  14267  faclbnd4lem1  14464  bcn1  14484  hashnemnf  14515  hashv01gt1  14516  hashsnle1  14589  hashgt12el2  14595  hashpw  14608  hashf1  14629  fz1isolem  14633  hash2prb  14644  hash3tpb  14667  0wrd0  14712  wrdlen1  14726  ccatvalfn  14753  eqs1  14788  wrdl1exs1  14789  swrdlen  14823  swrdwrdsymb  14840  swrdspsleq  14843  cats1un  14898  wrdind  14899  wrd2ind  14900  swrdccatin1  14902  repswsymballbi  14959  cshw1  15001  scshwfzeqfzo  15005  wrdl2exs2  15126  trclfvcotr  15191  relexp1g  15208  relexp0rel  15219  relexprelg  15220  relexpreld  15222  sgnmulsgn  15291  sqrt0  15437  sqrtsq  15465  mptfzshft  15973  prodf1f  16090  egt2lt3  16403  0dvds  16475  nn0onn  16579  nn0o  16582  divalgmod  16605  flodddiv4  16614  bitsp1o  16632  gcddvds  16702  bezout  16745  lcmdvds  16812  rpdvds  16864  1nprm  16883  prmind2  16889  dvdszzq  16926  nnoddn2prmb  17020  pcpre1  17049  vdwapf  17179  vdwapid1  17182  ram0  17229  ramz  17232  prmolefac  17253  cshws0  17308  prmlem0  17312  strle1  17365  restsspw  17631  prdsdsfn  17665  imasdsfn  17715  imasaddfnlem  17729  imasvscafn  17738  xpsfrnel  17763  isacs1i  17860  cidfn  17882  fnhomeqhomf  17894  comffn  17908  isoval  17969  sscres  18027  cofucl  18092  idffth  18139  ressffth  18144  cat1lem  18300  catcoppccl  18321  estrchomfn  18338  funcestrcsetclem4  18346  funcestrcsetclem7  18349  equivestrcsetc  18355  funcsetcestrclem4  18361  funcsetcestrclem7  18364  1stfcl  18400  2ndfcl  18401  prfcl  18406  evlfcl  18425  curf1cl  18431  curfcl  18435  hofcl  18462  yonedainv  18484  pospo  18546  lubfun  18553  glbfun  18566  joindmss  18580  meetdmss  18594  ipopos  18739  acsficl2d  18755  dirref  18804  mgmidcl  18875  mgmlrid  18876  ielefmnd  19112  smndex1basss  19133  smndex1n0mnd  19140  degenmgm  19166  degenmgm2  19169  cntzssv  19572  idresperm  19630  symgvalstruct  19641  pmtrfmvdn0  19706  symggen  19714  psgnunilem1  19737  psgnprfval  19765  slwpgp  19857  frgpmhm  20009  frgpuptinv  20015  frgpup3lem  20021  gsumzoppg  20188  gsumcom2  20219  c0snmhm  20723  srhmsubc  20962  rhmsubclem1  20967  rrgsupp  20983  abv0  21110  zrhrhm  21847  psgnodpmr  21926  frlmphllem  22116  ellspd  22138  psrvscafval  22286  psrridm  22300  ltbwe  22383  psrbag0  22401  psrbagsn  22402  subrgascl  22405  psdmul  22517  mattpostpos  22799  mavmul0  22897  mavmul0g  22898  mdet0f1o  22938  m1detdiag  22942  m2detleiblem5  22970  m2detleiblem6  22971  m2detleiblem3  22974  m2detleiblem4  22975  maducoeval2  22985  d1mat2pmat  23087  chpmat1dlem  23183  chpmat1d  23184  baspartn  23302  eltg3  23310  topnex  23344  fctop  23352  cctop  23354  discld  23437  mretopd  23440  neipeltop  23477  neitr  23528  restcls  23529  ordtbaslem  23536  ordtuni  23538  idcn  23605  cnrmi  23708  cmpsublem  23747  cmpsub  23748  tgcmp  23749  uncmp  23751  hauscmplem  23754  cmpfi  23756  bwth  23758  1stcrestlem  23800  disllycmp  23847  dis1stc  23848  refref  23862  kgeni  23886  1stckgenlem  23902  kqffn  24074  snfil  24213  filconn  24232  cfinfil  24242  ufileu  24268  filufint  24269  fixufil  24271  cfinufil  24277  ufilen  24279  fin1aufil  24281  fmf  24294  rnelfm  24302  flimclslem  24333  hauspwpwf1  24336  supnfcls  24369  flimfnfcls  24377  fclscmp  24379  alexsubALTlem2  24397  alexsubALTlem3  24398  alexsubALT  24400  ptcmplem1  24401  cnextrel  24412  tsmsfbas  24477  ustref  24568  trust  24578  restutop  24586  isusp  24610  xmet0  24691  imasdsf1olem  24722  blfvalps  24732  blfps  24755  blf  24756  restmetu  24919  dscmet  24921  isngp2  24946  nm0  24978  nrginvrcn  25041  nmoix  25078  qdensere  25118  iccconn  25180  iccpnfcnv  25295  xrhmeo  25297  lebnumlem3  25314  metsscmetcld  25666  bcthlem5  25679  csschl  25727  rrxmfval  25757  minveclem3b  25779  cniccbdd  25812  ovolicc2lem4  25871  iunmbl  25904  ioorinv  25927  ioorcl  25928  i1f1lem  26040  limcvallem  26221  ellimc2  26227  limccnp  26241  limccnp2  26242  limcco  26243  perfdvf  26253  recnprss  26254  fncpn  26283  dvcmulf  26295  c1lip1  26347  lhop2  26365  q1pcl  26505  r1pdeglt  26508  ply1remlem  26513  plyssc  26548  ulm0  26748  cxpeq0  27036  cxplea  27054  cxplogb  27144  asinlem  27226  isppw2  27472  muval2  27491  dchrfi  27612  dchrpt  27624  bposlem6  27646  lgsdir2lem2  27683  lgsqr  27708  gausslemma2dlem4  27726  2lgslem2  27752  2lgslem3  27761  2lgs  27764  2sqlem7  27781  2sqlem11  27786  chtppilim  27832  nosgnn0i  28046  nolesgn2ores  28059  nogesgn1ores  28061  nosepnelem  28066  nosepdmlem  28070  nosupbnd1lem3  28097  nosupbnd1lem5  28099  nosupbnd2lem1  28102  noinfbnd1lem3  28112  noinfbnd1lem5  28114  noinfbnd2lem1  28117  oldval  28250  made0  28279  lrrecpo  28357  pncan2s  28490  divscan3d  28652  abssor  28662  om2noseqfo  28714  noseqrdglem  28721  noseqrdgfn  28722  noseqrdg0  28723  onsfi  28772  nohalf  28840  expsne0  28852  pw2divscan3d  28857  tgldimor  28995  tgcgr4  29024  tglnfn  29040  tglnunirn  29041  mirne  29169  mircinv  29170  perpln1  29215  perpln2  29216  tgplnfn  29283  lmiisolem  29331  prlngmid2  29469  xmstrkgc  29493  axcgrtr  29523  axsegconlem9  29533  axlowdimlem5  29554  axlowdimlem17  29566  axlowdim1  29567  uhgr0e  29679  edglnl  29751  uhgr0edgfi  29851  issubgr2  29883  subgrprop2  29885  egrsubgr  29888  0grsubgr  29889  0uhgrsubgr  29890  uhgrsubgrself  29891  nbgr1vtx  29969  nbgrssovtx  29972  nb3grprlem1  29991  uvtx01vtx  30008  cplgr1vlem  30040  cplgr1v  30041  usgrexilem  30051  wlkcomp  30241  wlk1walk  30249  wlkp1lem5  30286  pthhashvtx  30345  uhgrwkspthlem1  30369  pthdlem1  30382  clwlkcomp  30396  lfgrn1cycl  30424  uspgrn2crct  30427  wwlksn0s  30480  usgrwwlks2on  30577  umgrwwlks2on  30578  clwwlkn  30647  clwwlkn1  30662  0ewlk  30735  1ewlk  30736  0spth  30747  upgr1wlkdlem2  30767  wlk2v2e  30788  upgr3v3e3cycl  30811  upgr4cycl4dv4e  30816  eupth0  30845  frgr0v  30893  frgr1v  30902  1vwmgr  30907  ex-opab  31063  grpoinvf  31164  nvmid  31291  nmlnoubi  31428  hiidrcl  31727  hsn0elch  31880  shjshseli  32125  cmbr4i  32233  dfiop2  32385  kbpj  32588  nmopun  32646  adjeq0  32723  kbass2  32749  pjssdif1i  32807  pjinvari  32823  pjcmul2i  32834  pj3i  32840  stge1i  32870  stle0i  32871  sumdmdlem2  33051  dmdbr6ati  33055  dmdbr7ati  33056  rabsnel  33168  unidifsnel  33203  unidifsnne  33204  disjdifprg  33241  ofoprabco  33330  padct  33381  fpwrelmapffslem  33394  nn0mnfxrd  33413  xrlelttric  33414  xnn0gt0  33431  iundisj2cnt  33461  f1ocnt  33462  fz1nnct  33463  fz1nntr  33464  hashxpe  33469  nn0min  33482  sgnmulsgp  33493  wrdt2ind  33586  xrge0tsmsbi  33705  opprabs  34076  rtelextdg2lem  34428  2sqr3minply  34482  locfinref  34543  dispcmp  34561  zartopn  34577  zarcmplem  34583  pstmxmet  34599  xrge0iifcnv  34635  xrge0iif1  34640  qqhre  34722  esumcl  34732  esumpr2  34769  esumpinfval  34775  esumpcvgval  34780  ofcfn  34802  pwsiga  34832  prsiga  34833  sigainb  34839  ldgenpisyslem1  34866  measiuns  34920  relfae  34950  pmeasmono  35026  sitgf  35049  eulerpartgbij  35074  signswch  35260  signslema  35261  signstlen  35266  signstfvn  35268  circlevma  35341  bnj216  35433  bnj151  35577  bnj517  35585  bnj970  35647  bnj1145  35693  bnj1498  35761  eqhf  35820  rankscottu  35839  fineqvrep  35882  fineqvac  35884  fineqvnttrclselem1  35889  fineqvnttrclselem2  35890  fineqvnttrclse  35892  fineqvinfep  35893  eqhfregs  35905  kard0b  35927  rankkardu  35939  dfk12  36012  dfk22  36013  dfk32  36014  wevgblacfn  36039  vonf1osev  36040  acycgr0v  36070  prclisacycgr  36073  umgracycusgr  36076  cusgracyclt3v  36078  subfacp1lem5  36116  erdszelem8  36130  kur14lem1  36138  indispconn  36166  cvmsss2  36206  satfvsuclem2  36292  satfrel  36299  satfrnmapom  36302  satfv0fun  36303  satf00  36306  satf0suclem  36307  fmlasuc0  36316  msubrn  36461  onprcr  36631  dfon2lem7  36729  brbigcup  36838  elsingles  36858  fnimage  36869  funpartlem  36884  dfrdg4  36893  imagesset  36895  altopthsn  36904  elaltxp  36918  ellines  37095  linethru  37096  rankeq1o  37110  hfninf  37113  nn0prpwlem  37288  fneref  37316  neibastop2lem  37326  limsucncmpi  37411  tz9.1tco  37449  bj-exlimmpbir  38004  curryset  38037  bj-snglex  38064  bj-axnul  38179  bj-restpw  38204  bj-inftyexpidisj  38323  topdifinffinlem  38462  relowlssretop  38478  rdgeqoa  38485  finxpreclem6  38511  fvineqsneq  38527  pibt2  38532  poimirlem23  38753  poimirlem29  38759  poimirlem31  38761  volsupnfl  38775  cnambfre  38778  dvasin  38814  dvacos  38815  sdclem2  38868  sstotbnd2  38900  ssbnd  38914  ismgmOLD  38976  grpokerinj  39019  rngomndo  39061  isdrngo1  39082  ac6s6  39296  iss2  39468  relecxrn  39531  sucmapsuc  39613  cosselrels  39699  cnvelrels  39700  brssrid  39706  brcnvssrid  39711  dfdisjs5  39921  eldisjs5  39947  eldisjsim3  40061  mpets2  40079  pets  40090  prtlem12  40116  riotasv2d  40206  lkrscss  40347  islshpkrN  40369  isline  40988  ispointN  40991  0psubN  40998  linepsubN  41001  atpsubN  41002  cdlemk36  42162  diafn  42283  dibfna  42403  dibvalrel  42412  dicvalrelN  42434  diclspsn  42443  dihvalrel  42528  dih1  42535  lclkrlem1  42755  lclkr  42782  mapd1o  42897  mapdin  42911  hdmapfnN  43078  hgmapfnN  43137  lcmineqlem10  43280  sticksstones9  43396  sn-iotalem  43468  readvrec2  43605  readvrec  43606  repncan2  43626  elrfirn  43899  ismrcd1  43902  istopclsd  43904  rabren3dioph  44015  jm2.17b  44161  jm2.22  44195  jm2.23  44196  ttac  44236  pw2f1ocnv  44237  dnnumch1  44244  hbtlem5  44322  mncn0  44333  aaitgo  44356  rngunsnply  44363  unielss  44412  onexlimgt  44437  cantnfresb  44518  dflim5  44523  naddwordnexlem4  44595  safesnsupfiss  44608  safesnsupfidom1o  44610  safesnsupfilb  44611  ensucne0OLD  44723  clcnvlem  44815  relexp01min  44905  ntrf  45315  ssrecnpr  45484  seff  45485  sblpnf  45486  nzss  45493  dvconstbi  45510  ipo0  45623  ifr0  45624  addrfn  45645  subrfn  45646  mulvfn  45647  wfaxrep  46179  refsum2cnlem1  46259  rn1st  46490  ellimciota  46831  dvmptconst  47130  dvmptidg  47132  dvmulcncf  47140  dvdivcncf  47142  stoweidlem26  47241  stoweidlem50  47265  stoweidlem57  47272  tannpoly  48145  tmachlem-agreefin  48163  aiotaval  48370  ndfatafv2nrn  48496  afv2ndefb  48499  funop1  48558  fun2dmnopgexmpl  48559  2ffzoeq  48603  2ltceilhalf  48607  m1modne  48629  iccpartiltu  48709  iccpartigtl  48710  zofldiv2ALTV  48965  evenprm2  49017  9fppr8  49040  stgoldbwt  49079  nnsum3primesle9  49097  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  tgblthelfgott  49118  dfclnbgr6  49159  cycl3grtri  49250  grtrimap  49251  stgredgel  49260  stgr1  49264  isubgr3stgrlem2  49270  isubgr3stgrlem3  49271  usgrexmpl2trifr  49340  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem2  49375  gpg5nbgrvtx13starlem3  49376  gpg5nbgr3star  49384  gpg3kgrtriex  49392  uspgrex  49453  0mgm  49468  nnsgrpmgm  49478  rngchomffvalALTV  49580  rhmsubcALTVlem1  49583  funcringcsetcALTV2lem4  49595  funcringcsetclem4ALTV  49618  srhmsubcALTV  49627  mapsnop  49661  zlmodzxzldeplem4  49820  zofldiv2  49848  fdivval  49856  nnlog2ge0lt1  49883  dig1  49925  itcoval2  49981  itcoval3  49982  mosn  50129  mo0  50130  mof02  50155  mofeu  50164  f102g  50168  f1mo  50169  tposres0  50195  f1omo  50212  f1omoOLD  50213  resipos  50294  intubeu  50303  unilbeu  50304  sectfn  50348  nelsubclem  50386  idfu1stf1o  50420  imaidfu  50431  oppfvallem  50456  funcoppc3  50468  idfth  50479  idsubc  50481  uptposlem  50518  swapf2fn  50595  swapf1f1o  50602  swapf2f1o  50603  swapf2f1oaALT  50605  fucof1  50649  fucofn2  50651  fucofn22  50667  reldmprcof1  50721  reldmprcof2  50722  fucoppcid  50748  fucoppc  50750  functhinclem1  50784  fullthinc  50790  thincciso  50793  indcthing  50800  indthinc  50802  indthincALT  50803  functermc  50848  discsntermlem  50913  reldmlan2  51005  reldmran2  51006  rellan  51011  relran  51012  termolmd  51058  veronesev1lem  51253  veronesev2lem  51254  veronesev3lem  51255  veronesev4lem  51256  veronesev5lem  51257  veronesev6lem  51258  veronesevrowd  51259  veronesematrowd  51261