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  1822  alexbii  1836  equequ1  2029  equequ2  2030  spsbbi  2077  elequ1  2115  elequ2  2123  sbequ12  2247  sbft  2265  cbv2w  2336  exsb  2357  dral1v  2367  dral1vOLD  2368  cbv2  2403  cbv2h  2406  ax12b  2424  dral1  2439  dral1ALT  2440  eupickb  2637  eupickbi  2638  2eu2  2654  ralbi  3092  ralbida  3156  rexbi  3169  ceqsalt  3452  vtoclgft  3482  rspcebdv  3545  ceqex  3574  mob2  3645  reu6  3656  sbciegft  3749  sbcg  3791  2reu2  3827  csbiebt  3858  sseq1  3942  ss2abdv  3993  ssdifsym  4194  reupick  4249  reupick2  4251  ab0OLD  4306  uneqdifeq  4420  prnebg  4783  preqsnd  4786  prel12g  4791  iuneqconst  4932  disjeq2  5039  disjeq1  5042  disjss3  5069  reusv2lem2  5317  reusv2lem3  5318  alxfr  5325  ralxfrd  5326  ralxfrd2  5330  copsexgw  5398  copsexg  5399  snopeqop  5414  euotd  5421  poeq2  5498  sotric  5522  sotrieq  5523  freq2  5551  seeq1  5552  seeq2  5553  iss  5932  tz7.7  6277  ordtri1  6284  ordelinel  6349  iotaval  6392  funeq  6438  funssres  6462  f0dom0  6642  tz6.12c  6781  fnbrfvb  6804  ssimaex  6835  fvimacnv  6912  elpreima  6917  eldmrexrnb  6950  fsn  6989  fnsnb  7020  fmptsng  7022  fmptsnd  7023  fprb  7051  tpres  7058  fconst2g  7060  fconst5  7063  elunirn  7106  f1ocnvfvb  7132  f1prex  7136  foeqcnvco  7152  f1eqcocnv  7153  f1eqcocnvOLD  7154  fliftfun  7163  soisores  7178  isofr  7193  isose  7194  isopo  7197  isoso  7199  f1oiso2  7203  eusvobj2  7248  oprabidw  7286  oprabid  7287  f1opw2  7502  oneqmin  7627  ordsuc  7636  ordelsuc  7642  ordsucelsuc  7644  ordunisuc2  7666  limsuc  7671  fndmexb  7729  f1ovv  7774  op1steq  7848  opreuopreu  7849  funeldmdif  7862  fvn0elsuppb  7968  extmptsuppeq  7975  rntpos  8026  smoiso2  8171  seqomlem2  8252  oaord  8340  oawordex  8350  oaordex  8351  omord2  8360  om00  8368  oeord  8381  nnaord  8412  nnmord  8425  nnawordex  8430  nnaordex  8431  erexb  8481  swoord1  8487  swoord2  8488  iiner  8536  eceqoveq  8569  mapsnd  8632  ralxpmap  8642  omxpenlem  8813  domtriord  8859  mapxpen  8879  mapunen  8882  ssenen  8887  nneneq  8896  nndomog  8904  enfi  8933  onomeneq  8943  en1eqsnbi  8978  fodomfib  9023  f1opwfi  9053  fsuppunbi  9079  elfiun  9119  suplub2  9150  ordiso2  9204  ordiso  9205  oieu  9228  brwdom2  9262  brwdom3  9271  cantnflem1  9377  cardidm  9648  carddom2  9666  pm54.43  9690  pr2ne  9692  acnen  9740  acnen2  9742  alephord  9762  alephinit  9782  dfac5  9815  infdif2  9897  fictb  9932  coflim  9948  fincssdom  10010  fin23lem25  10011  isf32lem9  10048  isf34lem4  10064  fin1a2lem11  10097  axdc3lem2  10138  ficard  10252  fpwwe2lem11  10328  fpwwe2  10330  indpi  10594  nqereq  10622  1idpr  10716  ltapr  10732  leltne  10995  ltlen  11006  ltadd2  11009  addlsub  11321  addid0  11324  ltord1  11431  mul0or  11545  ldiv  11739  ltmul1  11755  mulge0b  11775  lt2msq  11790  negfi  11854  nnsub  11947  nn0sub  12213  zrevaddcl  12295  zltp1le  12300  zdiv  12320  nneo  12334  zeo2  12337  zmax  12614  zbtwnre  12615  qrevaddcl  12640  xrlttri  12802  xrleltne  12808  xralrple  12868  xltneg  12880  xleadd1  12918  xlemul1  12953  supxrunb1  12982  supxrunb2  12983  ioo0  13033  iccid  13053  ico0  13054  ioc0  13055  icc0  13056  difreicc  13145  iccsplit  13146  zltaddlt1le  13166  0fz1  13205  uzsplit  13257  fzm1  13265  fzrevral  13270  ssfzo12bi  13410  elfznelfzob  13421  flge  13453  modid2  13546  modmuladd  13561  ssnn0fi  13633  seqf1olem1  13690  hashen  13989  hashdom  14022  hash2exprb  14113  pr2pwpr  14121  hashtpg  14127  len0nnbi  14182  ccats1pfxeqbi  14383  reuccatpfxs1  14388  repsdf2  14419  scshwfzeqfzo  14467  relexpindlem  14702  shftlem  14707  shftuz  14708  abslt  14954  absle  14955  rexico  14993  cau3lem  14994  reusq0  15102  rlim2lt  15134  rlim3  15135  o1lo1  15174  rlimdm  15188  climshft  15213  o1dif  15267  isercolllem2  15305  isercoll  15307  zsum  15358  fsum  15360  fsum00  15438  incexclem  15476  zprod  15575  fprod  15579  dvdsval2  15894  moddvds  15902  negdvdsb  15910  dvdsnegb  15911  dvdscmulr  15922  dvdsmulcr  15923  dvdssub2  15938  dvdsaddre2b  15944  fzo0dvdseq  15960  mod2eq1n2dvds  15984  ltoddhalfle  15998  sumodd  16025  bitsf1ocnv  16079  sadcaddlem  16092  bitsuz  16109  dvdsgcdb  16181  gcdzeq  16190  dvdssqlem  16199  lcmeq0  16233  lcmdvdsb  16246  lcmfeq0b  16263  lcmf  16266  lcmfdvdsb  16276  coprmgcdb  16282  cncongr  16302  isprm2lem  16314  dvdsprime  16320  dvdsprm  16336  isprm7  16341  coprm  16344  euclemma  16346  rpexp  16355  prmdvdsncoprmbd  16359  prmdiveq  16415  hashgcdlem  16417  odzdvds  16424  pythagtrip  16463  pc2dvds  16508  pcprmpw2  16511  pcprmpw  16512  vdwapun  16603  ramtcl2  16640  firest  17060  mrieqv2d  17265  isacs2  17279  isssc  17449  setciso  17722  posasymb  17952  pleval2  17970  pltval3  17972  lublecllem  17993  joinle  18019  meetle  18033  latdisd  18130  lubun  18148  clatleglb  18151  letsr  18226  intopsn  18253  gsumval2a  18284  frmdss2  18417  isgrpid2  18531  isgrpinv  18547  symg1bas  18913  oddvdsnn0  19067  oddvds  19070  odeq  19073  odeq1  19082  gexdvds  19104  pgpfi  19125  pgpssslw  19134  fislw  19145  sylow3lem2  19148  lsmelvalm  19171  lsmlub  19185  lsmss1b  19187  lsmss2b  19189  efgs1b  19257  cyggenod  19399  cyggexb  19415  dprdfeq0  19540  ablsimpgfind  19628  ringinvnz1ne0  19746  ringinvnzdiv  19747  unitmulclb  19822  dvreq1  19850  f1ghm0to0  19899  f1rhm0to0ALT  19900  drngmul0or  19927  isabvd  19995  issrngd  20036  lssats2  20177  lspsneq0  20189  lsmelval2  20262  lvecvs0or  20285  lspsneq  20299  lspsneu  20300  lidl1el  20402  lidldvgen  20439  isnzr2  20447  0ringnnzr  20453  0ring01eqbi  20457  rrgeq0  20474  domneq0  20481  znunit  20683  psgndif  20719  ipeq0  20755  ocvsscon  20792  pjdm2  20828  obselocv  20845  islinds4  20952  ply1coe1eq  21379  cply1coe0bi  21381  mat1dimelbas  21528  cramer  21748  toponcomb  21986  tgss3  22044  clsval2  22109  isopn3  22125  elcls3  22142  opncldf1  22143  neiint  22163  neips  22172  opnneissb  22173  opnssneib  22174  opnnei  22179  tpnei  22180  opnneiid  22185  restcld  22231  restopnb  22234  tgcn  22311  tgcnp  22312  subbascn  22313  iscnp4  22322  cnpnei  22323  cncls2  22332  cncls  22333  cnntr  22334  lmss  22357  hausnei2  22412  lpcls  22423  ordtt1  22438  cmpsub  22459  tgcmp  22460  1stcelcls  22520  locfincmp  22585  kgencn2  22616  ptpjpre1  22630  upxp  22682  txcn  22685  txlm  22707  tgqtop  22771  kqfvima  22789  isr0  22796  regr1lem2  22799  hmeoopn  22825  hmeocld  22826  ptuncnv  22866  fbunfip  22928  fgss2  22933  ufilb  22965  ufprim  22968  trufil  22969  cfinufil  22987  ufildr  22990  elfm2  23007  elfm3  23009  rnelfm  23012  fmfnfmlem4  23016  fmco  23020  flimtopon  23029  flimopn  23034  fbflim2  23036  flimrest  23042  flffbas  23054  cnpflf  23060  fclstopon  23071  fclsnei  23078  fclsbas  23080  fclsfnflim  23086  fclscmp  23089  ufilcmp  23091  isfcf  23093  fcfnei  23094  cnpfcf  23100  alexsubb  23105  alexsubALT  23110  cldsubg  23170  tgphaus  23176  tgpt0  23178  tsmsgsum  23198  tsmsres  23203  xbln0  23475  blssexps  23487  blssex  23488  isxms2  23509  prdsbl  23553  neibl  23563  metss  23570  met2ndc  23585  metrest  23586  metcnp3  23602  tngngp3  23726  nmoeq0  23806  xrsxmet  23878  reconn  23897  iccpnfcnv  24013  fgcfil  24340  iscau4  24348  cfilres  24365  iunmbl2  24626  ismbf3d  24723  mbfaddlem  24729  i1faddlem  24762  i1fmullem  24763  ellimc3  24948  tdeglem4  25129  tdeglem4OLD  25130  deg1nn0clb  25160  deg1lt0  25161  dvdsq1p  25230  plypf1  25278  0dgrb  25312  plymul0or  25346  ulmshft  25454  ulmcaulem  25458  ulmcau  25459  cosord  25592  eff1olem  25609  lognegb  25650  eflogeq  25662  logdivlt  25681  efopn  25718  cxpeq0  25738  cxpeq  25815  angpieqvd  25886  dcubic  25901  asinsinb  25952  acoscosb  25953  atantanb  25979  rlimcnp  26020  isppw  26168  isppw2  26169  vmappw  26170  isnsqf  26189  ppieq0  26230  fsumdvdsdiag  26238  dvdsppwf1o  26240  fsumfldivdiag  26244  chpeq0  26261  chteq0  26262  dchrptlem1  26317  lgsdir2lem4  26381  lgsne0  26388  lgsqr  26404  lgsdchrval  26407  gausslemma2dlem1a  26418  lgsquadlem1  26433  m1lgs  26441  2sqreultblem  26501  2sqreunnltblem  26504  iscgrglt  26779  brbtwn  27170  brcgr  27171  brbtwn2  27176  axcontlem7  27241  uhgr0vb  27345  edglnl  27416  ausgrusgrb  27438  ushgredgedg  27499  ushgredgedgloop  27501  usgr0vb  27507  usgr1v  27526  nbupgr  27614  nbumgrvtx  27616  nbuhgr2vtx1edgb  27622  edgusgrnbfin  27643  nb3grprlem1  27650  uvtxnbvtxm1  27676  cusgrfilem2  27726  uhgr0edg0rgrb  27844  cusgrm1rusgr  27852  spthonepeq  28021  usgr2pth  28033  wlkiswwlks  28142  wlkiswwlkupgr  28144  wlklnwwlkn  28150  wlklnwwlknupgr  28152  wwlksnextbi  28160  wwlksnredwwlkn0  28162  wwlksnextwrd  28163  wwlksnextprop  28178  umgrwwlks2on  28223  elwspths2on  28226  usgr2wspthons3  28230  elwwlks2  28232  elwspths2spth  28233  clwlkclwwlklem3  28266  loopclwwlkn1b  28307  clwwlknon1sn  28365  clwwlknonwwlknonb  28371  umgr3v3e3cycl  28449  eupth2lem3lem4  28496  frgr0v  28527  frgr3vlem2  28539  2clwwlk2clwwlk  28615  wlkl0  28632  grpoinvf  28795  nvmul0or  28913  nvz  28932  diporthcom  28979  ubthlem3  29135  hvmul0or  29288  his6  29362  hial0  29365  hial02  29366  orthcom  29371  normgt0  29390  ocin  29559  occon3  29560  shsel3  29578  shlub  29677  chssoc  29759  h1de2bi  29817  spansncol  29831  elspansn4  29836  spansnss2  29838  sumspansn  29912  lnopcnbd  30299  lnfncnbd  30320  riesz1  30328  elpjrn  30453  cvcon3  30547  dmdmd  30563  dmdbr3  30568  dmdbr4  30569  dmdbr5  30571  mdslmd1i  30592  atcveq0  30611  chcv1  30618  atssma  30641  atcv0eq  30642  atcv1  30643  bian1d  30710  disjeq1f  30813  br8d  30851  fpwrelmap  30970  xaddeq0  30978  eliccelico  31000  elicoelioo  31001  isarchiofld  31418  unitdivcld  31753  xrge0iifcnv  31785  lmxrge0  31804  indf1ofs  31894  eulerpartlemgh  32245  dstfrvunirn  32341  fnrelpredd  32961  loop1cycl  32999  cusgracyclt3v  33018  cvmliftmolem2  33144  cvmlift2lem12  33176  satfvsucsuc  33227  satfdm  33231  fmlasuc  33248  satffunlem1lem2  33265  satffunlem2lem2  33268  mthmb  33443  climuzcnv  33529  eldifsucnn  33597  br8  33629  br6  33630  br4  33631  funbreq  33650  axextbdist  33682  ttrclselem2  33712  nodenselem8  33821  oldlim  33996  sltlpss  34014  dfrdg4  34180  cgrcom  34219  cgrcoml  34225  cgrdegen  34233  btwncom  34243  brsegle  34337  brsegle2  34338  colinbtwnle  34347  btwnoutside  34354  broutsideof3  34355  outsidele  34361  lineunray  34376  lineelsb2  34377  elhf2  34404  elicc3  34433  nn0prpwlem  34438  opnbnd  34441  cldbnd  34442  opnregcld  34446  cldregopn  34447  fnessref  34473  refssfne  34474  neibastop2  34477  fnemeet2  34483  fnejoin2  34485  fgmin  34486  ontgval  34547  ordtop  34552  ordcmp  34563  nndivsub  34573  bj-19.21t  34878  bj-19.23t  34879  bj-19.42t  34882  bj-sbft  34884  bj-cbv2hv  34906  bj-equsal1t  34932  bj-19.21t0  34940  bj-ceqsalt0  34996  bj-ceqsalt1  34997  bj-xpnzexb  35078  bj-idreseq  35260  bj-imdiridlem  35283  bj-finsumval0  35383  bj-fvimacnv0  35384  bj-isrvec2  35398  bj-bary1  35410  dfgcd3  35422  isbasisrelowllem1  35453  isbasisrelowllem2  35454  finxpsuclem  35495  wl-lem-exsb  35648  wl-mo3t  35658  wl-ax11-lem1  35663  matunitlindf  35702  poimirlem6  35710  poimirlem7  35711  poimirlem16  35720  poimirlem19  35723  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  cnambfre  35752  itg2addnc  35758  brabg2  35801  istotbnd3  35856  sstotbnd2  35859  sstotbnd  35860  sstotbnd3  35861  ssbnd  35873  ismtybnd  35892  reheibor  35924  grpoeqdivid  35966  grpokerinj  35978  rngosn3  36009  rngoueqz  36025  1idl  36111  0rngo  36112  divrngidl  36113  igenval2  36151  ispridlc  36155  isdmn3  36159  relcnveq3  36383  iss2  36406  elrelscnveq3  36536  funALTVeq  36738  disjeq  36772  prtlem10  36806  prter2  36822  dral1-o  36845  lshpinN  36930  lsatcveq0  36973  lsatcv0eq  36988  lsatcv1  36989  islshpcv  36994  lkr0f  37035  lkrshp4  37049  lshpkrlem1  37051  lshpset2N  37060  lfl1dim  37062  lfl1dim2N  37063  lub0N  37130  glb0N  37134  oplecon3b  37141  cmtcomN  37190  cmtbr3N  37195  cmtbr4N  37196  cvrnbtwn2  37216  cvrnbtwn3  37217  cvrcon3b  37218  cvrnbtwn4  37220  cvrcmp  37224  atcvreq0  37255  atnle  37258  atlatle  37261  cvlexchb1  37271  cvlcvr1  37280  hlrelat2  37344  exatleN  37345  cvrval3  37354  cvrval4N  37355  cvrexch  37361  atcvr0eq  37367  lnnat  37368  atcvrj0  37369  atcvrj2b  37373  atltcvr  37376  atbtwn  37387  ps-1  37418  3at  37431  islln2a  37458  llncmp  37463  islpln2a  37489  lplncmp  37503  islvol2aN  37533  4at  37554  lvolcmp  37558  pmaple  37702  lncmp  37724  paddss  37786  llnexchb2lem  37809  2polcon4bN  37859  ispsubcl2N  37888  lhpat3  37987  lautcvr  38033  ltrnid  38076  trlval2  38104  trlatn0  38113  ltrnideq  38116  trlnidatb  38118  cdlemeg49lebilem  38480  trlord  38510  cdlemg1a  38511  cdlemg1cex  38529  tendoid0  38766  dva1dim  38926  cdlemm10N  39059  diarnN  39070  cdlemn  39153  dihlspsnssN  39273  dihatexv  39279  dochkrshp  39327  dochkrshp4  39330  djhlsmcl  39355  lcfl6  39441  lcfl8  39443  lcfrvalsnN  39482  lcfrlem9  39491  mapdval2N  39571  mapdordlem2  39578  mapd1o  39589  mapd0  39606  mapdheq2biN  39671  nnproddivdvdsd  39937  sticksstones11  40040  sticksstones22  40052  fnsnbt  40134  frlmfzowrdb  40161  frlmsnic  40188  dvdsexpnn  40261  mulgt0b2d  40351  prjspreln0  40369  elrfi  40432  diophrw  40497  eldioph2b  40501  diophin  40510  rexrabdioph  40532  rmxycomplete  40655  coprmdvdsb  40723  jm2.19  40731  jm2.26  40740  jm2.27  40746  limsuc2  40782  dgraa0p  40890  rngunsnply  40914  fiuneneq  40938  pwelg  41056  nzss  41824  dvconstbi  41841  expgrowth  41842  bcc0  41847  axc11next  41913  pm14.24  41939  sbiota1  41941  sbcim2g  42047  sineq0ALT  42446  pwssfi  42482  mapss2  42634  fsneq  42635  fsneqrn  42640  mapssbi  42642  ssmapsn  42645  rnmptbd2lem  42683  infnsuprnmpt  42685  rnmptbdlem  42690  xralrple2  42783  infxrunb2  42797  xralrple4  42802  xralrple3  42803  xrralrecnnle  42812  xrralrecnnge  42820  reclt0  42821  supxrunb3  42829  supxrleubrnmpt  42836  xrre4  42841  unb2ltle  42845  rexabslelem  42848  suprleubrnmpt  42852  infxrunb3rnmpt  42858  uzub  42861  supminfrnmpt  42875  iccintsng  42951  sqrlearg  42981  uzinico  42988  preimaiocmnf  42989  limcresiooub  43073  limclr  43086  climeldmeq  43096  limsuppnflem  43141  limsupmnflem  43151  limsupmnfuzlem  43157  limsupre3lem  43163  limsupre3uzlem  43166  liminfreuzlem  43233  dvnmul  43374  dvmptfprodlem  43375  ismbl3  43417  ismbl4  43424  fourierdlem50  43587  fourierdlem89  43626  fourierdlem91  43628  dfsalgen2  43770  sge0repnf  43814  sge0lefi  43826  sge0resplit  43834  sge0fodjrnlem  43844  voliunsge0lem  43900  hspdifhsp  44044  isvonmbl  44066  ovnovollem3  44086  vonvolmbl  44089  pimrecltpos  44133  preimaicomnf  44136  pimrecltneg  44147  issmflem  44150  issmfle  44168  issmfgt  44179  smfaddlem1  44185  issmfge  44192  smfresal  44209  smflimmpt  44230  smfinflem  44237  smflimsuplem7  44246  smflimsupmpt  44249  sigarcol  44267  confun  44321  or2expropbi  44415  fsetsniunop  44430  fcoresf1b  44451  f1cof1b  44456  funfocofob  44457  rexsb  44478  euoreqb  44488  ralbinrald  44501  rlimdmafv  44556  fafv2elrnb  44614  tz6.12c-afv2  44621  dfatbrafv2b  44624  fnbrafv2b  44627  rlimdmafv2  44637  f1oresf1o2  44670  el1fzopredsuc  44705  2ffzoeq  44708  imasetpreimafvbijlemfo  44745  iccpartiun  44774  ichnfb  44805  ich2exprop  44811  sprsymrelfolem2  44833  paireqne  44851  prprelprb  44857  reupr  44862  requad01  44961  requad1  44962  requad2  44963  dfodd6  44977  dfeven4  44978  evensumeven  45047  sbgoldbalt  45121  isomushgr  45166  isomuspgr  45174  isomgrsymb  45177  isassintop  45292  uzlidlring  45375  rngciso  45428  rngcisoALTV  45440  ringciso  45479  ringcisoALTV  45503  domnmsuppn0  45593  lindslininds  45693  snlindsntor  45700  isldepslvec2  45714  affinecomb1  45936  prelrrx2b  45948  rrx2plord2  45956  eenglngeehlnm  45973  rrx2vlinest  45975  line2xlem  45987  line2x  45988  line2y  45989  itsclc0xyqsolb  46004  itsclquadb  46010  mpbiran3d  46030  rspceb2dv  46036  opnneieqv  46092  iscnrm3lem2  46116  fullthinc2  46216  thincciso  46218