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  342  pm5.501  367  2falsedOLD  378  impbida  798  dedlem0b  1042  dedlema  1043  dedlemb  1044  albi  1821  alexbii  1836  equequ1  2029  equequ2  2030  spsbbi  2077  elequ1  2114  elequ2  2122  sbequ12  2245  sbft  2263  cbv2w  2335  exsb  2358  dral1v  2368  dral1vOLD  2369  cbv2  2404  cbv2h  2407  ax12b  2425  dral1  2440  dral1ALT  2441  eupickb  2638  eupickbi  2639  2eu2  2655  ralbi  3090  ralbida  3160  rexbi  3174  ceqsalt  3463  vtoclgft  3493  rspcebdv  3556  ceqex  3583  mob2  3651  reu6  3662  sbciegft  3755  sbcg  3796  2reu2  3832  csbiebt  3863  sseq1  3947  ss2abdv  3998  ssdifsym  4198  reupick  4253  reupick2  4255  ab0OLD  4310  uneqdifeq  4424  prnebg  4787  preqsnd  4790  prel12g  4795  iuneqconst  4936  disjeq2  5044  disjeq1  5047  disjss3  5074  reusv2lem2  5323  reusv2lem3  5324  alxfr  5331  ralxfrd  5332  ralxfrd2  5336  copsexgw  5405  copsexg  5406  snopeqop  5421  euotd  5428  poeq2  5508  sotric  5532  sotrieq  5533  freq2  5561  seeq1  5562  seeq2  5563  iss  5946  tz7.7  6296  ordtri1  6303  ordelinel  6368  iotaval  6411  funeq  6461  funssres  6485  f0dom0  6667  tz6.12c  6808  fnbrfvb  6831  ssimaex  6862  fvimacnv  6939  elpreima  6944  eldmrexrnb  6977  fsn  7016  fnsnb  7047  fmptsng  7049  fmptsnd  7050  fprb  7078  tpres  7085  fconst2g  7087  fconst5  7090  elunirn  7133  f1ocnvfvb  7160  f1prex  7165  foeqcnvco  7181  f1eqcocnv  7182  f1eqcocnvOLD  7183  fliftfun  7192  soisores  7207  isofr  7222  isose  7223  isopo  7226  isoso  7228  f1oiso2  7232  eusvobj2  7277  oprabidw  7315  oprabid  7316  f1opw2  7533  oneqmin  7659  ordsuc  7670  ordelsuc  7676  ordsucelsuc  7678  ordunisuc2  7700  limsuc  7705  fndmexb  7764  f1ovv  7809  op1steq  7884  opreuopreu  7885  funeldmdif  7898  fvn0elsuppb  8006  extmptsuppeq  8013  rntpos  8064  smoiso2  8209  seqomlem2  8291  oaord  8387  oawordex  8397  oaordex  8398  omord2  8407  om00  8415  oeord  8428  nnaord  8459  nnmord  8472  nnawordex  8477  nnaordex  8478  eldifsucnn  8503  erexb  8532  swoord1  8538  swoord2  8539  iiner  8587  eceqoveq  8620  mapsnd  8683  ralxpmap  8693  omxpenlem  8869  domtriord  8919  mapxpen  8939  mapunen  8942  ssenen  8947  enfi  8982  nneneq  9001  nndomog  9008  nneneqOLD  9013  nndomogOLD  9018  onomeneq  9020  onomeneqOLD  9021  en1eqsnbi  9058  fodomfib  9102  f1opwfi  9132  fsuppunbi  9158  elfiun  9198  suplub2  9229  ordiso2  9283  ordiso  9284  oieu  9307  brwdom2  9341  brwdom3  9350  cantnflem1  9456  ttrclselem2  9493  cardidm  9726  carddom2  9744  pm54.43  9768  pr2ne  9770  acnen  9818  acnen2  9820  alephord  9840  alephinit  9860  dfac5  9893  infdif2  9975  fictb  10010  coflim  10026  fincssdom  10088  fin23lem25  10089  isf32lem9  10126  isf34lem4  10142  fin1a2lem11  10175  axdc3lem2  10216  ficard  10330  fpwwe2lem11  10406  fpwwe2  10408  indpi  10672  nqereq  10700  1idpr  10794  ltapr  10810  leltne  11073  ltlen  11085  ltadd2  11088  addlsub  11400  addid0  11403  ltord1  11510  mul0or  11624  ldiv  11818  ltmul1  11834  mulge0b  11854  lt2msq  11869  negfi  11933  nnsub  12026  nn0sub  12292  zrevaddcl  12374  zltp1le  12379  zdiv  12399  nneo  12413  zeo2  12416  zmax  12694  zbtwnre  12695  qrevaddcl  12720  xrlttri  12882  xrleltne  12888  xralrple  12948  xltneg  12960  xleadd1  12998  xlemul1  13033  supxrunb1  13062  supxrunb2  13063  ioo0  13113  iccid  13133  ico0  13134  ioc0  13135  icc0  13136  difreicc  13225  iccsplit  13226  zltaddlt1le  13246  0fz1  13285  uzsplit  13337  fzm1  13345  fzrevral  13350  ssfzo12bi  13491  elfznelfzob  13502  flge  13534  modid2  13627  modmuladd  13642  ssnn0fi  13714  seqf1olem1  13771  hashen  14070  hashdom  14103  hash2exprb  14194  pr2pwpr  14202  hashtpg  14208  len0nnbi  14263  ccats1pfxeqbi  14464  reuccatpfxs1  14469  repsdf2  14500  scshwfzeqfzo  14548  relexpindlem  14783  shftlem  14788  shftuz  14789  abslt  15035  absle  15036  rexico  15074  cau3lem  15075  reusq0  15183  rlim2lt  15215  rlim3  15216  o1lo1  15255  rlimdm  15269  climshft  15294  o1dif  15348  isercolllem2  15386  isercoll  15388  zsum  15439  fsum  15441  fsum00  15519  incexclem  15557  zprod  15656  fprod  15660  dvdsval2  15975  moddvds  15983  negdvdsb  15991  dvdsnegb  15992  dvdscmulr  16003  dvdsmulcr  16004  dvdssub2  16019  dvdsaddre2b  16025  fzo0dvdseq  16041  mod2eq1n2dvds  16065  ltoddhalfle  16079  sumodd  16106  bitsf1ocnv  16160  sadcaddlem  16173  bitsuz  16190  dvdsgcdb  16262  gcdzeq  16271  dvdssqlem  16280  lcmeq0  16314  lcmdvdsb  16327  lcmfeq0b  16344  lcmf  16347  lcmfdvdsb  16357  coprmgcdb  16363  cncongr  16383  isprm2lem  16395  dvdsprime  16401  dvdsprm  16417  isprm7  16422  coprm  16425  euclemma  16427  rpexp  16436  prmdvdsncoprmbd  16440  prmdiveq  16496  hashgcdlem  16498  odzdvds  16505  pythagtrip  16544  pc2dvds  16589  pcprmpw2  16592  pcprmpw  16593  vdwapun  16684  ramtcl2  16721  firest  17152  mrieqv2d  17357  isacs2  17371  isssc  17541  setciso  17815  posasymb  18046  pleval2  18064  pltval3  18066  lublecllem  18087  joinle  18113  meetle  18127  latdisd  18224  lubun  18242  clatleglb  18245  letsr  18320  intopsn  18347  gsumval2a  18378  frmdss2  18511  isgrpid2  18625  isgrpinv  18641  symg1bas  19007  oddvdsnn0  19161  oddvds  19164  odeq  19167  odeq1  19176  gexdvds  19198  pgpfi  19219  pgpssslw  19228  fislw  19239  sylow3lem2  19242  lsmelvalm  19265  lsmlub  19279  lsmss1b  19281  lsmss2b  19283  efgs1b  19351  cyggenod  19493  cyggexb  19509  dprdfeq0  19634  ablsimpgfind  19722  ringinvnz1ne0  19840  ringinvnzdiv  19841  unitmulclb  19916  dvreq1  19944  f1ghm0to0  19993  f1rhm0to0ALT  19994  drngmul0or  20021  isabvd  20089  issrngd  20130  lssats2  20271  lspsneq0  20283  lsmelval2  20356  lvecvs0or  20379  lspsneq  20393  lspsneu  20394  lidl1el  20498  lidldvgen  20535  isnzr2  20543  0ringnnzr  20549  0ring01eqbi  20553  rrgeq0  20570  domneq0  20577  znunit  20780  psgndif  20816  ipeq0  20852  ocvsscon  20889  pjdm2  20927  obselocv  20944  islinds4  21051  ply1coe1eq  21478  cply1coe0bi  21480  mat1dimelbas  21629  cramer  21849  toponcomb  22087  tgss3  22145  clsval2  22210  isopn3  22226  elcls3  22243  opncldf1  22244  neiint  22264  neips  22273  opnneissb  22274  opnssneib  22275  opnnei  22280  tpnei  22281  opnneiid  22286  restcld  22332  restopnb  22335  tgcn  22412  tgcnp  22413  subbascn  22414  iscnp4  22423  cnpnei  22424  cncls2  22433  cncls  22434  cnntr  22435  lmss  22458  hausnei2  22513  lpcls  22524  ordtt1  22539  cmpsub  22560  tgcmp  22561  1stcelcls  22621  locfincmp  22686  kgencn2  22717  ptpjpre1  22731  upxp  22783  txcn  22786  txlm  22808  tgqtop  22872  kqfvima  22890  isr0  22897  regr1lem2  22900  hmeoopn  22926  hmeocld  22927  ptuncnv  22967  fbunfip  23029  fgss2  23034  ufilb  23066  ufprim  23069  trufil  23070  cfinufil  23088  ufildr  23091  elfm2  23108  elfm3  23110  rnelfm  23113  fmfnfmlem4  23117  fmco  23121  flimtopon  23130  flimopn  23135  fbflim2  23137  flimrest  23143  flffbas  23155  cnpflf  23161  fclstopon  23172  fclsnei  23179  fclsbas  23181  fclsfnflim  23187  fclscmp  23190  ufilcmp  23192  isfcf  23194  fcfnei  23195  cnpfcf  23201  alexsubb  23206  alexsubALT  23211  cldsubg  23271  tgphaus  23277  tgpt0  23279  tsmsgsum  23299  tsmsres  23304  xbln0  23576  blssexps  23588  blssex  23589  isxms2  23610  prdsbl  23656  neibl  23666  metss  23673  met2ndc  23688  metrest  23689  metcnp3  23705  tngngp3  23829  nmoeq0  23909  xrsxmet  23981  reconn  24000  iccpnfcnv  24116  fgcfil  24444  iscau4  24452  cfilres  24469  iunmbl2  24730  ismbf3d  24827  mbfaddlem  24833  i1faddlem  24866  i1fmullem  24867  ellimc3  25052  tdeglem4  25233  tdeglem4OLD  25234  deg1nn0clb  25264  deg1lt0  25265  dvdsq1p  25334  plypf1  25382  0dgrb  25416  plymul0or  25450  ulmshft  25558  ulmcaulem  25562  ulmcau  25563  cosord  25696  eff1olem  25713  lognegb  25754  eflogeq  25766  logdivlt  25785  efopn  25822  cxpeq0  25842  cxpeq  25919  angpieqvd  25990  dcubic  26005  asinsinb  26056  acoscosb  26057  atantanb  26083  rlimcnp  26124  isppw  26272  isppw2  26273  vmappw  26274  isnsqf  26293  ppieq0  26334  fsumdvdsdiag  26342  dvdsppwf1o  26344  fsumfldivdiag  26348  chpeq0  26365  chteq0  26366  dchrptlem1  26421  lgsdir2lem4  26485  lgsne0  26492  lgsqr  26508  lgsdchrval  26511  gausslemma2dlem1a  26522  lgsquadlem1  26537  m1lgs  26545  2sqreultblem  26605  2sqreunnltblem  26608  iscgrglt  26884  brbtwn  27276  brcgr  27277  brbtwn2  27282  axcontlem7  27347  uhgr0vb  27451  edglnl  27522  ausgrusgrb  27544  ushgredgedg  27605  ushgredgedgloop  27607  usgr0vb  27613  usgr1v  27632  nbupgr  27720  nbumgrvtx  27722  nbuhgr2vtx1edgb  27728  edgusgrnbfin  27749  nb3grprlem1  27756  uvtxnbvtxm1  27782  cusgrfilem2  27832  uhgr0edg0rgrb  27950  cusgrm1rusgr  27958  spthonepeq  28129  usgr2pth  28141  wlkiswwlks  28250  wlkiswwlkupgr  28252  wlklnwwlkn  28258  wlklnwwlknupgr  28260  wwlksnextbi  28268  wwlksnredwwlkn0  28270  wwlksnextwrd  28271  wwlksnextprop  28286  umgrwwlks2on  28331  elwspths2on  28334  usgr2wspthons3  28338  elwwlks2  28340  elwspths2spth  28341  clwlkclwwlklem3  28374  loopclwwlkn1b  28415  clwwlknon1sn  28473  clwwlknonwwlknonb  28479  umgr3v3e3cycl  28557  eupth2lem3lem4  28604  frgr0v  28635  frgr3vlem2  28647  2clwwlk2clwwlk  28723  wlkl0  28740  grpoinvf  28903  nvmul0or  29021  nvz  29040  diporthcom  29087  ubthlem3  29243  hvmul0or  29396  his6  29470  hial0  29473  hial02  29474  orthcom  29479  normgt0  29498  ocin  29667  occon3  29668  shsel3  29686  shlub  29785  chssoc  29867  h1de2bi  29925  spansncol  29939  elspansn4  29944  spansnss2  29946  sumspansn  30020  lnopcnbd  30407  lnfncnbd  30428  riesz1  30436  elpjrn  30561  cvcon3  30655  dmdmd  30671  dmdbr3  30676  dmdbr4  30677  dmdbr5  30679  mdslmd1i  30700  atcveq0  30719  chcv1  30726  atssma  30749  atcv0eq  30750  atcv1  30751  bian1d  30818  disjeq1f  30921  br8d  30959  fpwrelmap  31077  xaddeq0  31085  eliccelico  31107  elicoelioo  31108  isarchiofld  31525  unitdivcld  31860  xrge0iifcnv  31892  lmxrge0  31911  indf1ofs  32003  eulerpartlemgh  32354  dstfrvunirn  32450  fnrelpredd  33070  loop1cycl  33108  cusgracyclt3v  33127  cvmliftmolem2  33253  cvmlift2lem12  33285  satfvsucsuc  33336  satfdm  33340  fmlasuc  33357  satffunlem1lem2  33374  satffunlem2lem2  33377  mthmb  33552  climuzcnv  33638  br8  33732  br6  33733  br4  33734  funbreq  33753  axextbdist  33785  nodenselem8  33903  oldlim  34078  sltlpss  34096  dfrdg4  34262  cgrcom  34301  cgrcoml  34307  cgrdegen  34315  btwncom  34325  brsegle  34419  brsegle2  34420  colinbtwnle  34429  btwnoutside  34436  broutsideof3  34437  outsidele  34443  lineunray  34458  lineelsb2  34459  elhf2  34486  elicc3  34515  nn0prpwlem  34520  opnbnd  34523  cldbnd  34524  opnregcld  34528  cldregopn  34529  fnessref  34555  refssfne  34556  neibastop2  34559  fnemeet2  34565  fnejoin2  34567  fgmin  34568  ontgval  34629  ordtop  34634  ordcmp  34645  nndivsub  34655  bj-19.21t  34960  bj-19.23t  34961  bj-19.42t  34964  bj-sbft  34966  bj-cbv2hv  34988  bj-equsal1t  35014  bj-19.21t0  35022  bj-ceqsalt0  35078  bj-ceqsalt1  35079  bj-xpnzexb  35160  bj-idreseq  35342  bj-imdiridlem  35365  bj-finsumval0  35465  bj-fvimacnv0  35466  bj-isrvec2  35480  bj-bary1  35492  dfgcd3  35504  isbasisrelowllem1  35535  isbasisrelowllem2  35536  finxpsuclem  35577  wl-lem-exsb  35730  wl-mo3t  35740  wl-ax11-lem1  35745  matunitlindf  35784  poimirlem6  35792  poimirlem7  35793  poimirlem16  35802  poimirlem19  35805  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  cnambfre  35834  itg2addnc  35840  brabg2  35883  istotbnd3  35938  sstotbnd2  35941  sstotbnd  35942  sstotbnd3  35943  ssbnd  35955  ismtybnd  35974  reheibor  36006  grpoeqdivid  36048  grpokerinj  36060  rngosn3  36091  rngoueqz  36107  1idl  36193  0rngo  36194  divrngidl  36195  igenval2  36233  ispridlc  36237  isdmn3  36241  relcnveq3  36463  iss2  36486  elrelscnveq3  36616  funALTVeq  36818  disjeq  36852  prtlem10  36886  prter2  36902  dral1-o  36925  lshpinN  37010  lsatcveq0  37053  lsatcv0eq  37068  lsatcv1  37069  islshpcv  37074  lkr0f  37115  lkrshp4  37129  lshpkrlem1  37131  lshpset2N  37140  lfl1dim  37142  lfl1dim2N  37143  lub0N  37210  glb0N  37214  oplecon3b  37221  cmtcomN  37270  cmtbr3N  37275  cmtbr4N  37276  cvrnbtwn2  37296  cvrnbtwn3  37297  cvrcon3b  37298  cvrnbtwn4  37300  cvrcmp  37304  atcvreq0  37335  atnle  37338  atlatle  37341  cvlexchb1  37351  cvlcvr1  37360  hlrelat2  37424  exatleN  37425  cvrval3  37434  cvrval4N  37435  cvrexch  37441  atcvr0eq  37447  lnnat  37448  atcvrj0  37449  atcvrj2b  37453  atltcvr  37456  atbtwn  37467  ps-1  37498  3at  37511  islln2a  37538  llncmp  37543  islpln2a  37569  lplncmp  37583  islvol2aN  37613  4at  37634  lvolcmp  37638  pmaple  37782  lncmp  37804  paddss  37866  llnexchb2lem  37889  2polcon4bN  37939  ispsubcl2N  37968  lhpat3  38067  lautcvr  38113  ltrnid  38156  trlval2  38184  trlatn0  38193  ltrnideq  38196  trlnidatb  38198  cdlemeg49lebilem  38560  trlord  38590  cdlemg1a  38591  cdlemg1cex  38609  tendoid0  38846  dva1dim  39006  cdlemm10N  39139  diarnN  39150  cdlemn  39233  dihlspsnssN  39353  dihatexv  39359  dochkrshp  39407  dochkrshp4  39410  djhlsmcl  39435  lcfl6  39521  lcfl8  39523  lcfrvalsnN  39562  lcfrlem9  39571  mapdval2N  39651  mapdordlem2  39658  mapd1o  39669  mapd0  39686  mapdheq2biN  39751  nnproddivdvdsd  40016  sticksstones11  40119  sticksstones22  40131  fnsnbt  40215  frlmfzowrdb  40242  frlmsnic  40270  dvdsexpnn  40347  mulgt0b2d  40437  prjspreln0  40455  elrfi  40523  diophrw  40588  eldioph2b  40592  diophin  40601  rexrabdioph  40623  rmxycomplete  40746  coprmdvdsb  40814  jm2.19  40822  jm2.26  40831  jm2.27  40837  limsuc2  40873  dgraa0p  40981  rngunsnply  41005  fiuneneq  41029  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  pwelg  41174  nzss  41942  dvconstbi  41959  expgrowth  41960  bcc0  41965  axc11next  42031  pm14.24  42057  sbiota1  42059  sbcim2g  42165  sineq0ALT  42564  pwssfi  42600  mapss2  42752  fsneq  42753  fsneqrn  42758  mapssbi  42760  ssmapsn  42763  rnmptbd2lem  42801  infnsuprnmpt  42803  rnmptbdlem  42808  xralrple2  42900  infxrunb2  42914  xralrple4  42919  xralrple3  42920  xrralrecnnle  42929  xrralrecnnge  42937  reclt0  42938  supxrunb3  42946  supxrleubrnmpt  42953  xrre4  42958  unb2ltle  42962  rexabslelem  42965  suprleubrnmpt  42969  infxrunb3rnmpt  42975  uzub  42978  supminfrnmpt  42992  iccintsng  43068  sqrlearg  43098  uzinico  43105  preimaiocmnf  43106  limcresiooub  43190  limclr  43203  climeldmeq  43213  limsuppnflem  43258  limsupmnflem  43268  limsupmnfuzlem  43274  limsupre3lem  43280  limsupre3uzlem  43283  liminfreuzlem  43350  dvnmul  43491  dvmptfprodlem  43492  ismbl3  43534  ismbl4  43541  fourierdlem50  43704  fourierdlem89  43743  fourierdlem91  43745  dfsalgen2  43887  sge0repnf  43931  sge0lefi  43943  sge0resplit  43951  sge0fodjrnlem  43961  voliunsge0lem  44017  hspdifhsp  44161  isvonmbl  44183  ovnovollem3  44203  vonvolmbl  44206  pimrecltpos  44253  preimaicomnf  44256  pimrecltneg  44269  issmflem  44272  issmfle  44290  issmfgt  44301  smfaddlem1  44308  issmfge  44315  smfresal  44333  smflimmpt  44354  smfinflem  44361  smflimsuplem7  44370  smflimsupmpt  44373  sigarcol  44391  confun  44445  or2expropbi  44539  fsetsniunop  44554  fcoresf1b  44575  f1cof1b  44580  funfocofob  44581  rexsb  44602  euoreqb  44612  ralbinrald  44625  rlimdmafv  44680  fafv2elrnb  44738  tz6.12c-afv2  44745  dfatbrafv2b  44748  fnbrafv2b  44751  rlimdmafv2  44761  f1oresf1o2  44794  el1fzopredsuc  44828  2ffzoeq  44831  imasetpreimafvbijlemfo  44868  iccpartiun  44897  ichnfb  44928  ich2exprop  44934  sprsymrelfolem2  44956  paireqne  44974  prprelprb  44980  reupr  44985  requad01  45084  requad1  45085  requad2  45086  dfodd6  45100  dfeven4  45101  evensumeven  45170  sbgoldbalt  45244  isomushgr  45289  isomuspgr  45297  isomgrsymb  45300  isassintop  45415  uzlidlring  45498  rngciso  45551  rngcisoALTV  45563  ringciso  45602  ringcisoALTV  45626  domnmsuppn0  45716  lindslininds  45816  snlindsntor  45823  isldepslvec2  45837  affinecomb1  46059  prelrrx2b  46071  rrx2plord2  46079  eenglngeehlnm  46096  rrx2vlinest  46098  line2xlem  46110  line2x  46111  line2y  46112  itsclc0xyqsolb  46127  itsclquadb  46133  mpbiran3d  46153  rspceb2dv  46159  opnneieqv  46215  iscnrm3lem2  46239  fullthinc2  46339  thincciso  46341