Theorem impbid 214

Description: Deduce an equivalence from two implications. Deduction associated with impbi 210 and impbii 211. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 213. (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 213	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 52	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bicom1  223  impbid1  227  impcon4bid  229  pm5.74  272  imbi1d  344  pm5.501  369  2falsedOLD  380  impbida  799  dedlem0b  1039  dedlema  1040  dedlemb  1041  albi  1819  alexbii  1833  equequ1  2032  equequ2  2033  spsbbi  2078  sbbidvOLD  2085  sbequOLD  2092  elequ1  2121  elequ2  2129  sbbidOLD  2248  sbequ12  2253  sbft  2270  sb56OLD  2278  sbequvvOLD  2335  cbv2w  2357  exsb  2378  dral1v  2387  cbv2  2423  cbv2h  2426  ax12b  2446  dral1  2461  dral1ALT  2462  sbequ12ALT  2581  sbftALT  2593  sbequALT  2597  eupickb  2720  eupickbi  2721  2eu2  2737  ralbi  3167  ceqsalt  3527  vtoclgft  3553  rspcebdv  3617  ceqex  3645  mob2  3706  reu6  3717  sbciegft  3808  2reu2  3882  csbiebt  3912  sseq1  3992  ssdifsym  4240  reupick  4287  reupick2  4289  uneqdifeq  4438  prnebg  4786  preqsnd  4789  prel12g  4794  iuneqconst  4930  disjeq2  5035  disjeq1  5038  disjss3  5065  reusv2lem2  5300  reusv2lem3  5301  alxfr  5308  ralxfrd  5309  ralxfrd2  5313  copsexgw  5381  copsexg  5382  snopeqop  5396  euotd  5403  poeq2  5478  sotric  5501  sotrieq  5502  freq2  5526  seeq1  5527  seeq2  5528  iss  5903  tz7.7  6217  ordtri1  6224  ordelinel  6289  iotaval  6329  funeq  6375  funssres  6398  f0dom0  6563  tz6.12c  6695  fnbrfvb  6718  ssimaex  6748  fvimacnv  6823  elpreima  6828  eldmrexrnb  6858  fsn  6897  fnsnb  6928  fmptsng  6930  fmptsnd  6931  fprb  6956  tpres  6963  fconst2g  6965  fconst5  6968  elunirn  7010  f1ocnvfvb  7036  f1prex  7040  foeqcnvco  7056  f1eqcocnv  7057  fliftfun  7065  soisores  7080  isofr  7095  isose  7096  isopo  7099  isoso  7101  f1oiso2  7105  eusvobj2  7149  oprabidw  7187  oprabid  7188  f1opw2  7400  oneqmin  7520  ordsuc  7529  ordelsuc  7535  ordsucelsuc  7537  ordunisuc2  7559  limsuc  7564  f1ovv  7659  op1steq  7733  opreuopreu  7734  funeldmdif  7747  fvn0elsuppb  7847  extmptsuppeq  7854  rntpos  7905  smoiso2  8006  seqomlem2  8087  oaord  8173  oawordex  8183  oaordex  8184  omord2  8193  om00  8201  oeord  8214  nnaord  8245  nnmord  8258  nnawordex  8263  nnaordex  8264  erexb  8314  swoord1  8320  swoord2  8321  iiner  8369  eceqoveq  8402  mapsnd  8450  ralxpmap  8460  omxpenlem  8618  domtriord  8663  mapxpen  8683  mapunen  8686  ssenen  8691  nneneq  8700  onomeneq  8708  nndomo  8712  en1eqsnbi  8749  fodomfib  8798  f1opwfi  8828  fsuppunbi  8854  elfiun  8894  suplub2  8925  ordiso2  8979  ordiso  8980  oieu  9003  brwdom2  9037  brwdom3  9046  cantnflem1  9152  cardidm  9388  carddom2  9406  pm54.43  9429  pr2ne  9431  acnen  9479  acnen2  9481  alephord  9501  alephinit  9521  dfac5  9554  infdif2  9632  fictb  9667  coflim  9683  fincssdom  9745  fin23lem25  9746  isf32lem9  9783  isf34lem4  9799  fin1a2lem11  9832  axdc3lem2  9873  ficard  9987  fpwwe2lem12  10063  fpwwe2  10065  indpi  10329  nqereq  10357  1idpr  10451  ltapr  10467  leltne  10730  ltlen  10741  ltadd2  10744  addlsub  11056  addid0  11059  ltord1  11166  mul0or  11280  ldiv  11474  ltmul1  11490  mulge0b  11510  lt2msq  11525  negfi  11589  nnsub  11682  nn0sub  11948  zrevaddcl  12028  zltp1le  12033  zdiv  12053  nneo  12067  zeo2  12070  zmax  12346  zbtwnre  12347  qrevaddcl  12371  xrlttri  12533  xrleltne  12539  xralrple  12599  xltneg  12611  xleadd1  12649  xlemul1  12684  supxrunb1  12713  supxrunb2  12714  ioo0  12764  iccid  12784  ico0  12785  ioc0  12786  icc0  12787  difreicc  12871  iccsplit  12872  zltaddlt1le  12891  0fz1  12928  uzsplit  12980  fzm1  12988  fzrevral  12993  ssfzo12bi  13133  elfznelfzob  13144  flge  13176  modid2  13267  modmuladd  13282  ssnn0fi  13354  seqf1olem1  13410  hashen  13708  hashdom  13741  hash2exprb  13830  pr2pwpr  13838  hashtpg  13844  len0nnbi  13903  ccats1pfxeqbi  14104  reuccatpfxs1  14109  repsdf2  14140  scshwfzeqfzo  14188  relexpindlem  14422  shftlem  14427  shftuz  14428  abslt  14674  absle  14675  rexico  14713  cau3lem  14714  reusq0  14822  rlim2lt  14854  rlim3  14855  o1lo1  14894  rlimdm  14908  climshft  14933  o1dif  14986  isercolllem2  15022  isercoll  15024  zsum  15075  fsum  15077  fsum00  15153  incexclem  15191  zprod  15291  fprod  15295  dvdsval2  15610  moddvds  15618  negdvdsb  15626  dvdsnegb  15627  dvdscmulr  15638  dvdsmulcr  15639  dvdssub2  15651  dvdsaddre2b  15657  fzo0dvdseq  15673  mod2eq1n2dvds  15696  ltoddhalfle  15710  sumodd  15739  bitsf1ocnv  15793  sadcaddlem  15806  bitsuz  15823  dvdsgcdb  15893  gcdzeq  15902  dvdssqlem  15910  lcmeq0  15944  lcmdvdsb  15957  lcmfeq0b  15974  lcmf  15977  lcmfdvdsb  15987  coprmgcdb  15993  cncongr  16013  isprm2lem  16025  dvdsprime  16031  dvdsprm  16047  isprm7  16052  coprm  16055  euclemma  16057  rpexp  16064  prmdiveq  16123  hashgcdlem  16125  odzdvds  16132  pythagtrip  16171  pc2dvds  16215  pcprmpw2  16218  pcprmpw  16219  vdwapun  16310  ramtcl2  16347  firest  16706  mrieqv2d  16910  isacs2  16924  isssc  17090  setciso  17351  posasymb  17562  pleval2  17575  pltval3  17577  lublecllem  17598  joinle  17624  meetle  17638  lubun  17733  clatleglb  17736  latdisd  17800  letsr  17837  intopsn  17864  gsumval2a  17895  frmdss2  18028  isgrpid2  18140  isgrpinv  18156  symg1bas  18519  oddvdsnn0  18672  oddvds  18675  odeq  18678  odeq1  18687  gexdvds  18709  pgpfi  18730  pgpssslw  18739  fislw  18750  sylow3lem2  18753  lsmelvalm  18776  lsmlub  18790  lsmss1b  18792  lsmss2b  18794  efgs1b  18862  cyggenod  19003  cyggexb  19019  dprdfeq0  19144  ablsimpgfind  19232  ringinvnz1ne0  19342  ringinvnzdiv  19343  unitmulclb  19415  dvreq1  19443  f1ghm0to0  19492  f1rhm0to0OLD  19493  f1rhm0to0ALT  19494  drngmul0or  19523  isabvd  19591  issrngd  19632  lssats2  19772  lspsneq0  19784  lsmelval2  19857  lvecvs0or  19880  lspsneq  19894  lspsneu  19895  lidl1el  19991  lidldvgen  20028  isnzr2  20036  0ringnnzr  20042  0ring01eqbi  20046  rrgeq0  20063  domneq0  20070  ply1coe1eq  20466  cply1coe0bi  20468  znunit  20710  psgndif  20746  ipeq0  20782  ocvsscon  20819  pjdm2  20855  obselocv  20872  islinds4  20979  mat1dimelbas  21080  cramer  21300  toponcomb  21537  tgss3  21594  clsval2  21658  isopn3  21674  elcls3  21691  opncldf1  21692  neiint  21712  neips  21721  opnneissb  21722  opnssneib  21723  opnnei  21728  tpnei  21729  opnneiid  21734  restcld  21780  restopnb  21783  tgcn  21860  tgcnp  21861  subbascn  21862  iscnp4  21871  cnpnei  21872  cncls2  21881  cncls  21882  cnntr  21883  lmss  21906  hausnei2  21961  lpcls  21972  ordtt1  21987  cmpsub  22008  tgcmp  22009  1stcelcls  22069  locfincmp  22134  kgencn2  22165  ptpjpre1  22179  upxp  22231  txcn  22234  txlm  22256  tgqtop  22320  kqfvima  22338  isr0  22345  regr1lem2  22348  hmeoopn  22374  hmeocld  22375  ptuncnv  22415  fbunfip  22477  fgss2  22482  ufilb  22514  ufprim  22517  trufil  22518  cfinufil  22536  ufildr  22539  elfm2  22556  elfm3  22558  rnelfm  22561  fmfnfmlem4  22565  fmco  22569  flimtopon  22578  flimopn  22583  fbflim2  22585  flimrest  22591  flffbas  22603  cnpflf  22609  fclstopon  22620  fclsnei  22627  fclsbas  22629  fclsfnflim  22635  fclscmp  22638  ufilcmp  22640  isfcf  22642  fcfnei  22643  cnpfcf  22649  alexsubb  22654  alexsubALT  22659  cldsubg  22719  tgphaus  22725  tgpt0  22727  tsmsgsum  22747  tsmsres  22752  xbln0  23024  blssexps  23036  blssex  23037  isxms2  23058  prdsbl  23101  neibl  23111  metss  23118  met2ndc  23133  metrest  23134  metcnp3  23150  tngngp3  23265  nmoeq0  23345  xrsxmet  23417  reconn  23436  iccpnfcnv  23548  fgcfil  23874  iscau4  23882  cfilres  23899  iunmbl2  24158  ismbf3d  24255  mbfaddlem  24261  i1faddlem  24294  i1fmullem  24295  ellimc3  24477  tdeglem4  24654  deg1nn0clb  24684  deg1lt0  24685  dvdsq1p  24754  plypf1  24802  0dgrb  24836  plymul0or  24870  ulmshft  24978  ulmcaulem  24982  ulmcau  24983  cosord  25116  eff1olem  25132  lognegb  25173  eflogeq  25185  logdivlt  25204  efopn  25241  cxpeq0  25261  cxpeq  25338  angpieqvd  25409  dcubic  25424  asinsinb  25475  acoscosb  25476  atantanb  25502  rlimcnp  25543  isppw  25691  isppw2  25692  vmappw  25693  isnsqf  25712  ppieq0  25753  fsumdvdsdiag  25761  dvdsppwf1o  25763  fsumfldivdiag  25767  chpeq0  25784  chteq0  25785  dchrptlem1  25840  lgsdir2lem4  25904  lgsne0  25911  lgsqr  25927  lgsdchrval  25930  gausslemma2dlem1a  25941  lgsquadlem1  25956  m1lgs  25964  2sqreultblem  26024  2sqreunnltblem  26027  iscgrglt  26300  brbtwn  26685  brcgr  26686  brbtwn2  26691  axcontlem7  26756  uhgr0vb  26857  edglnl  26928  ausgrusgrb  26950  ushgredgedg  27011  ushgredgedgloop  27013  usgr0vb  27019  usgr1v  27038  nbupgr  27126  nbumgrvtx  27128  nbuhgr2vtx1edgb  27134  edgusgrnbfin  27155  nb3grprlem1  27162  uvtxnbvtxm1  27188  cusgrfilem2  27238  uhgr0edg0rgrb  27356  cusgrm1rusgr  27364  spthonepeq  27533  usgr2pth  27545  wlkiswwlks  27654  wlkiswwlkupgr  27656  wlklnwwlkn  27662  wlklnwwlknupgr  27664  wwlksnextbi  27672  wwlksnredwwlkn0  27674  wwlksnextwrd  27675  wwlksnextprop  27691  umgrwwlks2on  27736  elwspths2on  27739  usgr2wspthons3  27743  elwwlks2  27745  elwspths2spth  27746  clwlkclwwlklem3  27779  loopclwwlkn1b  27820  clwwlknon1sn  27879  clwwlknonwwlknonb  27885  umgr3v3e3cycl  27963  eupth2lem3lem4  28010  frgr0v  28041  frgr3vlem2  28053  2clwwlk2clwwlk  28129  wlkl0  28146  grpoinvf  28309  nvmul0or  28427  nvz  28446  diporthcom  28493  ubthlem3  28649  hvmul0or  28802  his6  28876  hial0  28879  hial02  28880  orthcom  28885  normgt0  28904  ocin  29073  occon3  29074  shsel3  29092  shlub  29191  chssoc  29273  h1de2bi  29331  spansncol  29345  elspansn4  29350  spansnss2  29352  sumspansn  29426  lnopcnbd  29813  lnfncnbd  29834  riesz1  29842  elpjrn  29967  cvcon3  30061  dmdmd  30077  dmdbr3  30082  dmdbr4  30083  dmdbr5  30085  mdslmd1i  30106  atcveq0  30125  chcv1  30132  atssma  30155  atcv0eq  30156  atcv1  30157  bian1d  30224  disjeq1f  30323  br8d  30361  fpwrelmap  30469  xaddeq0  30477  eliccelico  30500  elicoelioo  30501  isarchiofld  30890  unitdivcld  31144  xrge0iifcnv  31176  lmxrge0  31195  indf1ofs  31285  eulerpartlemgh  31636  dstfrvunirn  31732  loop1cycl  32384  cusgracyclt3v  32403  cvmliftmolem2  32529  cvmlift2lem12  32561  satfvsucsuc  32612  satfdm  32616  fmlasuc  32633  satffunlem1lem2  32650  satffunlem2lem2  32653  mthmb  32828  climuzcnv  32914  br8  32992  br6  32993  br4  32994  funbreq  33013  axextbdist  33045  nodenselem8  33195  dfrdg4  33412  cgrcom  33451  cgrcoml  33457  cgrdegen  33465  btwncom  33475  brsegle  33569  brsegle2  33570  colinbtwnle  33579  btwnoutside  33586  broutsideof3  33587  outsidele  33593  lineunray  33608  lineelsb2  33609  elhf2  33636  elicc3  33665  nn0prpwlem  33670  opnbnd  33673  cldbnd  33674  opnregcld  33678  cldregopn  33679  fnessref  33705  refssfne  33706  neibastop2  33709  fnemeet2  33715  fnejoin2  33717  fgmin  33718  ontgval  33779  ordtop  33784  ordcmp  33795  nndivsub  33805  bj-19.21t  34098  bj-19.23t  34099  bj-19.42t  34102  bj-sbft  34104  bj-cbv2hv  34119  bj-equsal1t  34145  bj-19.21t0  34153  bj-ceqsalt0  34203  bj-ceqsalt1  34204  bj-xpnzexb  34276  bj-idreseq  34457  bj-finsumval0  34570  bj-fvimacnv0  34571  bj-isrvec2  34584  bj-bary1  34596  dfgcd3  34608  isbasisrelowllem1  34639  isbasisrelowllem2  34640  finxpsuclem  34681  wl-lem-exsb  34817  wl-mo3t  34827  wl-ax11-lem1  34832  matunitlindf  34905  poimirlem6  34913  poimirlem7  34914  poimirlem16  34923  poimirlem19  34926  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  cnambfre  34955  itg2addnc  34961  brabg2  35006  istotbnd3  35064  sstotbnd2  35067  sstotbnd  35068  sstotbnd3  35069  ssbnd  35081  ismtybnd  35100  reheibor  35132  grpoeqdivid  35174  grpokerinj  35186  rngosn3  35217  rngoueqz  35233  1idl  35319  0rngo  35320  divrngidl  35321  igenval2  35359  ispridlc  35363  isdmn3  35367  relcnveq3  35593  iss2  35616  elrelscnveq3  35746  funALTVeq  35948  disjeq  35982  prtlem10  36016  prter2  36032  dral1-o  36055  lshpinN  36140  lsatcveq0  36183  lsatcv0eq  36198  lsatcv1  36199  islshpcv  36204  lkr0f  36245  lkrshp4  36259  lshpkrlem1  36261  lshpset2N  36270  lfl1dim  36272  lfl1dim2N  36273  lub0N  36340  glb0N  36344  oplecon3b  36351  cmtcomN  36400  cmtbr3N  36405  cmtbr4N  36406  cvrnbtwn2  36426  cvrnbtwn3  36427  cvrcon3b  36428  cvrnbtwn4  36430  cvrcmp  36434  atcvreq0  36465  atnle  36468  atlatle  36471  cvlexchb1  36481  cvlcvr1  36490  hlrelat2  36554  exatleN  36555  cvrval3  36564  cvrval4N  36565  cvrexch  36571  atcvr0eq  36577  lnnat  36578  atcvrj0  36579  atcvrj2b  36583  atltcvr  36586  atbtwn  36597  ps-1  36628  3at  36641  islln2a  36668  llncmp  36673  islpln2a  36699  lplncmp  36713  islvol2aN  36743  4at  36764  lvolcmp  36768  pmaple  36912  lncmp  36934  paddss  36996  llnexchb2lem  37019  2polcon4bN  37069  ispsubcl2N  37098  lhpat3  37197  lautcvr  37243  ltrnid  37286  trlval2  37314  trlatn0  37323  ltrnideq  37326  trlnidatb  37328  cdlemeg49lebilem  37690  trlord  37720  cdlemg1a  37721  cdlemg1cex  37739  tendoid0  37976  dva1dim  38136  cdlemm10N  38269  diarnN  38280  cdlemn  38363  dihlspsnssN  38483  dihatexv  38489  dochkrshp  38537  dochkrshp4  38540  djhlsmcl  38565  lcfl6  38651  lcfl8  38653  lcfrvalsnN  38692  lcfrlem9  38701  mapdval2N  38781  mapdordlem2  38788  mapd1o  38799  mapd0  38816  mapdheq2biN  38881  fnsnbt  39169  frlmfzowrdb  39192  frlmsnic  39198  prjspreln0  39308  elrfi  39340  diophrw  39405  eldioph2b  39409  diophin  39418  rexrabdioph  39440  rmxycomplete  39563  coprmdvdsb  39631  jm2.19  39639  jm2.26  39648  jm2.27  39654  limsuc2  39690  dgraa0p  39798  rngunsnply  39822  fiuneneq  39846  nndomog  39946  pwelg  39968  nzss  40698  dvconstbi  40715  expgrowth  40716  bcc0  40721  axc11next  40787  pm14.24  40813  sbiota1  40815  sbcim2g  40921  sineq0ALT  41320  pwssfi  41356  mapss2  41517  fsneq  41518  fsneqrn  41523  mapssbi  41525  ssmapsn  41528  rnmptbd2lem  41569  infnsuprnmpt  41571  rnmptbdlem  41576  xralrple2  41671  infxrunb2  41685  xralrple4  41690  xralrple3  41691  xrralrecnnle  41702  xrralrecnnge  41711  reclt0  41712  supxrunb3  41721  supxrleubrnmpt  41728  xrre4  41734  unb2ltle  41738  rexabslelem  41741  suprleubrnmpt  41745  infxrunb3rnmpt  41751  uzub  41754  supminfrnmpt  41768  iccintsng  41848  sqrlearg  41878  uzinico  41885  preimaiocmnf  41886  limcresiooub  41972  limclr  41985  climeldmeq  41995  limsuppnflem  42040  limsupmnflem  42050  limsupmnfuzlem  42056  limsupre3lem  42062  limsupre3uzlem  42065  liminfreuzlem  42132  dvnmul  42277  dvmptfprodlem  42278  ismbl3  42320  ismbl4  42327  fourierdlem50  42490  fourierdlem89  42529  fourierdlem91  42531  dfsalgen2  42673  sge0repnf  42717  sge0lefi  42729  sge0resplit  42737  sge0fodjrnlem  42747  voliunsge0lem  42803  hspdifhsp  42947  isvonmbl  42969  ovnovollem3  42989  vonvolmbl  42992  pimrecltpos  43036  preimaicomnf  43039  pimrecltneg  43050  issmflem  43053  issmfle  43071  issmfgt  43082  smfaddlem1  43088  issmfge  43095  smfresal  43112  smflimmpt  43133  smfinflem  43140  smflimsuplem7  43149  smflimsupmpt  43152  sigarcol  43170  confun  43224  or2expropbi  43318  rexsb  43346  euoreqb  43357  ralbinrald  43370  rlimdmafv  43425  fafv2elrnb  43483  tz6.12c-afv2  43490  dfatbrafv2b  43493  fnbrafv2b  43496  rlimdmafv2  43506  f1oresf1o2  43539  el1fzopredsuc  43574  2ffzoeq  43577  imasetpreimafvbijlemfo  43614  iccpartiun  43643  ichnfb  43674  ich2exprop  43682  sprsymrelfolem2  43704  paireqne  43722  prprelprb  43728  reupr  43733  requad01  43835  requad1  43836  requad2  43837  dfodd6  43851  dfeven4  43852  evensumeven  43921  sbgoldbalt  43995  isomushgr  44040  isomuspgr  44048  isomgrsymb  44051  isassintop  44166  uzlidlring  44249  rngciso  44302  rngcisoALTV  44314  ringciso  44353  ringcisoALTV  44377  domnmsuppn0  44466  lindslininds  44568  snlindsntor  44575  isldepslvec2  44589  affinecomb1  44738  prelrrx2b  44750  rrx2plord2  44758  eenglngeehlnm  44775  rrx2vlinest  44777  line2xlem  44789  line2x  44790  line2y  44791  itsclc0xyqsolb  44806  itsclquadb  44812