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  269  imbi1d  341  pm5.501  366  2falsedOLD  377  impbida  797  dedlem0b  1041  dedlema  1042  dedlemb  1043  albi  1824  alexbii  1838  equequ1  2031  equequ2  2032  spsbbi  2079  elequ1  2116  elequ2  2124  sbequ12  2247  sbft  2265  cbv2w  2337  exsb  2358  dral1v  2368  dral1vOLD  2369  cbv2  2404  cbv2h  2407  ax12b  2425  dral1  2440  dral1ALT  2441  eupickb  2638  eupickbi  2639  2eu2  2655  ralbi  3094  ralbida  3158  rexbi  3171  ceqsalt  3460  vtoclgft  3490  rspcebdv  3553  ceqex  3582  mob2  3653  reu6  3664  sbciegft  3757  sbcg  3799  2reu2  3835  csbiebt  3866  sseq1  3950  ss2abdv  4001  ssdifsym  4202  reupick  4257  reupick2  4259  ab0OLD  4314  uneqdifeq  4428  prnebg  4791  preqsnd  4794  prel12g  4799  iuneqconst  4940  disjeq2  5047  disjeq1  5050  disjss3  5077  reusv2lem2  5325  reusv2lem3  5326  alxfr  5333  ralxfrd  5334  ralxfrd2  5338  copsexgw  5406  copsexg  5407  snopeqop  5422  euotd  5429  poeq2  5506  sotric  5530  sotrieq  5531  freq2  5559  seeq1  5560  seeq2  5561  iss  5940  tz7.7  6289  ordtri1  6296  ordelinel  6361  iotaval  6404  funeq  6450  funssres  6474  f0dom0  6654  tz6.12c  6793  fnbrfvb  6816  ssimaex  6847  fvimacnv  6924  elpreima  6929  eldmrexrnb  6962  fsn  7001  fnsnb  7032  fmptsng  7034  fmptsnd  7035  fprb  7063  tpres  7070  fconst2g  7072  fconst5  7075  elunirn  7118  f1ocnvfvb  7145  f1prex  7149  foeqcnvco  7165  f1eqcocnv  7166  f1eqcocnvOLD  7167  fliftfun  7176  soisores  7191  isofr  7206  isose  7207  isopo  7210  isoso  7212  f1oiso2  7216  eusvobj2  7261  oprabidw  7299  oprabid  7300  f1opw2  7515  oneqmin  7640  ordsuc  7649  ordelsuc  7655  ordsucelsuc  7657  ordunisuc2  7679  limsuc  7684  fndmexb  7742  f1ovv  7787  op1steq  7861  opreuopreu  7862  funeldmdif  7875  fvn0elsuppb  7981  extmptsuppeq  7988  rntpos  8039  smoiso2  8184  seqomlem2  8266  oaord  8354  oawordex  8364  oaordex  8365  omord2  8374  om00  8382  oeord  8395  nnaord  8426  nnmord  8439  nnawordex  8444  nnaordex  8445  eldifsucnn  8468  erexb  8497  swoord1  8503  swoord2  8504  iiner  8552  eceqoveq  8585  mapsnd  8648  ralxpmap  8658  omxpenlem  8829  domtriord  8875  mapxpen  8895  mapunen  8898  ssenen  8903  enfi  8938  nneneq  8956  nndomog  8964  nneneqOLD  8969  nndomogOLD  8974  onomeneq  8975  en1eqsnbi  9010  fodomfib  9054  f1opwfi  9084  fsuppunbi  9110  elfiun  9150  suplub2  9181  ordiso2  9235  ordiso  9236  oieu  9259  brwdom2  9293  brwdom3  9302  cantnflem1  9408  ttrclselem2  9445  cardidm  9701  carddom2  9719  pm54.43  9743  pr2ne  9745  acnen  9793  acnen2  9795  alephord  9815  alephinit  9835  dfac5  9868  infdif2  9950  fictb  9985  coflim  10001  fincssdom  10063  fin23lem25  10064  isf32lem9  10101  isf34lem4  10117  fin1a2lem11  10150  axdc3lem2  10191  ficard  10305  fpwwe2lem11  10381  fpwwe2  10383  indpi  10647  nqereq  10675  1idpr  10769  ltapr  10785  leltne  11048  ltlen  11059  ltadd2  11062  addlsub  11374  addid0  11377  ltord1  11484  mul0or  11598  ldiv  11792  ltmul1  11808  mulge0b  11828  lt2msq  11843  negfi  11907  nnsub  12000  nn0sub  12266  zrevaddcl  12348  zltp1le  12353  zdiv  12373  nneo  12387  zeo2  12390  zmax  12667  zbtwnre  12668  qrevaddcl  12693  xrlttri  12855  xrleltne  12861  xralrple  12921  xltneg  12933  xleadd1  12971  xlemul1  13006  supxrunb1  13035  supxrunb2  13036  ioo0  13086  iccid  13106  ico0  13107  ioc0  13108  icc0  13109  difreicc  13198  iccsplit  13199  zltaddlt1le  13219  0fz1  13258  uzsplit  13310  fzm1  13318  fzrevral  13323  ssfzo12bi  13463  elfznelfzob  13474  flge  13506  modid2  13599  modmuladd  13614  ssnn0fi  13686  seqf1olem1  13743  hashen  14042  hashdom  14075  hash2exprb  14166  pr2pwpr  14174  hashtpg  14180  len0nnbi  14235  ccats1pfxeqbi  14436  reuccatpfxs1  14441  repsdf2  14472  scshwfzeqfzo  14520  relexpindlem  14755  shftlem  14760  shftuz  14761  abslt  15007  absle  15008  rexico  15046  cau3lem  15047  reusq0  15155  rlim2lt  15187  rlim3  15188  o1lo1  15227  rlimdm  15241  climshft  15266  o1dif  15320  isercolllem2  15358  isercoll  15360  zsum  15411  fsum  15413  fsum00  15491  incexclem  15529  zprod  15628  fprod  15632  dvdsval2  15947  moddvds  15955  negdvdsb  15963  dvdsnegb  15964  dvdscmulr  15975  dvdsmulcr  15976  dvdssub2  15991  dvdsaddre2b  15997  fzo0dvdseq  16013  mod2eq1n2dvds  16037  ltoddhalfle  16051  sumodd  16078  bitsf1ocnv  16132  sadcaddlem  16145  bitsuz  16162  dvdsgcdb  16234  gcdzeq  16243  dvdssqlem  16252  lcmeq0  16286  lcmdvdsb  16299  lcmfeq0b  16316  lcmf  16319  lcmfdvdsb  16329  coprmgcdb  16335  cncongr  16355  isprm2lem  16367  dvdsprime  16373  dvdsprm  16389  isprm7  16394  coprm  16397  euclemma  16399  rpexp  16408  prmdvdsncoprmbd  16412  prmdiveq  16468  hashgcdlem  16470  odzdvds  16477  pythagtrip  16516  pc2dvds  16561  pcprmpw2  16564  pcprmpw  16565  vdwapun  16656  ramtcl2  16693  firest  17124  mrieqv2d  17329  isacs2  17343  isssc  17513  setciso  17787  posasymb  18018  pleval2  18036  pltval3  18038  lublecllem  18059  joinle  18085  meetle  18099  latdisd  18196  lubun  18214  clatleglb  18217  letsr  18292  intopsn  18319  gsumval2a  18350  frmdss2  18483  isgrpid2  18597  isgrpinv  18613  symg1bas  18979  oddvdsnn0  19133  oddvds  19136  odeq  19139  odeq1  19148  gexdvds  19170  pgpfi  19191  pgpssslw  19200  fislw  19211  sylow3lem2  19214  lsmelvalm  19237  lsmlub  19251  lsmss1b  19253  lsmss2b  19255  efgs1b  19323  cyggenod  19465  cyggexb  19481  dprdfeq0  19606  ablsimpgfind  19694  ringinvnz1ne0  19812  ringinvnzdiv  19813  unitmulclb  19888  dvreq1  19916  f1ghm0to0  19965  f1rhm0to0ALT  19966  drngmul0or  19993  isabvd  20061  issrngd  20102  lssats2  20243  lspsneq0  20255  lsmelval2  20328  lvecvs0or  20351  lspsneq  20365  lspsneu  20366  lidl1el  20470  lidldvgen  20507  isnzr2  20515  0ringnnzr  20521  0ring01eqbi  20525  rrgeq0  20542  domneq0  20549  znunit  20752  psgndif  20788  ipeq0  20824  ocvsscon  20861  pjdm2  20899  obselocv  20916  islinds4  21023  ply1coe1eq  21450  cply1coe0bi  21452  mat1dimelbas  21601  cramer  21821  toponcomb  22059  tgss3  22117  clsval2  22182  isopn3  22198  elcls3  22215  opncldf1  22216  neiint  22236  neips  22245  opnneissb  22246  opnssneib  22247  opnnei  22252  tpnei  22253  opnneiid  22258  restcld  22304  restopnb  22307  tgcn  22384  tgcnp  22385  subbascn  22386  iscnp4  22395  cnpnei  22396  cncls2  22405  cncls  22406  cnntr  22407  lmss  22430  hausnei2  22485  lpcls  22496  ordtt1  22511  cmpsub  22532  tgcmp  22533  1stcelcls  22593  locfincmp  22658  kgencn2  22689  ptpjpre1  22703  upxp  22755  txcn  22758  txlm  22780  tgqtop  22844  kqfvima  22862  isr0  22869  regr1lem2  22872  hmeoopn  22898  hmeocld  22899  ptuncnv  22939  fbunfip  23001  fgss2  23006  ufilb  23038  ufprim  23041  trufil  23042  cfinufil  23060  ufildr  23063  elfm2  23080  elfm3  23082  rnelfm  23085  fmfnfmlem4  23089  fmco  23093  flimtopon  23102  flimopn  23107  fbflim2  23109  flimrest  23115  flffbas  23127  cnpflf  23133  fclstopon  23144  fclsnei  23151  fclsbas  23153  fclsfnflim  23159  fclscmp  23162  ufilcmp  23164  isfcf  23166  fcfnei  23167  cnpfcf  23173  alexsubb  23178  alexsubALT  23183  cldsubg  23243  tgphaus  23249  tgpt0  23251  tsmsgsum  23271  tsmsres  23276  xbln0  23548  blssexps  23560  blssex  23561  isxms2  23582  prdsbl  23628  neibl  23638  metss  23645  met2ndc  23660  metrest  23661  metcnp3  23677  tngngp3  23801  nmoeq0  23881  xrsxmet  23953  reconn  23972  iccpnfcnv  24088  fgcfil  24416  iscau4  24424  cfilres  24441  iunmbl2  24702  ismbf3d  24799  mbfaddlem  24805  i1faddlem  24838  i1fmullem  24839  ellimc3  25024  tdeglem4  25205  tdeglem4OLD  25206  deg1nn0clb  25236  deg1lt0  25237  dvdsq1p  25306  plypf1  25354  0dgrb  25388  plymul0or  25422  ulmshft  25530  ulmcaulem  25534  ulmcau  25535  cosord  25668  eff1olem  25685  lognegb  25726  eflogeq  25738  logdivlt  25757  efopn  25794  cxpeq0  25814  cxpeq  25891  angpieqvd  25962  dcubic  25977  asinsinb  26028  acoscosb  26029  atantanb  26055  rlimcnp  26096  isppw  26244  isppw2  26245  vmappw  26246  isnsqf  26265  ppieq0  26306  fsumdvdsdiag  26314  dvdsppwf1o  26316  fsumfldivdiag  26320  chpeq0  26337  chteq0  26338  dchrptlem1  26393  lgsdir2lem4  26457  lgsne0  26464  lgsqr  26480  lgsdchrval  26483  gausslemma2dlem1a  26494  lgsquadlem1  26509  m1lgs  26517  2sqreultblem  26577  2sqreunnltblem  26580  iscgrglt  26856  brbtwn  27248  brcgr  27249  brbtwn2  27254  axcontlem7  27319  uhgr0vb  27423  edglnl  27494  ausgrusgrb  27516  ushgredgedg  27577  ushgredgedgloop  27579  usgr0vb  27585  usgr1v  27604  nbupgr  27692  nbumgrvtx  27694  nbuhgr2vtx1edgb  27700  edgusgrnbfin  27721  nb3grprlem1  27728  uvtxnbvtxm1  27754  cusgrfilem2  27804  uhgr0edg0rgrb  27922  cusgrm1rusgr  27930  spthonepeq  28099  usgr2pth  28111  wlkiswwlks  28220  wlkiswwlkupgr  28222  wlklnwwlkn  28228  wlklnwwlknupgr  28230  wwlksnextbi  28238  wwlksnredwwlkn0  28240  wwlksnextwrd  28241  wwlksnextprop  28256  umgrwwlks2on  28301  elwspths2on  28304  usgr2wspthons3  28308  elwwlks2  28310  elwspths2spth  28311  clwlkclwwlklem3  28344  loopclwwlkn1b  28385  clwwlknon1sn  28443  clwwlknonwwlknonb  28449  umgr3v3e3cycl  28527  eupth2lem3lem4  28574  frgr0v  28605  frgr3vlem2  28617  2clwwlk2clwwlk  28693  wlkl0  28710  grpoinvf  28873  nvmul0or  28991  nvz  29010  diporthcom  29057  ubthlem3  29213  hvmul0or  29366  his6  29440  hial0  29443  hial02  29444  orthcom  29449  normgt0  29468  ocin  29637  occon3  29638  shsel3  29656  shlub  29755  chssoc  29837  h1de2bi  29895  spansncol  29909  elspansn4  29914  spansnss2  29916  sumspansn  29990  lnopcnbd  30377  lnfncnbd  30398  riesz1  30406  elpjrn  30531  cvcon3  30625  dmdmd  30641  dmdbr3  30646  dmdbr4  30647  dmdbr5  30649  mdslmd1i  30670  atcveq0  30689  chcv1  30696  atssma  30719  atcv0eq  30720  atcv1  30721  bian1d  30788  disjeq1f  30891  br8d  30929  fpwrelmap  31047  xaddeq0  31055  eliccelico  31077  elicoelioo  31078  isarchiofld  31495  unitdivcld  31830  xrge0iifcnv  31862  lmxrge0  31881  indf1ofs  31973  eulerpartlemgh  32324  dstfrvunirn  32420  fnrelpredd  33040  loop1cycl  33078  cusgracyclt3v  33097  cvmliftmolem2  33223  cvmlift2lem12  33255  satfvsucsuc  33306  satfdm  33310  fmlasuc  33327  satffunlem1lem2  33344  satffunlem2lem2  33347  mthmb  33522  climuzcnv  33608  br8  33702  br6  33703  br4  33704  funbreq  33723  axextbdist  33755  nodenselem8  33873  oldlim  34048  sltlpss  34066  dfrdg4  34232  cgrcom  34271  cgrcoml  34277  cgrdegen  34285  btwncom  34295  brsegle  34389  brsegle2  34390  colinbtwnle  34399  btwnoutside  34406  broutsideof3  34407  outsidele  34413  lineunray  34428  lineelsb2  34429  elhf2  34456  elicc3  34485  nn0prpwlem  34490  opnbnd  34493  cldbnd  34494  opnregcld  34498  cldregopn  34499  fnessref  34525  refssfne  34526  neibastop2  34529  fnemeet2  34535  fnejoin2  34537  fgmin  34538  ontgval  34599  ordtop  34604  ordcmp  34615  nndivsub  34625  bj-19.21t  34930  bj-19.23t  34931  bj-19.42t  34934  bj-sbft  34936  bj-cbv2hv  34958  bj-equsal1t  34984  bj-19.21t0  34992  bj-ceqsalt0  35048  bj-ceqsalt1  35049  bj-xpnzexb  35130  bj-idreseq  35312  bj-imdiridlem  35335  bj-finsumval0  35435  bj-fvimacnv0  35436  bj-isrvec2  35450  bj-bary1  35462  dfgcd3  35474  isbasisrelowllem1  35505  isbasisrelowllem2  35506  finxpsuclem  35547  wl-lem-exsb  35700  wl-mo3t  35710  wl-ax11-lem1  35715  matunitlindf  35754  poimirlem6  35762  poimirlem7  35763  poimirlem16  35772  poimirlem19  35775  poimirlem22  35778  poimirlem23  35779  poimirlem24  35780  cnambfre  35804  itg2addnc  35810  brabg2  35853  istotbnd3  35908  sstotbnd2  35911  sstotbnd  35912  sstotbnd3  35913  ssbnd  35925  ismtybnd  35944  reheibor  35976  grpoeqdivid  36018  grpokerinj  36030  rngosn3  36061  rngoueqz  36077  1idl  36163  0rngo  36164  divrngidl  36165  igenval2  36203  ispridlc  36207  isdmn3  36211  relcnveq3  36435  iss2  36458  elrelscnveq3  36588  funALTVeq  36790  disjeq  36824  prtlem10  36858  prter2  36874  dral1-o  36897  lshpinN  36982  lsatcveq0  37025  lsatcv0eq  37040  lsatcv1  37041  islshpcv  37046  lkr0f  37087  lkrshp4  37101  lshpkrlem1  37103  lshpset2N  37112  lfl1dim  37114  lfl1dim2N  37115  lub0N  37182  glb0N  37186  oplecon3b  37193  cmtcomN  37242  cmtbr3N  37247  cmtbr4N  37248  cvrnbtwn2  37268  cvrnbtwn3  37269  cvrcon3b  37270  cvrnbtwn4  37272  cvrcmp  37276  atcvreq0  37307  atnle  37310  atlatle  37313  cvlexchb1  37323  cvlcvr1  37332  hlrelat2  37396  exatleN  37397  cvrval3  37406  cvrval4N  37407  cvrexch  37413  atcvr0eq  37419  lnnat  37420  atcvrj0  37421  atcvrj2b  37425  atltcvr  37428  atbtwn  37439  ps-1  37470  3at  37483  islln2a  37510  llncmp  37515  islpln2a  37541  lplncmp  37555  islvol2aN  37585  4at  37606  lvolcmp  37610  pmaple  37754  lncmp  37776  paddss  37838  llnexchb2lem  37861  2polcon4bN  37911  ispsubcl2N  37940  lhpat3  38039  lautcvr  38085  ltrnid  38128  trlval2  38156  trlatn0  38165  ltrnideq  38168  trlnidatb  38170  cdlemeg49lebilem  38532  trlord  38562  cdlemg1a  38563  cdlemg1cex  38581  tendoid0  38818  dva1dim  38978  cdlemm10N  39111  diarnN  39122  cdlemn  39205  dihlspsnssN  39325  dihatexv  39331  dochkrshp  39379  dochkrshp4  39382  djhlsmcl  39407  lcfl6  39493  lcfl8  39495  lcfrvalsnN  39534  lcfrlem9  39543  mapdval2N  39623  mapdordlem2  39630  mapd1o  39641  mapd0  39658  mapdheq2biN  39723  nnproddivdvdsd  39989  sticksstones11  40092  sticksstones22  40104  fnsnbt  40188  frlmfzowrdb  40215  frlmsnic  40243  dvdsexpnn  40320  mulgt0b2d  40410  prjspreln0  40428  elrfi  40496  diophrw  40561  eldioph2b  40565  diophin  40574  rexrabdioph  40596  rmxycomplete  40719  coprmdvdsb  40787  jm2.19  40795  jm2.26  40804  jm2.27  40810  limsuc2  40846  dgraa0p  40954  rngunsnply  40978  fiuneneq  41002  pwelg  41120  nzss  41888  dvconstbi  41905  expgrowth  41906  bcc0  41911  axc11next  41977  pm14.24  42003  sbiota1  42005  sbcim2g  42111  sineq0ALT  42510  pwssfi  42546  mapss2  42698  fsneq  42699  fsneqrn  42704  mapssbi  42706  ssmapsn  42709  rnmptbd2lem  42747  infnsuprnmpt  42749  rnmptbdlem  42754  xralrple2  42847  infxrunb2  42861  xralrple4  42866  xralrple3  42867  xrralrecnnle  42876  xrralrecnnge  42884  reclt0  42885  supxrunb3  42893  supxrleubrnmpt  42900  xrre4  42905  unb2ltle  42909  rexabslelem  42912  suprleubrnmpt  42916  infxrunb3rnmpt  42922  uzub  42925  supminfrnmpt  42939  iccintsng  43015  sqrlearg  43045  uzinico  43052  preimaiocmnf  43053  limcresiooub  43137  limclr  43150  climeldmeq  43160  limsuppnflem  43205  limsupmnflem  43215  limsupmnfuzlem  43221  limsupre3lem  43227  limsupre3uzlem  43230  liminfreuzlem  43297  dvnmul  43438  dvmptfprodlem  43439  ismbl3  43481  ismbl4  43488  fourierdlem50  43651  fourierdlem89  43690  fourierdlem91  43692  dfsalgen2  43834  sge0repnf  43878  sge0lefi  43890  sge0resplit  43898  sge0fodjrnlem  43908  voliunsge0lem  43964  hspdifhsp  44108  isvonmbl  44130  ovnovollem3  44150  vonvolmbl  44153  pimrecltpos  44197  preimaicomnf  44200  pimrecltneg  44211  issmflem  44214  issmfle  44232  issmfgt  44243  smfaddlem1  44249  issmfge  44256  smfresal  44273  smflimmpt  44294  smfinflem  44301  smflimsuplem7  44310  smflimsupmpt  44313  sigarcol  44331  confun  44385  or2expropbi  44479  fsetsniunop  44494  fcoresf1b  44515  f1cof1b  44520  funfocofob  44521  rexsb  44542  euoreqb  44552  ralbinrald  44565  rlimdmafv  44620  fafv2elrnb  44678  tz6.12c-afv2  44685  dfatbrafv2b  44688  fnbrafv2b  44691  rlimdmafv2  44701  f1oresf1o2  44734  el1fzopredsuc  44769  2ffzoeq  44772  imasetpreimafvbijlemfo  44809  iccpartiun  44838  ichnfb  44869  ich2exprop  44875  sprsymrelfolem2  44897  paireqne  44915  prprelprb  44921  reupr  44926  requad01  45025  requad1  45026  requad2  45027  dfodd6  45041  dfeven4  45042  evensumeven  45111  sbgoldbalt  45185  isomushgr  45230  isomuspgr  45238  isomgrsymb  45241  isassintop  45356  uzlidlring  45439  rngciso  45492  rngcisoALTV  45504  ringciso  45543  ringcisoALTV  45567  domnmsuppn0  45657  lindslininds  45757  snlindsntor  45764  isldepslvec2  45778  affinecomb1  46000  prelrrx2b  46012  rrx2plord2  46020  eenglngeehlnm  46037  rrx2vlinest  46039  line2xlem  46051  line2x  46052  line2y  46053  itsclc0xyqsolb  46068  itsclquadb  46074  mpbiran3d  46094  rspceb2dv  46100  opnneieqv  46156  iscnrm3lem2  46180  fullthinc2  46280  thincciso  46282