Theorem impbid 211

Description: Deduce an equivalence from two implications. Deduction associated with impbi 207 and impbii 208. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 210. (Revised by Wolf Lammen, 3-Nov-2012.)

Hypotheses

Ref	Expression
impbid.1	⊢ (𝜑 → (𝜓 → 𝜒))
impbid.2	⊢ (𝜑 → (𝜒 → 𝜓))

Assertion

Ref	Expression
impbid	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impbid.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	1, 2	impbid21d 210	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 52	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:  bicom1  220  impbid1  224  impcon4bid  226  pm5.74  270  imbi1d  341  pm5.501  366  impbida  798  dedlem0b  1042  dedlema  1043  dedlemb  1044  albi  1819  alexbii  1834  equequ1  2027  equequ2  2028  spsbbi  2075  elequ1  2112  elequ2  2120  sbequ12  2242  sbft  2260  cbv2w  2332  exsb  2354  dral1v  2365  dral1vOLD  2366  cbv2  2401  cbv2h  2404  ax12b  2422  dral1  2437  dral1ALT  2438  eupickb  2630  eupickbi  2631  2eu2  2647  ralbi  3102  rexbi  3103  ralbida  3266  ceqsalt  3505  rspcebdv  3606  ceqex  3640  mob2  3711  reu6  3722  sbciegft  3815  sbcg  3856  2reu2  3892  csbiebt  3923  sseq1  4007  ss2abdv  4060  ssdifsym  4263  reupick  4318  reupick2  4320  ab0OLD  4375  uneqdifeq  4492  prnebg  4856  preqsnd  4859  prel12g  4864  iuneqconst  5008  disjeq2  5117  disjeq1  5120  disjss3  5147  reusv2lem2  5397  reusv2lem3  5398  alxfr  5405  ralxfrd  5406  ralxfrd2  5410  copsexgw  5490  copsexg  5491  snopeqop  5506  euotd  5513  poeq2  5592  sotric  5616  sotrieq  5617  freq2  5647  seeq1  5648  seeq2  5649  iss  6035  tz7.7  6390  ordtri1  6397  ordelinel  6465  iotavalOLD  6517  funeq  6568  funssres  6592  f0dom0  6775  tz6.12cOLD  6918  fnbrfvb  6944  ssimaex  6976  fvimacnv  7054  elpreima  7059  eldmrexrnb  7093  fsn  7135  fnsnb  7166  fmptsng  7168  fmptsnd  7169  fprb  7197  tpres  7204  fconst2g  7206  fconst5  7209  elunirn  7253  f1ocnvfvb  7280  f1prex  7285  foeqcnvco  7301  f1eqcocnv  7302  f1eqcocnvOLD  7303  fliftfun  7312  soisores  7327  isofr  7342  isose  7343  isopo  7346  isoso  7348  f1oiso2  7352  eusvobj2  7404  oprabidw  7443  oprabid  7444  f1opw2  7665  oneqmin  7792  ordsucOLD  7806  ordelsuc  7812  ordsucelsuc  7814  ordunisuc2  7837  limsuc  7842  fndmexb  7903  f1ovv  7948  op1steq  8023  opreuopreu  8024  funeldmdif  8038  fvn0elsuppb  8171  extmptsuppeq  8178  rntpos  8230  smoiso2  8375  seqomlem2  8457  oaord  8553  oawordex  8563  oaordex  8564  omord2  8573  om00  8581  oeord  8594  nnaord  8625  nnmord  8638  nnawordex  8643  nnaordex  8644  eldifsucnn  8669  erexb  8734  swoord1  8740  swoord2  8741  iiner  8789  eceqoveq  8822  mapsnd  8886  ralxpmap  8896  omxpenlem  9079  domtriord  9129  mapxpen  9149  mapunen  9152  ssenen  9157  enfi  9196  nneneq  9215  nndomog  9222  nneneqOLD  9227  nndomogOLD  9232  onomeneq  9234  onomeneqOLD  9235  en1eqsnbi  9282  fodomfib  9332  f1opwfi  9362  fsuppunbi  9390  elfiun  9431  suplub2  9462  ordiso2  9516  ordiso  9517  oieu  9540  brwdom2  9574  brwdom3  9583  cantnflem1  9690  ttrclselem2  9727  cardidm  9960  carddom2  9978  pm54.43  10002  pr2neOLD  10006  acnen  10054  acnen2  10056  alephord  10076  alephinit  10096  dfac5  10129  infdif2  10211  fictb  10246  coflim  10262  fincssdom  10324  fin23lem25  10325  isf32lem9  10362  isf34lem4  10378  fin1a2lem11  10411  axdc3lem2  10452  ficard  10566  fpwwe2lem11  10642  fpwwe2  10644  indpi  10908  nqereq  10936  1idpr  11030  ltapr  11046  leltne  11310  ltlen  11322  ltadd2  11325  addlsub  11637  addid0  11640  ltord1  11747  mul0or  11861  ldiv  12055  ltmul1  12071  mulge0b  12091  lt2msq  12106  negfi  12170  nnsub  12263  nn0sub  12529  zrevaddcl  12614  zltp1le  12619  zdiv  12639  nneo  12653  zeo2  12656  zmax  12936  zbtwnre  12937  qrevaddcl  12962  xrlttri  13125  xrleltne  13131  xralrple  13191  xltneg  13203  xleadd1  13241  xlemul1  13276  supxrunb1  13305  supxrunb2  13306  ioo0  13356  iccid  13376  ico0  13377  ioc0  13378  icc0  13379  difreicc  13468  iccsplit  13469  zltaddlt1le  13489  0fz1  13528  uzsplit  13580  fzm1  13588  fzrevral  13593  ssfzo12bi  13734  elfznelfzob  13745  flge  13777  modid2  13870  modmuladd  13885  ssnn0fi  13957  seqf1olem1  14014  hashen  14314  hashdom  14346  hash2exprb  14439  pr2pwpr  14447  hashtpg  14453  len0nnbi  14508  ccats1pfxeqbi  14699  reuccatpfxs1  14704  repsdf2  14735  scshwfzeqfzo  14784  relexpindlem  15017  shftlem  15022  shftuz  15023  abslt  15268  absle  15269  rexico  15307  cau3lem  15308  reusq0  15416  rlim2lt  15448  rlim3  15449  o1lo1  15488  rlimdm  15502  climshft  15527  o1dif  15581  isercolllem2  15619  isercoll  15621  zsum  15671  fsum  15673  fsum00  15751  incexclem  15789  zprod  15888  fprod  15892  dvdsval2  16207  moddvds  16215  negdvdsb  16223  dvdsnegb  16224  dvdscmulr  16235  dvdsmulcr  16236  dvdssub2  16251  dvdsaddre2b  16257  fzo0dvdseq  16273  mod2eq1n2dvds  16297  ltoddhalfle  16311  sumodd  16338  bitsf1ocnv  16392  sadcaddlem  16405  bitsuz  16422  dvdsgcdb  16494  gcdzeq  16501  dvdssqlem  16510  lcmeq0  16544  lcmdvdsb  16557  lcmfeq0b  16574  lcmf  16577  lcmfdvdsb  16587  coprmgcdb  16593  cncongr  16613  isprm2lem  16625  dvdsprime  16631  dvdsprm  16647  isprm7  16652  coprm  16655  euclemma  16657  rpexp  16666  prmdvdsncoprmbd  16670  prmdiveq  16726  hashgcdlem  16728  odzdvds  16735  pythagtrip  16774  pc2dvds  16819  pcprmpw2  16822  pcprmpw  16823  vdwapun  16914  ramtcl2  16951  firest  17385  mrieqv2d  17590  isacs2  17604  isssc  17774  setciso  18051  posasymb  18282  pleval2  18300  pltval3  18302  lublecllem  18323  joinle  18349  meetle  18363  latdisd  18460  lubun  18478  clatleglb  18481  letsr  18556  intopsn  18585  gsumval2a  18616  frmdss2  18786  isgrpid2  18904  isgrpinv  18921  f1ghm0to0  19166  symg1bas  19306  oddvdsnn0  19460  oddvds  19463  odeq  19466  odeq1  19476  gexdvds  19500  pgpfi  19521  pgpssslw  19530  fislw  19541  sylow3lem2  19544  lsmelvalm  19567  lsmlub  19580  lsmss1b  19582  lsmss2b  19584  efgs1b  19652  cyggenod  19800  cyggexb  19815  dprdfeq0  19940  ablsimpgfind  20028  ringinvnz1ne0  20195  ringinvnzdiv  20196  unitmulclb  20279  dvreq1  20309  isnzr2  20416  0ringnnzr  20421  0ring01eqbi  20428  rngciso  20530  ringciso  20564  drngmul0or  20612  isabvd  20659  issrngd  20700  lssats2  20843  lspsneq0  20855  lsmelval2  20929  lvecvs0or  20955  lspsneq  20969  lspsneu  20970  lidl1el  21079  lidldvgen  21182  rrgeq0  21195  domneq0  21202  pzriprnglem10  21350  pzriprnglem11  21351  znunit  21429  psgndif  21465  ipeq0  21501  ocvsscon  21538  pjdm2  21576  obselocv  21593  islinds4  21700  ply1coe1eq  22142  cply1coe0bi  22144  mat1dimelbas  22293  cramer  22513  toponcomb  22751  tgss3  22809  clsval2  22874  isopn3  22890  elcls3  22907  opncldf1  22908  neiint  22928  neips  22937  opnneissb  22938  opnssneib  22939  opnnei  22944  tpnei  22945  opnneiid  22950  restcld  22996  restopnb  22999  tgcn  23076  tgcnp  23077  subbascn  23078  iscnp4  23087  cnpnei  23088  cncls2  23097  cncls  23098  cnntr  23099  lmss  23122  hausnei2  23177  lpcls  23188  ordtt1  23203  cmpsub  23224  tgcmp  23225  1stcelcls  23285  locfincmp  23350  kgencn2  23381  ptpjpre1  23395  upxp  23447  txcn  23450  txlm  23472  tgqtop  23536  kqfvima  23554  isr0  23561  regr1lem2  23564  hmeoopn  23590  hmeocld  23591  ptuncnv  23631  fbunfip  23693  fgss2  23698  ufilb  23730  ufprim  23733  trufil  23734  cfinufil  23752  ufildr  23755  elfm2  23772  elfm3  23774  rnelfm  23777  fmfnfmlem4  23781  fmco  23785  flimtopon  23794  flimopn  23799  fbflim2  23801  flimrest  23807  flffbas  23819  cnpflf  23825  fclstopon  23836  fclsnei  23843  fclsbas  23845  fclsfnflim  23851  fclscmp  23854  ufilcmp  23856  isfcf  23858  fcfnei  23859  cnpfcf  23865  alexsubb  23870  alexsubALT  23875  cldsubg  23935  tgphaus  23941  tgpt0  23943  tsmsgsum  23963  tsmsres  23968  xbln0  24240  blssexps  24252  blssex  24253  isxms2  24274  prdsbl  24320  neibl  24330  metss  24337  met2ndc  24352  metrest  24353  metcnp3  24369  tngngp3  24493  nmoeq0  24573  xrsxmet  24645  reconn  24664  iccpnfcnv  24789  fgcfil  25119  iscau4  25127  cfilres  25144  iunmbl2  25406  ismbf3d  25503  mbfaddlem  25509  i1faddlem  25542  i1fmullem  25543  ellimc3  25728  dvfsumlem2  25881  tdeglem4  25915  tdeglem4OLD  25916  deg1nn0clb  25946  deg1lt0  25947  dvdsq1p  26016  plypf1  26064  0dgrb  26098  plymul0or  26133  ulmshft  26241  ulmcaulem  26245  ulmcau  26246  cosord  26380  eff1olem  26397  lognegb  26438  eflogeq  26450  logdivlt  26469  efopn  26506  cxpeq0  26526  cxpeq  26606  angpieqvd  26677  dcubic  26692  asinsinb  26743  acoscosb  26744  atantanb  26770  rlimcnp  26811  isppw  26959  isppw2  26960  vmappw  26961  isnsqf  26980  ppieq0  27021  fsumdvdsdiag  27029  dvdsppwf1o  27031  fsumfldivdiag  27035  chpeq0  27054  chteq0  27055  dchrptlem1  27110  lgsdir2lem4  27174  lgsne0  27181  lgsqr  27197  lgsdchrval  27200  gausslemma2dlem1a  27211  lgsquadlem1  27226  m1lgs  27234  2sqreultblem  27294  2sqreunnltblem  27297  nodenselem8  27537  sltlend  27617  oldlim  27726  sltlpss  27746  sleadd1  27819  sltneg  27870  muls0ord  27998  absslt  28056  iscgrglt  28198  brbtwn  28590  brcgr  28591  brbtwn2  28596  axcontlem7  28661  uhgr0vb  28765  edglnl  28836  ausgrusgrb  28858  ushgredgedg  28919  ushgredgedgloop  28921  usgr0vb  28927  usgr1v  28946  nbupgr  29034  nbumgrvtx  29036  nbuhgr2vtx1edgb  29042  edgusgrnbfin  29063  nb3grprlem1  29070  uvtxnbvtxm1  29096  cusgrfilem2  29146  uhgr0edg0rgrb  29264  cusgrm1rusgr  29272  spthonepeq  29442  usgr2pth  29454  wlkiswwlks  29563  wlkiswwlkupgr  29565  wlklnwwlkn  29571  wlklnwwlknupgr  29573  wwlksnextbi  29581  wwlksnredwwlkn0  29583  wwlksnextwrd  29584  wwlksnextprop  29599  umgrwwlks2on  29644  elwspths2on  29647  usgr2wspthons3  29651  elwwlks2  29653  elwspths2spth  29654  clwlkclwwlklem3  29687  loopclwwlkn1b  29728  clwwlknon1sn  29786  clwwlknonwwlknonb  29792  umgr3v3e3cycl  29870  eupth2lem3lem4  29917  frgr0v  29948  frgr3vlem2  29960  2clwwlk2clwwlk  30036  wlkl0  30053  grpoinvf  30218  nvmul0or  30336  nvz  30355  diporthcom  30402  ubthlem3  30558  hvmul0or  30711  his6  30785  hial0  30788  hial02  30789  orthcom  30794  normgt0  30813  ocin  30982  occon3  30983  shsel3  31001  shlub  31100  chssoc  31182  h1de2bi  31240  spansncol  31254  elspansn4  31259  spansnss2  31261  sumspansn  31335  lnopcnbd  31722  lnfncnbd  31743  riesz1  31751  elpjrn  31876  cvcon3  31970  dmdmd  31986  dmdbr3  31991  dmdbr4  31992  dmdbr5  31994  mdslmd1i  32015  atcveq0  32034  chcv1  32041  atssma  32064  atcv0eq  32065  atcv1  32066  bian1d  32133  disjeq1f  32237  br8d  32272  fpwrelmap  32391  xaddeq0  32399  eliccelico  32421  elicoelioo  32422  isarchiofld  32871  unitdivcld  33345  xrge0iifcnv  33377  lmxrge0  33396  indf1ofs  33488  eulerpartlemgh  33841  dstfrvunirn  33937  fnrelpredd  34556  loop1cycl  34592  cusgracyclt3v  34611  cvmliftmolem2  34737  cvmlift2lem12  34769  satfvsucsuc  34820  satfdm  34824  fmlasuc  34841  satffunlem1lem2  34858  satffunlem2lem2  34861  mthmb  35036  climuzcnv  35120  br8  35196  br6  35197  br4  35198  funbreq  35211  axextbdist  35242  dfrdg4  35393  cgrcom  35432  cgrcoml  35438  cgrdegen  35446  btwncom  35456  brsegle  35550  brsegle2  35551  colinbtwnle  35560  btwnoutside  35567  broutsideof3  35568  outsidele  35574  lineunray  35589  lineelsb2  35590  elhf2  35617  elicc3  35666  nn0prpwlem  35671  opnbnd  35674  cldbnd  35675  opnregcld  35679  cldregopn  35680  fnessref  35706  refssfne  35707  neibastop2  35710  fnemeet2  35716  fnejoin2  35718  fgmin  35719  ontgval  35780  ordtop  35785  ordcmp  35796  nndivsub  35806  bj-19.21t  36111  bj-19.23t  36112  bj-19.42t  36115  bj-sbft  36117  bj-cbv2hv  36139  bj-equsal1t  36164  bj-19.21t0  36172  bj-ceqsalt0  36228  bj-ceqsalt1  36229  bj-xpnzexb  36306  bj-idreseq  36507  bj-imdiridlem  36530  bj-finsumval0  36630  bj-fvimacnv0  36631  bj-isrvec2  36645  bj-bary1  36657  dfgcd3  36669  isbasisrelowllem1  36700  isbasisrelowllem2  36701  finxpsuclem  36742  wl-lem-exsb  36895  wl-mo3t  36905  wl-ax11-lem1  36911  matunitlindf  36950  poimirlem6  36958  poimirlem7  36959  poimirlem16  36968  poimirlem19  36971  poimirlem22  36974  poimirlem23  36975  poimirlem24  36976  cnambfre  37000  itg2addnc  37006  brabg2  37049  istotbnd3  37103  sstotbnd2  37106  sstotbnd  37107  sstotbnd3  37108  ssbnd  37120  ismtybnd  37139  reheibor  37171  grpoeqdivid  37213  grpokerinj  37225  rngosn3  37256  rngoueqz  37272  1idl  37358  0rngo  37359  divrngidl  37360  igenval2  37398  ispridlc  37402  isdmn3  37406  relcnveq3  37654  iss2  37677  elrelscnveq3  37825  funALTVeq  38034  disjeq  38068  prtlem10  38199  prter2  38215  dral1-o  38238  lshpinN  38323  lsatcveq0  38366  lsatcv0eq  38381  lsatcv1  38382  islshpcv  38387  lkr0f  38428  lkrshp4  38442  lshpkrlem1  38444  lshpset2N  38453  lfl1dim  38455  lfl1dim2N  38456  lub0N  38523  glb0N  38527  oplecon3b  38534  cmtcomN  38583  cmtbr3N  38588  cmtbr4N  38589  cvrnbtwn2  38609  cvrnbtwn3  38610  cvrcon3b  38611  cvrnbtwn4  38613  cvrcmp  38617  atcvreq0  38648  atnle  38651  atlatle  38654  cvlexchb1  38664  cvlcvr1  38673  hlrelat2  38738  exatleN  38739  cvrval3  38748  cvrval4N  38749  cvrexch  38755  atcvr0eq  38761  lnnat  38762  atcvrj0  38763  atcvrj2b  38767  atltcvr  38770  atbtwn  38781  ps-1  38812  3at  38825  islln2a  38852  llncmp  38857  islpln2a  38883  lplncmp  38897  islvol2aN  38927  4at  38948  lvolcmp  38952  pmaple  39096  lncmp  39118  paddss  39180  llnexchb2lem  39203  2polcon4bN  39253  ispsubcl2N  39282  lhpat3  39381  lautcvr  39427  ltrnid  39470  trlval2  39498  trlatn0  39507  ltrnideq  39510  trlnidatb  39512  cdlemeg49lebilem  39874  trlord  39904  cdlemg1a  39905  cdlemg1cex  39923  tendoid0  40160  dva1dim  40320  cdlemm10N  40453  diarnN  40464  cdlemn  40547  dihlspsnssN  40667  dihatexv  40673  dochkrshp  40721  dochkrshp4  40724  djhlsmcl  40749  lcfl6  40835  lcfl8  40837  lcfrvalsnN  40876  lcfrlem9  40885  mapdval2N  40965  mapdordlem2  40972  mapd1o  40983  mapd0  41000  mapdheq2biN  41065  nnproddivdvdsd  41333  sticksstones11  41439  sticksstones22  41451  fnsnbt  41518  eqresfnbd  41521  frlmfzowrdb  41545  frlmsnic  41573  evlselvlem  41621  dvdsexpnn  41694  mulgt0b2d  41796  prjspreln0  41814  elrfi  41895  diophrw  41960  eldioph2b  41964  diophin  41973  rexrabdioph  41995  rmxycomplete  42119  coprmdvdsb  42187  jm2.19  42195  jm2.26  42204  jm2.27  42210  limsuc2  42246  dgraa0p  42354  rngunsnply  42378  fiuneneq  42402  unielss  42430  oaabsb  42507  nnoeomeqom  42525  cantnfresb  42537  tfsconcatrn  42555  tfsconcat0b  42559  tfsconcatrev  42561  oadif1lem  42592  oadif1  42593  fzunt  42669  fzuntd  42670  fzunt1d  42671  fzuntgd  42672  pwelg  42774  nzss  43539  dvconstbi  43556  expgrowth  43557  bcc0  43562  axc11next  43628  pm14.24  43654  sbiota1  43656  sbcim2g  43762  sineq0ALT  44161  pwssfi  44194  mapss2  44363  fsneq  44364  fsneqrn  44369  mapssbi  44371  ssmapsn  44374  rnmptbd2lem  44411  infnsuprnmpt  44413  rnmptbdlem  44418  xralrple2  44523  infxrunb2  44537  xralrple4  44542  xralrple3  44543  xrralrecnnle  44552  xrralrecnnge  44559  reclt0  44560  supxrunb3  44568  supxrleubrnmpt  44575  xrre4  44580  unb2ltle  44584  rexabslelem  44587  suprleubrnmpt  44591  infxrunb3rnmpt  44597  uzub  44600  supminfrnmpt  44614  iccintsng  44695  sqrlearg  44725  uzinico  44732  preimaiocmnf  44733  limcresiooub  44817  limclr  44830  climeldmeq  44840  limsuppnflem  44885  limsupmnflem  44895  limsupmnfuzlem  44901  limsupre3lem  44907  limsupre3uzlem  44910  liminfreuzlem  44977  dvnmul  45118  dvmptfprodlem  45119  ismbl3  45161  ismbl4  45168  fourierdlem50  45331  fourierdlem89  45370  fourierdlem91  45372  dfsalgen2  45516  sge0repnf  45561  sge0lefi  45573  sge0resplit  45581  sge0fodjrnlem  45591  voliunsge0lem  45647  hspdifhsp  45791  isvonmbl  45813  ovnovollem3  45833  vonvolmbl  45836  pimrecltpos  45883  preimaicomnf  45886  pimrecltneg  45899  issmflem  45902  issmfle  45920  issmfgt  45931  smfaddlem1  45938  issmfge  45945  smfresal  45963  smflimmpt  45985  smfinflem  45992  smflimsuplem7  46001  smflimsupmpt  46004  sigarcol  46039  confun  46108  or2expropbi  46203  fsetsniunop  46218  fcoresf1b  46239  f1cof1b  46244  funfocofob  46245  rexsb  46266  euoreqb  46276  ralbinrald  46289  rlimdmafv  46344  fafv2elrnb  46402  tz6.12c-afv2  46409  dfatbrafv2b  46412  fnbrafv2b  46415  rlimdmafv2  46425  f1oresf1o2  46458  el1fzopredsuc  46492  2ffzoeq  46495  imasetpreimafvbijlemfo  46532  iccpartiun  46561  ichnfb  46592  ich2exprop  46598  sprsymrelfolem2  46620  paireqne  46638  prprelprb  46644  reupr  46649  requad01  46748  requad1  46749  requad2  46750  dfodd6  46764  dfeven4  46765  evensumeven  46834  sbgoldbalt  46908  isomushgr  46953  isomuspgr  46961  isomgrsymb  46964  isassintop  47047  uzlidlring  47072  rngcisoALTV  47114  ringcisoALTV  47148  domnmsuppn0  47208  lindslininds  47307  snlindsntor  47314  isldepslvec2  47328  affinecomb1  47550  prelrrx2b  47562  rrx2plord2  47570  eenglngeehlnm  47587  rrx2vlinest  47589  line2xlem  47601  line2x  47602  line2y  47603  itsclc0xyqsolb  47618  itsclquadb  47624  mpbiran3d  47644  rspceb2dv  47650  opnneieqv  47705  iscnrm3lem2  47729  fullthinc2  47829  thincciso  47831