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  2423  nfald2  2474  nfabd2  2945  raleleq  3331  ceqsexv2d  3499  dedhb  3660  csbie2df  4400  ssdifeq0  4441  dedth  4540  pwidgOLD  4577  snidg  4620  rexreusng  4639  exsnrex  4640  ifpr  4653  rmosn  4679  rabrsn  4684  prid1g  4720  tpid1g  4729  tpid2g  4731  tpid3g  4732  pwpw0  4773  sssn  4786  elpreqpr  4826  unimax  4904  intmin3  4935  eqbrtrdi  5143  al0ssb  5261  vneqv  5269  rabelpw  5297  intabs  5309  difelpw  5314  0inp0  5319  axpr  5388  intidg  5424  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  euotd  5482  elopab  5497  elvvuni  5724  posn  5733  frsn  5735  eqrelriv  5761  relsnb  5776  relopabiALT  5797  opabid2  5802  ididg  5827  iss  6025  dfpo2  6288  ord0eln0  6408  sucidg  6435  nsuceq0  6437  funopg  6562  fn0  6658  f00  6752  f0bi  6753  f10d  6847  f1o00  6848  fo00  6849  brprcneu  6863  brprcneuALT  6864  dffn5  6931  fsn  7124  funop  7141  funsndifnop  7143  fnsnbOLD  7159  eufnfv  7223  f1ounsn  7268  f1eqcocnv  7297  nfriotadw  7373  nfriotad  7376  riotaprop  7392  oprabidw  7439  oprabid  7440  elrnmpo  7544  ov6g  7572  ovelrn  7585  caovmo  7646  offn  7689  caofinvl  7708  fr3nr  7769  onprc  7775  ordeleqon  7779  onint0  7788  0elsuc  7829  onuninsuci  7834  orduninsuc  7837  ordzsl  7839  onzsl  7840  tfinds  7854  limomss  7865  limom  7876  peano5  7888  xpexr  7913  eqop2  8027  opreuopreu  8029  1stconst  8094  2ndconst  8095  frxp2  8139  frxp3  8146  funsssuppss  8185  dftpos3  8239  dftpos4  8240  oawordeulem  8540  omwordi  8557  nnmwordi  8622  riiner  8789  ecopover  8820  map0g  8890  mapsnd  8892  elixpsn  8943  en0  9023  en0ALT  9024  en0r  9025  en1  9029  snfi  9049  fiprc  9050  sbthlem2  9085  sbthlem4  9087  sbthlem5  9088  0domg  9101  findcard  9157  findcard2  9158  nneneq  9199  sdom1  9219  1sdom2dom  9223  fineqvlem  9235  nfielex  9243  enp1i  9248  elfiun  9400  marypha1lem  9403  oicl  9501  oif  9502  oion  9508  hartogslem1  9514  hartogs  9516  wemapso2  9525  card2on  9526  0wdom  9542  brwdom2  9545  elirrv  9569  inf3lem6  9612  cantnflem3  9670  cantnflem4  9671  wemapwe  9676  cnfcom  9679  ssttrcl  9694  ttrclselem2  9705  tctr  9717  r1tr  9758  r1rankidb  9786  r1pw  9832  elhf2  9882  scottex  9905  scottexOLD  9906  scott0b  9909  scott0OLD  9910  bnd2  9928  eldju2ndl  9977  tskwe  10003  oncard  10013  cardlim  10025  harsdom  10048  en2eleq  10059  dfac8alem  10080  dfac8b  10082  cardaleph  10140  iunfictbso  10165  infmap2  10267  ackbij1lem18  10286  cff  10297  cfsuc  10307  cff1  10308  cflim2  10313  cfss  10315  sdom2en01  10352  infpssrlem4  10356  fin23lem7  10366  fin23lem11  10367  isfin2-2  10369  fin23lem26  10375  fin23lem19  10386  fin23lem17  10388  isf34lem2  10423  isf34lem4  10427  fin1a2lem6  10455  fin1a2lem10  10459  fin1a2lem12  10461  itunifn  10467  hsmexlem1  10476  axcc2lem  10486  dcomex  10497  axdc3lem4  10503  ondomon  10619  konigthlem  10625  pwcfsdom  10640  cfpwsdom  10641  axpowndlem3  10656  canth4  10704  canthnumlem  10705  canthwelem  10707  canthwe  10708  canthp1lem2  10710  pwfseqlem4  10719  pwfseqlem5  10720  gchaleph  10728  gch2  10732  winainflem  10750  0tsk  10812  rankcf  10834  tskcard  10838  gruina  10875  grutsk  10879  tskmid  10897  indpi  10964  nqereu  10986  mulcanenq  11017  recmulnq  11021  archnq  11037  ltsopr  11089  1ne0sr  11153  0idsr  11154  00sr  11156  leid  11378  lelttric  11389  divcan3  11970  divid  11974  div0  11975  lemul1a  12141  nn1suc  12327  nn0n0n1ge2b  12645  xnn0xr  12654  xnn0nemnf  12660  0nn0m1nnn0  12723  nn0lt10b  12731  nn0ind-raph  12769  elnn1uz2  13022  indstr2  13024  uzsupss  13037  rpnnen1lem4  13078  rpnnen1lem5  13079  xrnemnf  13216  xrnepnf  13217  mnfltxr  13226  xnn0n0n1ge2b  13231  xnn0ge0  13233  xrlttri  13238  xrlttr  13239  xrleid  13250  qbtwnxr  13300  xmullem2  13365  xlemul1a  13388  xrub  13412  reltxrnmnf  13443  ixxun  13462  xnn0xrge0  13607  fztpval  13689  fseq1p1m1  13701  elfznelfzob  13878  ltweuz  14073  fzfi  14084  fsuppmapnn0fiubex  14104  ser0f  14167  0exp  14209  faclbnd4lem1  14405  bcn1  14425  hashnemnf  14456  hashv01gt1  14457  hashsnle1  14530  hashgt12el2  14536  hashpw  14549  hashf1  14570  fz1isolem  14574  hash2prb  14585  hash3tpb  14608  0wrd0  14653  wrdlen1  14667  ccatvalfn  14694  eqs1  14728  wrdl1exs1  14729  swrdlen  14763  swrdwrdsymb  14780  swrdspsleq  14783  cats1un  14838  wrdind  14839  wrd2ind  14840  swrdccatin1  14842  repswsymballbi  14899  cshw1  14941  scshwfzeqfzo  14945  wrdl2exs2  15065  trclfvcotr  15130  relexp1g  15147  relexp0rel  15158  relexprelg  15159  relexpreld  15161  sgnmulsgn  15230  sqrt0  15376  sqrtsq  15404  mptfzshft  15912  prodf1f  16029  egt2lt3  16342  0dvds  16414  nn0onn  16518  nn0o  16521  divalgmod  16544  flodddiv4  16553  bitsp1o  16571  gcddvds  16641  bezout  16681  lcmdvds  16746  rpdvds  16798  1nprm  16817  prmind2  16823  dvdszzq  16860  nnoddn2prmb  16953  pcpre1  16982  vdwapf  17112  vdwapid1  17115  ram0  17162  ramz  17165  prmolefac  17186  cshws0  17241  prmlem0  17245  strle1  17298  restsspw  17564  prdsdsfn  17598  imasdsfn  17648  imasaddfnlem  17662  imasvscafn  17671  xpsfrnel  17696  isacs1i  17793  cidfn  17815  fnhomeqhomf  17827  comffn  17841  isoval  17902  sscres  17960  cofucl  18025  idffth  18072  ressffth  18077  cat1lem  18233  catcoppccl  18254  estrchomfn  18271  funcestrcsetclem4  18279  funcestrcsetclem7  18282  equivestrcsetc  18288  funcsetcestrclem4  18294  funcsetcestrclem7  18297  1stfcl  18333  2ndfcl  18334  prfcl  18339  evlfcl  18358  curf1cl  18364  curfcl  18368  hofcl  18395  yonedainv  18417  pospo  18479  lubfun  18486  glbfun  18499  joindmss  18513  meetdmss  18527  ipopos  18672  acsficl2d  18688  dirref  18737  mgmidcl  18808  mgmlrid  18809  ielefmnd  19045  smndex1basss  19066  smndex1n0mnd  19073  degenmgm  19099  degenmgm2  19102  cntzssv  19504  idresperm  19562  symgvalstruct  19573  pmtrfmvdn0  19638  symggen  19646  psgnunilem1  19669  psgnprfval  19697  slwpgp  19789  frgpmhm  19941  frgpuptinv  19947  frgpup3lem  19953  gsumzoppg  20120  gsumcom2  20151  c0snmhm  20655  srhmsubc  20894  rhmsubclem1  20899  rrgsupp  20915  abv0  21042  zrhrhm  21779  psgnodpmr  21858  frlmphllem  22048  ellspd  22070  psrvscafval  22218  psrridm  22232  ltbwe  22315  psrbag0  22333  psrbagsn  22334  subrgascl  22337  psdmul  22449  mattpostpos  22731  mavmul0  22829  mavmul0g  22830  mdet0f1o  22870  m1detdiag  22874  m2detleiblem5  22902  m2detleiblem6  22903  m2detleiblem3  22906  m2detleiblem4  22907  maducoeval2  22917  d1mat2pmat  23019  chpmat1dlem  23115  chpmat1d  23116  baspartn  23234  eltg3  23242  topnex  23276  fctop  23284  cctop  23286  discld  23369  mretopd  23372  neipeltop  23409  neitr  23460  restcls  23461  ordtbaslem  23468  ordtuni  23470  idcn  23537  cnrmi  23640  cmpsublem  23679  cmpsub  23680  tgcmp  23681  uncmp  23683  hauscmplem  23686  cmpfi  23688  bwth  23690  1stcrestlem  23732  disllycmp  23779  dis1stc  23780  refref  23794  kgeni  23818  1stckgenlem  23834  kqffn  24006  snfil  24145  filconn  24164  cfinfil  24174  ufileu  24200  filufint  24201  fixufil  24203  cfinufil  24209  ufilen  24211  fin1aufil  24213  fmf  24226  rnelfm  24234  flimclslem  24265  hauspwpwf1  24268  supnfcls  24301  flimfnfcls  24309  fclscmp  24311  alexsubALTlem2  24329  alexsubALTlem3  24330  alexsubALT  24332  ptcmplem1  24333  cnextrel  24344  tsmsfbas  24409  ustref  24500  trust  24510  restutop  24518  isusp  24542  xmet0  24623  imasdsf1olem  24654  blfvalps  24664  blfps  24687  blf  24688  restmetu  24851  dscmet  24853  isngp2  24878  nm0  24910  nrginvrcn  24973  nmoix  25010  qdensere  25050  iccconn  25112  iccpnfcnv  25227  xrhmeo  25229  lebnumlem3  25246  metsscmetcld  25598  bcthlem5  25611  csschl  25659  rrxmfval  25689  minveclem3b  25711  cniccbdd  25744  ovolicc2lem4  25803  iunmbl  25836  ioorinv  25859  ioorcl  25860  i1f1lem  25972  limcvallem  26153  ellimc2  26159  limccnp  26173  limccnp2  26174  limcco  26175  perfdvf  26185  recnprss  26186  fncpn  26215  dvcmulf  26227  c1lip1  26279  lhop2  26297  q1pcl  26437  r1pdeglt  26440  ply1remlem  26445  plyssc  26480  ulm0  26682  cxpeq0  26970  cxplea  26988  cxplogb  27078  asinlem  27160  isppw2  27406  muval2  27425  dchrfi  27546  dchrpt  27558  bposlem6  27580  lgsdir2lem2  27617  lgsqr  27642  gausslemma2dlem4  27660  2lgslem2  27686  2lgslem3  27695  2lgs  27698  2sqlem7  27715  2sqlem11  27720  chtppilim  27766  nosgnn0i  27950  nolesgn2ores  27963  nogesgn1ores  27965  nosepnelem  27970  nosepdmlem  27974  nosupbnd1lem3  28001  nosupbnd1lem5  28003  nosupbnd2lem1  28006  noinfbnd1lem3  28016  noinfbnd1lem5  28018  noinfbnd2lem1  28021  oldval  28154  made0  28183  lrrecpo  28261  pncan2s  28394  divscan3d  28556  abssor  28566  om2noseqfo  28618  noseqrdglem  28625  noseqrdgfn  28626  noseqrdg0  28627  onsfi  28676  nohalf  28744  expsne0  28756  pw2divscan3d  28761  tgldimor  28899  tgcgr4  28928  tglnfn  28944  tglnunirn  28945  mirne  29073  mircinv  29074  perpln1  29119  perpln2  29120  tgplnfn  29187  lmiisolem  29235  prlngmid2  29373  xmstrkgc  29397  axcgrtr  29427  axsegconlem9  29437  axlowdimlem5  29458  axlowdimlem17  29470  axlowdim1  29471  uhgr0e  29583  edglnl  29655  uhgr0edgfi  29755  issubgr2  29787  subgrprop2  29789  egrsubgr  29792  0grsubgr  29793  0uhgrsubgr  29794  uhgrsubgrself  29795  nbgr1vtx  29873  nbgrssovtx  29876  nb3grprlem1  29895  uvtx01vtx  29912  cplgr1vlem  29944  cplgr1v  29945  usgrexilem  29955  wlkcomp  30145  wlk1walk  30153  wlkp1lem5  30190  pthhashvtx  30249  uhgrwkspthlem1  30273  pthdlem1  30286  clwlkcomp  30300  lfgrn1cycl  30328  uspgrn2crct  30331  wwlksn0s  30384  usgrwwlks2on  30481  umgrwwlks2on  30482  clwwlkn  30551  clwwlkn1  30566  0ewlk  30639  1ewlk  30640  0spth  30651  upgr1wlkdlem2  30671  wlk2v2e  30692  upgr3v3e3cycl  30715  upgr4cycl4dv4e  30720  eupth0  30749  frgr0v  30797  frgr1v  30806  1vwmgr  30811  ex-opab  30967  grpoinvf  31068  nvmid  31195  nmlnoubi  31332  hiidrcl  31631  hsn0elch  31784  shjshseli  32029  cmbr4i  32137  dfiop2  32289  kbpj  32492  nmopun  32550  adjeq0  32627  kbass2  32653  pjssdif1i  32711  pjinvari  32727  pjcmul2i  32738  pj3i  32744  stge1i  32774  stle0i  32775  sumdmdlem2  32955  dmdbr6ati  32959  dmdbr7ati  32960  rabsnel  33030  unidifsnel  33065  unidifsnne  33066  disjdifprg  33103  ofoprabco  33192  padct  33244  fpwrelmapffslem  33258  nn0mnfxrd  33277  xrlelttric  33278  xnn0gt0  33295  iundisj2cnt  33325  f1ocnt  33326  fz1nnct  33327  fz1nntr  33328  hashxpe  33333  nn0min  33346  sgnmulsgp  33357  wrdt2ind  33450  xrge0tsmsbi  33569  opprabs  33940  rtelextdg2lem  34292  2sqr3minply  34346  locfinref  34407  dispcmp  34425  zartopn  34441  zarcmplem  34447  pstmxmet  34463  xrge0iifcnv  34499  xrge0iif1  34504  qqhre  34586  esumcl  34596  esumpr2  34633  esumpinfval  34639  esumpcvgval  34644  ofcfn  34666  pwsiga  34696  prsiga  34697  sigainb  34703  ldgenpisyslem1  34730  measiuns  34784  relfae  34814  pmeasmono  34891  sitgf  34914  eulerpartgbij  34939  signswch  35125  signslema  35126  signstlen  35131  signstfvn  35133  circlevma  35206  bnj216  35298  bnj151  35442  bnj517  35450  bnj970  35512  bnj1145  35558  bnj1498  35626  r1omhfb  35669  rankscottu  35683  fineqvrep  35707  fineqvac  35709  fineqvnttrclselem1  35714  fineqvnttrclselem2  35715  fineqvnttrclse  35717  fineqvinfep  35718  r1omhfbregs  35730  kard0b  35752  rankkardu  35764  wevgblacfn  35815  vonf1osev  35816  acycgr0v  35834  prclisacycgr  35837  umgracycusgr  35840  cusgracyclt3v  35842  subfacp1lem5  35870  erdszelem8  35884  kur14lem1  35892  indispconn  35920  cvmsss2  35960  satfvsuclem2  36046  satfrel  36053  satfrnmapom  36056  satfv0fun  36057  satf00  36060  satf0suclem  36061  fmlasuc0  36070  msubrn  36215  dfon2lem7  36473  brbigcup  36582  elsingles  36602  fnimage  36613  funpartlem  36628  dfrdg4  36637  imagesset  36639  altopthsn  36648  elaltxp  36662  ellines  36839  linethru  36840  rankeq1o  36854  hfninf  36857  nn0prpwlem  37032  fneref  37060  neibastop2lem  37070  limsucncmpi  37155  tz9.1tco  37193  bj-exlimmpbir  37748  curryset  37781  bj-snglex  37808  bj-axnul  37908  bj-restpw  37933  bj-inftyexpidisj  38051  topdifinffinlem  38190  relowlssretop  38206  rdgeqoa  38213  finxpreclem6  38239  fvineqsneq  38255  pibt2  38260  poimirlem23  38481  poimirlem29  38487  poimirlem31  38489  volsupnfl  38503  cnambfre  38506  dvasin  38542  dvacos  38543  sdclem2  38596  sstotbnd2  38628  ssbnd  38642  ismgmOLD  38704  grpokerinj  38747  rngomndo  38789  isdrngo1  38810  ac6s6  39024  iss2  39196  relecxrn  39259  sucmapsuc  39341  cosselrels  39427  cnvelrels  39428  brssrid  39434  brcnvssrid  39439  dfdisjs5  39649  eldisjs5  39675  eldisjsim3  39789  mpets2  39807  pets  39818  prtlem12  39844  riotasv2d  39934  lkrscss  40075  islshpkrN  40097  isline  40716  ispointN  40719  0psubN  40726  linepsubN  40729  atpsubN  40730  cdlemk36  41890  diafn  42011  dibfna  42131  dibvalrel  42140  dicvalrelN  42162  diclspsn  42171  dihvalrel  42256  dih1  42263  lclkrlem1  42483  lclkr  42510  mapd1o  42625  mapdin  42639  hdmapfnN  42806  hgmapfnN  42865  lcmineqlem10  43008  sticksstones9  43124  sn-iotalem  43195  readvrec2  43340  readvrec  43341  repncan2  43361  elrfirn  43644  ismrcd1  43647  istopclsd  43649  rabren3dioph  43760  jm2.17b  43906  jm2.22  43940  jm2.23  43941  ttac  43981  pw2f1ocnv  43982  dnnumch1  43989  hbtlem5  44073  mncn0  44084  aaitgo  44107  rngunsnply  44114  unielss  44163  onexlimgt  44188  cantnfresb  44269  dflim5  44274  naddwordnexlem4  44346  safesnsupfiss  44359  safesnsupfidom1o  44361  safesnsupfilb  44362  ensucne0OLD  44474  clcnvlem  44567  relexp01min  44657  ntrf  45067  ssrecnpr  45236  seff  45237  sblpnf  45238  nzss  45245  dvconstbi  45262  ipo0  45376  ifr0  45377  addrfn  45398  subrfn  45399  mulvfn  45400  wfaxrep  45921  refsum2cnlem1  45975  rn1st  46206  ellimciota  46548  dvmptconst  46847  dvmptidg  46849  dvmulcncf  46857  dvdivcncf  46859  stoweidlem26  46958  stoweidlem50  46982  stoweidlem57  46989  tannpoly  47862  tmachlem-agreefin  47880  aiotaval  48087  ndfatafv2nrn  48213  afv2ndefb  48216  funop1  48275  fun2dmnopgexmpl  48276  2ffzoeq  48320  2ltceilhalf  48324  m1modne  48346  iccpartiltu  48426  iccpartigtl  48427  zofldiv2ALTV  48682  evenprm2  48734  9fppr8  48757  stgoldbwt  48796  nnsum3primesle9  48814  nnsum4primeseven  48820  nnsum4primesevenALTV  48821  tgblthelfgott  48835  dfclnbgr6  48876  cycl3grtri  48967  grtrimap  48968  stgredgel  48977  stgr1  48981  isubgr3stgrlem2  48987  isubgr3stgrlem3  48988  usgrexmpl2trifr  49057  gpg5nbgrvtx13starlem1  49091  gpg5nbgrvtx13starlem2  49092  gpg5nbgrvtx13starlem3  49093  gpg5nbgr3star  49101  gpg3kgrtriex  49109  uspgrex  49170  0mgm  49185  nnsgrpmgm  49195  rngchomffvalALTV  49297  rhmsubcALTVlem1  49300  funcringcsetcALTV2lem4  49312  funcringcsetclem4ALTV  49335  srhmsubcALTV  49344  mapsnop  49378  zlmodzxzldeplem4  49537  zofldiv2  49565  fdivval  49573  nnlog2ge0lt1  49600  dig1  49642  itcoval2  49698  itcoval3  49699  mosn  49845  mo0  49846  mof02  49871  mofeu  49880  f102g  49884  f1mo  49885  tposres0  49907  f1omo  49923  f1omoOLD  49924  resipos  50005  intubeu  50014  unilbeu  50015  sectfn  50059  nelsubclem  50097  idfu1stf1o  50129  imaidfu  50140  oppfvallem  50165  funcoppc3  50177  idfth  50188  idsubc  50190  uptposlem  50227  swapf2fn  50298  swapf1f1o  50305  swapf2f1o  50306  swapf2f1oaALT  50308  fucof1  50352  fucofn2  50354  fucofn22  50370  reldmprcof1  50411  reldmprcof2  50412  fucoppcid  50438  fucoppc  50440  functhinclem1  50474  fullthinc  50480  thincciso  50483  indcthing  50490  indthinc  50492  indthincALT  50493  functermc  50538  discsntermlem  50600  reldmlan2  50647  reldmran2  50648  rellan  50653  relran  50654  termolmd  50700  veronesev1lem  50895  veronesev2lem  50896  veronesev3lem  50897  veronesev4lem  50898  veronesev5lem  50899  veronesev6lem  50900  veronesevrowd  50901  veronesematrowd  50903