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  342  pm5.501  367  2falsedOLD  378  impbida  800  dedlem0b  1044  dedlema  1045  dedlemb  1046  albi  1821  alexbii  1836  equequ1  2029  equequ2  2030  spsbbi  2077  elequ1  2114  elequ2  2122  sbequ12  2244  sbft  2262  cbv2w  2334  exsb  2356  dral1v  2367  dral1vOLD  2368  cbv2  2403  cbv2h  2406  ax12b  2424  dral1  2439  dral1ALT  2440  eupickb  2632  eupickbi  2633  2eu2  2649  ralbi  3104  rexbi  3105  ralbida  3268  ceqsalt  3506  rspcebdv  3607  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  6034  tz7.7  6388  ordtri1  6395  ordelinel  6463  iotavalOLD  6515  funeq  6566  funssres  6590  f0dom0  6773  tz6.12cOLD  6916  fnbrfvb  6942  ssimaex  6974  fvimacnv  7052  elpreima  7057  eldmrexrnb  7091  fsn  7130  fnsnb  7161  fmptsng  7163  fmptsnd  7164  fprb  7192  tpres  7199  fconst2g  7201  fconst5  7204  elunirn  7247  f1ocnvfvb  7274  f1prex  7279  foeqcnvco  7295  f1eqcocnv  7296  f1eqcocnvOLD  7297  fliftfun  7306  soisores  7321  isofr  7336  isose  7337  isopo  7340  isoso  7342  f1oiso2  7346  eusvobj2  7398  oprabidw  7437  oprabid  7438  f1opw2  7658  oneqmin  7785  ordsucOLD  7799  ordelsuc  7805  ordsucelsuc  7807  ordunisuc2  7830  limsuc  7835  fndmexb  7896  f1ovv  7941  op1steq  8016  opreuopreu  8017  funeldmdif  8031  fvn0elsuppb  8163  extmptsuppeq  8170  rntpos  8221  smoiso2  8366  seqomlem2  8448  oaord  8544  oawordex  8554  oaordex  8555  omord2  8564  om00  8572  oeord  8585  nnaord  8616  nnmord  8629  nnawordex  8634  nnaordex  8635  eldifsucnn  8660  erexb  8725  swoord1  8731  swoord2  8732  iiner  8780  eceqoveq  8813  mapsnd  8877  ralxpmap  8887  omxpenlem  9070  domtriord  9120  mapxpen  9140  mapunen  9143  ssenen  9148  enfi  9187  nneneq  9206  nndomog  9213  nneneqOLD  9218  nndomogOLD  9223  onomeneq  9225  onomeneqOLD  9226  en1eqsnbi  9273  fodomfib  9323  f1opwfi  9353  fsuppunbi  9381  elfiun  9422  suplub2  9453  ordiso2  9507  ordiso  9508  oieu  9531  brwdom2  9565  brwdom3  9574  cantnflem1  9681  ttrclselem2  9718  cardidm  9951  carddom2  9969  pm54.43  9993  pr2neOLD  9997  acnen  10045  acnen2  10047  alephord  10067  alephinit  10087  dfac5  10120  infdif2  10202  fictb  10237  coflim  10253  fincssdom  10315  fin23lem25  10316  isf32lem9  10353  isf34lem4  10369  fin1a2lem11  10402  axdc3lem2  10443  ficard  10557  fpwwe2lem11  10633  fpwwe2  10635  indpi  10899  nqereq  10927  1idpr  11021  ltapr  11037  leltne  11300  ltlen  11312  ltadd2  11315  addlsub  11627  addid0  11630  ltord1  11737  mul0or  11851  ldiv  12045  ltmul1  12061  mulge0b  12081  lt2msq  12096  negfi  12160  nnsub  12253  nn0sub  12519  zrevaddcl  12604  zltp1le  12609  zdiv  12629  nneo  12643  zeo2  12646  zmax  12926  zbtwnre  12927  qrevaddcl  12952  xrlttri  13115  xrleltne  13121  xralrple  13181  xltneg  13193  xleadd1  13231  xlemul1  13266  supxrunb1  13295  supxrunb2  13296  ioo0  13346  iccid  13366  ico0  13367  ioc0  13368  icc0  13369  difreicc  13458  iccsplit  13459  zltaddlt1le  13479  0fz1  13518  uzsplit  13570  fzm1  13578  fzrevral  13583  ssfzo12bi  13724  elfznelfzob  13735  flge  13767  modid2  13860  modmuladd  13875  ssnn0fi  13947  seqf1olem1  14004  hashen  14304  hashdom  14336  hash2exprb  14429  pr2pwpr  14437  hashtpg  14443  len0nnbi  14498  ccats1pfxeqbi  14689  reuccatpfxs1  14694  repsdf2  14725  scshwfzeqfzo  14774  relexpindlem  15007  shftlem  15012  shftuz  15013  abslt  15258  absle  15259  rexico  15297  cau3lem  15298  reusq0  15406  rlim2lt  15438  rlim3  15439  o1lo1  15478  rlimdm  15492  climshft  15517  o1dif  15571  isercolllem2  15609  isercoll  15611  zsum  15661  fsum  15663  fsum00  15741  incexclem  15779  zprod  15878  fprod  15882  dvdsval2  16197  moddvds  16205  negdvdsb  16213  dvdsnegb  16214  dvdscmulr  16225  dvdsmulcr  16226  dvdssub2  16241  dvdsaddre2b  16247  fzo0dvdseq  16263  mod2eq1n2dvds  16287  ltoddhalfle  16301  sumodd  16328  bitsf1ocnv  16382  sadcaddlem  16395  bitsuz  16412  dvdsgcdb  16484  gcdzeq  16491  dvdssqlem  16500  lcmeq0  16534  lcmdvdsb  16547  lcmfeq0b  16564  lcmf  16567  lcmfdvdsb  16577  coprmgcdb  16583  cncongr  16603  isprm2lem  16615  dvdsprime  16621  dvdsprm  16637  isprm7  16642  coprm  16645  euclemma  16647  rpexp  16656  prmdvdsncoprmbd  16660  prmdiveq  16716  hashgcdlem  16718  odzdvds  16725  pythagtrip  16764  pc2dvds  16809  pcprmpw2  16812  pcprmpw  16813  vdwapun  16904  ramtcl2  16941  firest  17375  mrieqv2d  17580  isacs2  17594  isssc  17764  setciso  18038  posasymb  18269  pleval2  18287  pltval3  18289  lublecllem  18310  joinle  18336  meetle  18350  latdisd  18447  lubun  18465  clatleglb  18468  letsr  18543  intopsn  18570  gsumval2a  18601  frmdss2  18741  isgrpid2  18858  isgrpinv  18875  symg1bas  19253  oddvdsnn0  19407  oddvds  19410  odeq  19413  odeq1  19423  gexdvds  19447  pgpfi  19468  pgpssslw  19477  fislw  19488  sylow3lem2  19491  lsmelvalm  19514  lsmlub  19527  lsmss1b  19529  lsmss2b  19531  efgs1b  19599  cyggenod  19747  cyggexb  19762  dprdfeq0  19887  ablsimpgfind  19975  ringinvnz1ne0  20106  ringinvnzdiv  20107  unitmulclb  20188  dvreq1  20218  f1ghm0to0  20272  f1rhm0to0ALT  20273  isnzr2  20290  0ringnnzr  20295  0ring01eqbi  20300  drngmul0or  20337  isabvd  20421  issrngd  20462  lssats2  20604  lspsneq0  20616  lsmelval2  20689  lvecvs0or  20714  lspsneq  20728  lspsneu  20729  lidl1el  20834  lidldvgen  20886  rrgeq0  20899  domneq0  20906  znunit  21111  psgndif  21147  ipeq0  21183  ocvsscon  21220  pjdm2  21258  obselocv  21275  islinds4  21382  ply1coe1eq  21814  cply1coe0bi  21816  mat1dimelbas  21965  cramer  22185  toponcomb  22423  tgss3  22481  clsval2  22546  isopn3  22562  elcls3  22579  opncldf1  22580  neiint  22600  neips  22609  opnneissb  22610  opnssneib  22611  opnnei  22616  tpnei  22617  opnneiid  22622  restcld  22668  restopnb  22671  tgcn  22748  tgcnp  22749  subbascn  22750  iscnp4  22759  cnpnei  22760  cncls2  22769  cncls  22770  cnntr  22771  lmss  22794  hausnei2  22849  lpcls  22860  ordtt1  22875  cmpsub  22896  tgcmp  22897  1stcelcls  22957  locfincmp  23022  kgencn2  23053  ptpjpre1  23067  upxp  23119  txcn  23122  txlm  23144  tgqtop  23208  kqfvima  23226  isr0  23233  regr1lem2  23236  hmeoopn  23262  hmeocld  23263  ptuncnv  23303  fbunfip  23365  fgss2  23370  ufilb  23402  ufprim  23405  trufil  23406  cfinufil  23424  ufildr  23427  elfm2  23444  elfm3  23446  rnelfm  23449  fmfnfmlem4  23453  fmco  23457  flimtopon  23466  flimopn  23471  fbflim2  23473  flimrest  23479  flffbas  23491  cnpflf  23497  fclstopon  23508  fclsnei  23515  fclsbas  23517  fclsfnflim  23523  fclscmp  23526  ufilcmp  23528  isfcf  23530  fcfnei  23531  cnpfcf  23537  alexsubb  23542  alexsubALT  23547  cldsubg  23607  tgphaus  23613  tgpt0  23615  tsmsgsum  23635  tsmsres  23640  xbln0  23912  blssexps  23924  blssex  23925  isxms2  23946  prdsbl  23992  neibl  24002  metss  24009  met2ndc  24024  metrest  24025  metcnp3  24041  tngngp3  24165  nmoeq0  24245  xrsxmet  24317  reconn  24336  iccpnfcnv  24452  fgcfil  24780  iscau4  24788  cfilres  24805  iunmbl2  25066  ismbf3d  25163  mbfaddlem  25169  i1faddlem  25202  i1fmullem  25203  ellimc3  25388  tdeglem4  25569  tdeglem4OLD  25570  deg1nn0clb  25600  deg1lt0  25601  dvdsq1p  25670  plypf1  25718  0dgrb  25752  plymul0or  25786  ulmshft  25894  ulmcaulem  25898  ulmcau  25899  cosord  26032  eff1olem  26049  lognegb  26090  eflogeq  26102  logdivlt  26121  efopn  26158  cxpeq0  26178  cxpeq  26255  angpieqvd  26326  dcubic  26341  asinsinb  26392  acoscosb  26393  atantanb  26419  rlimcnp  26460  isppw  26608  isppw2  26609  vmappw  26610  isnsqf  26629  ppieq0  26670  fsumdvdsdiag  26678  dvdsppwf1o  26680  fsumfldivdiag  26684  chpeq0  26701  chteq0  26702  dchrptlem1  26757  lgsdir2lem4  26821  lgsne0  26828  lgsqr  26844  lgsdchrval  26847  gausslemma2dlem1a  26858  lgsquadlem1  26873  m1lgs  26881  2sqreultblem  26941  2sqreunnltblem  26944  nodenselem8  27184  oldlim  27371  sltlpss  27391  sleadd1  27462  sltneg  27509  iscgrglt  27755  brbtwn  28147  brcgr  28148  brbtwn2  28153  axcontlem7  28218  uhgr0vb  28322  edglnl  28393  ausgrusgrb  28415  ushgredgedg  28476  ushgredgedgloop  28478  usgr0vb  28484  usgr1v  28503  nbupgr  28591  nbumgrvtx  28593  nbuhgr2vtx1edgb  28599  edgusgrnbfin  28620  nb3grprlem1  28627  uvtxnbvtxm1  28653  cusgrfilem2  28703  uhgr0edg0rgrb  28821  cusgrm1rusgr  28829  spthonepeq  28999  usgr2pth  29011  wlkiswwlks  29120  wlkiswwlkupgr  29122  wlklnwwlkn  29128  wlklnwwlknupgr  29130  wwlksnextbi  29138  wwlksnredwwlkn0  29140  wwlksnextwrd  29141  wwlksnextprop  29156  umgrwwlks2on  29201  elwspths2on  29204  usgr2wspthons3  29208  elwwlks2  29210  elwspths2spth  29211  clwlkclwwlklem3  29244  loopclwwlkn1b  29285  clwwlknon1sn  29343  clwwlknonwwlknonb  29349  umgr3v3e3cycl  29427  eupth2lem3lem4  29474  frgr0v  29505  frgr3vlem2  29517  2clwwlk2clwwlk  29593  wlkl0  29610  grpoinvf  29773  nvmul0or  29891  nvz  29910  diporthcom  29957  ubthlem3  30113  hvmul0or  30266  his6  30340  hial0  30343  hial02  30344  orthcom  30349  normgt0  30368  ocin  30537  occon3  30538  shsel3  30556  shlub  30655  chssoc  30737  h1de2bi  30795  spansncol  30809  elspansn4  30814  spansnss2  30816  sumspansn  30890  lnopcnbd  31277  lnfncnbd  31298  riesz1  31306  elpjrn  31431  cvcon3  31525  dmdmd  31541  dmdbr3  31546  dmdbr4  31547  dmdbr5  31549  mdslmd1i  31570  atcveq0  31589  chcv1  31596  atssma  31619  atcv0eq  31620  atcv1  31621  bian1d  31688  disjeq1f  31792  br8d  31827  fpwrelmap  31946  xaddeq0  31954  eliccelico  31976  elicoelioo  31977  isarchiofld  32424  unitdivcld  32870  xrge0iifcnv  32902  lmxrge0  32921  indf1ofs  33013  eulerpartlemgh  33366  dstfrvunirn  33462  fnrelpredd  34081  loop1cycl  34117  cusgracyclt3v  34136  cvmliftmolem2  34262  cvmlift2lem12  34294  satfvsucsuc  34345  satfdm  34349  fmlasuc  34366  satffunlem1lem2  34383  satffunlem2lem2  34386  mthmb  34561  climuzcnv  34645  br8  34715  br6  34716  br4  34717  funbreq  34730  axextbdist  34761  dfrdg4  34912  cgrcom  34951  cgrcoml  34957  cgrdegen  34965  btwncom  34975  brsegle  35069  brsegle2  35070  colinbtwnle  35079  btwnoutside  35086  broutsideof3  35087  outsidele  35093  lineunray  35108  lineelsb2  35109  elhf2  35136  gg-dvfsumlem2  35172  elicc3  35191  nn0prpwlem  35196  opnbnd  35199  cldbnd  35200  opnregcld  35204  cldregopn  35205  fnessref  35231  refssfne  35232  neibastop2  35235  fnemeet2  35241  fnejoin2  35243  fgmin  35244  ontgval  35305  ordtop  35310  ordcmp  35321  nndivsub  35331  bj-19.21t  35636  bj-19.23t  35637  bj-19.42t  35640  bj-sbft  35642  bj-cbv2hv  35664  bj-equsal1t  35689  bj-19.21t0  35697  bj-ceqsalt0  35753  bj-ceqsalt1  35754  bj-xpnzexb  35831  bj-idreseq  36032  bj-imdiridlem  36055  bj-finsumval0  36155  bj-fvimacnv0  36156  bj-isrvec2  36170  bj-bary1  36182  dfgcd3  36194  isbasisrelowllem1  36225  isbasisrelowllem2  36226  finxpsuclem  36267  wl-lem-exsb  36420  wl-mo3t  36430  wl-ax11-lem1  36436  matunitlindf  36475  poimirlem6  36483  poimirlem7  36484  poimirlem16  36493  poimirlem19  36496  poimirlem22  36499  poimirlem23  36500  poimirlem24  36501  cnambfre  36525  itg2addnc  36531  brabg2  36574  istotbnd3  36628  sstotbnd2  36631  sstotbnd  36632  sstotbnd3  36633  ssbnd  36645  ismtybnd  36664  reheibor  36696  grpoeqdivid  36738  grpokerinj  36750  rngosn3  36781  rngoueqz  36797  1idl  36883  0rngo  36884  divrngidl  36885  igenval2  36923  ispridlc  36927  isdmn3  36931  relcnveq3  37179  iss2  37202  elrelscnveq3  37350  funALTVeq  37559  disjeq  37593  prtlem10  37724  prter2  37740  dral1-o  37763  lshpinN  37848  lsatcveq0  37891  lsatcv0eq  37906  lsatcv1  37907  islshpcv  37912  lkr0f  37953  lkrshp4  37967  lshpkrlem1  37969  lshpset2N  37978  lfl1dim  37980  lfl1dim2N  37981  lub0N  38048  glb0N  38052  oplecon3b  38059  cmtcomN  38108  cmtbr3N  38113  cmtbr4N  38114  cvrnbtwn2  38134  cvrnbtwn3  38135  cvrcon3b  38136  cvrnbtwn4  38138  cvrcmp  38142  atcvreq0  38173  atnle  38176  atlatle  38179  cvlexchb1  38189  cvlcvr1  38198  hlrelat2  38263  exatleN  38264  cvrval3  38273  cvrval4N  38274  cvrexch  38280  atcvr0eq  38286  lnnat  38287  atcvrj0  38288  atcvrj2b  38292  atltcvr  38295  atbtwn  38306  ps-1  38337  3at  38350  islln2a  38377  llncmp  38382  islpln2a  38408  lplncmp  38422  islvol2aN  38452  4at  38473  lvolcmp  38477  pmaple  38621  lncmp  38643  paddss  38705  llnexchb2lem  38728  2polcon4bN  38778  ispsubcl2N  38807  lhpat3  38906  lautcvr  38952  ltrnid  38995  trlval2  39023  trlatn0  39032  ltrnideq  39035  trlnidatb  39037  cdlemeg49lebilem  39399  trlord  39429  cdlemg1a  39430  cdlemg1cex  39448  tendoid0  39685  dva1dim  39845  cdlemm10N  39978  diarnN  39989  cdlemn  40072  dihlspsnssN  40192  dihatexv  40198  dochkrshp  40246  dochkrshp4  40249  djhlsmcl  40274  lcfl6  40360  lcfl8  40362  lcfrvalsnN  40401  lcfrlem9  40410  mapdval2N  40490  mapdordlem2  40497  mapd1o  40508  mapd0  40525  mapdheq2biN  40590  nnproddivdvdsd  40855  sticksstones11  40961  sticksstones22  40973  fnsnbt  41049  eqresfnbd  41052  frlmfzowrdb  41076  frlmsnic  41108  evlselvlem  41156  dvdsexpnn  41227  mulgt0b2d  41330  prjspreln0  41348  elrfi  41418  diophrw  41483  eldioph2b  41487  diophin  41496  rexrabdioph  41518  rmxycomplete  41642  coprmdvdsb  41710  jm2.19  41718  jm2.26  41727  jm2.27  41733  limsuc2  41769  dgraa0p  41877  rngunsnply  41901  fiuneneq  41925  unielss  41953  oaabsb  42030  nnoeomeqom  42048  cantnfresb  42060  tfsconcatrn  42078  tfsconcat0b  42082  tfsconcatrev  42084  oadif1lem  42115  oadif1  42116  fzunt  42192  fzuntd  42193  fzunt1d  42194  fzuntgd  42195  pwelg  42297  nzss  43062  dvconstbi  43079  expgrowth  43080  bcc0  43085  axc11next  43151  pm14.24  43177  sbiota1  43179  sbcim2g  43285  sineq0ALT  43684  pwssfi  43718  mapss2  43890  fsneq  43891  fsneqrn  43896  mapssbi  43898  ssmapsn  43901  rnmptbd2lem  43939  infnsuprnmpt  43941  rnmptbdlem  43946  xralrple2  44051  infxrunb2  44065  xralrple4  44070  xralrple3  44071  xrralrecnnle  44080  xrralrecnnge  44087  reclt0  44088  supxrunb3  44096  supxrleubrnmpt  44103  xrre4  44108  unb2ltle  44112  rexabslelem  44115  suprleubrnmpt  44119  infxrunb3rnmpt  44125  uzub  44128  supminfrnmpt  44142  iccintsng  44223  sqrlearg  44253  uzinico  44260  preimaiocmnf  44261  limcresiooub  44345  limclr  44358  climeldmeq  44368  limsuppnflem  44413  limsupmnflem  44423  limsupmnfuzlem  44429  limsupre3lem  44435  limsupre3uzlem  44438  liminfreuzlem  44505  dvnmul  44646  dvmptfprodlem  44647  ismbl3  44689  ismbl4  44696  fourierdlem50  44859  fourierdlem89  44898  fourierdlem91  44900  dfsalgen2  45044  sge0repnf  45089  sge0lefi  45101  sge0resplit  45109  sge0fodjrnlem  45119  voliunsge0lem  45175  hspdifhsp  45319  isvonmbl  45341  ovnovollem3  45361  vonvolmbl  45364  pimrecltpos  45411  preimaicomnf  45414  pimrecltneg  45427  issmflem  45430  issmfle  45448  issmfgt  45459  smfaddlem1  45466  issmfge  45473  smfresal  45491  smflimmpt  45513  smfinflem  45520  smflimsuplem7  45529  smflimsupmpt  45532  sigarcol  45567  confun  45636  or2expropbi  45731  fsetsniunop  45746  fcoresf1b  45767  f1cof1b  45772  funfocofob  45773  rexsb  45794  euoreqb  45804  ralbinrald  45817  rlimdmafv  45872  fafv2elrnb  45930  tz6.12c-afv2  45937  dfatbrafv2b  45940  fnbrafv2b  45943  rlimdmafv2  45953  f1oresf1o2  45986  el1fzopredsuc  46020  2ffzoeq  46023  imasetpreimafvbijlemfo  46060  iccpartiun  46089  ichnfb  46120  ich2exprop  46126  sprsymrelfolem2  46148  paireqne  46166  prprelprb  46172  reupr  46177  requad01  46276  requad1  46277  requad2  46278  dfodd6  46292  dfeven4  46293  evensumeven  46362  sbgoldbalt  46436  isomushgr  46481  isomuspgr  46489  isomgrsymb  46492  isassintop  46607  uzlidlring  46781  rngciso  46834  rngcisoALTV  46846  ringciso  46885  ringcisoALTV  46909  domnmsuppn0  46999  lindslininds  47099  snlindsntor  47106  isldepslvec2  47120  affinecomb1  47342  prelrrx2b  47354  rrx2plord2  47362  eenglngeehlnm  47379  rrx2vlinest  47381  line2xlem  47393  line2x  47394  line2y  47395  itsclc0xyqsolb  47410  itsclquadb  47416  mpbiran3d  47436  rspceb2dv  47442  opnneieqv  47497  iscnrm3lem2  47521  fullthinc2  47621  thincciso  47623