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  1815  alexbii  1829  equequ1  2028  equequ2  2029  spsbbi  2074  sbbidvOLD  2081  sbequOLD  2088  elequ1  2117  elequ2  2125  sbbidOLD  2244  sbequ12  2249  sbft  2266  sb56OLD  2274  sbequvvOLD  2331  cbv2w  2353  exsb  2374  dral1v  2383  cbv2  2419  cbv2h  2422  ax12b  2442  dral1  2457  dral1ALT  2458  sbequ12ALT  2577  sbftALT  2589  sbequALT  2593  eupickb  2716  eupickbi  2717  2eu2  2734  ralbi  3167  ceqsalt  3527  vtoclgft  3553  rspcebdv  3616  ceqex  3644  mob2  3705  reu6  3716  sbciegft  3807  2reu2  3881  csbiebt  3911  sseq1  3991  ssdifsym  4239  reupick  4286  reupick2  4288  uneqdifeq  4437  prnebg  4779  preqsnd  4782  prel12g  4787  iuneqconst  4922  disjeq2  5027  disjeq1  5030  disjss3  5057  reusv2lem2  5291  reusv2lem3  5292  alxfr  5299  ralxfrd  5300  ralxfrd2  5304  copsexgw  5373  copsexg  5374  snopeqop  5388  euotd  5395  poeq2  5472  sotric  5495  sotrieq  5496  freq2  5520  seeq1  5521  seeq2  5522  iss  5897  tz7.7  6211  ordtri1  6218  ordelinel  6283  iotaval  6323  funeq  6369  funssres  6392  f0dom0  6557  tz6.12c  6689  fnbrfvb  6712  ssimaex  6742  fvimacnv  6817  elpreima  6822  eldmrexrnb  6852  fsn  6891  fnsnb  6922  fmptsng  6924  fmptsnd  6925  fprb  6950  tpres  6957  fconst2g  6959  fconst5  6962  elunirn  7004  f1ocnvfvb  7030  f1prex  7034  foeqcnvco  7050  f1eqcocnv  7051  fliftfun  7059  soisores  7074  isofr  7089  isose  7090  isopo  7093  isoso  7095  f1oiso2  7099  eusvobj2  7143  oprabidw  7181  oprabid  7182  f1opw2  7394  oneqmin  7514  ordsuc  7523  ordelsuc  7529  ordsucelsuc  7531  ordunisuc2  7553  limsuc  7558  f1ovv  7653  op1steq  7727  opreuopreu  7728  funeldmdif  7741  fvn0elsuppb  7841  extmptsuppeq  7848  rntpos  7899  smoiso2  8000  seqomlem2  8081  oaord  8167  oawordex  8177  oaordex  8178  omord2  8187  om00  8195  oeord  8208  nnaord  8239  nnmord  8252  nnawordex  8257  nnaordex  8258  erexb  8308  swoord1  8314  swoord2  8315  iiner  8363  eceqoveq  8396  mapsnd  8444  ralxpmap  8454  omxpenlem  8612  domtriord  8657  mapxpen  8677  mapunen  8680  ssenen  8685  nneneq  8694  onomeneq  8702  nndomo  8706  en1eqsnbi  8743  fodomfib  8792  f1opwfi  8822  fsuppunbi  8848  elfiun  8888  suplub2  8919  ordiso2  8973  ordiso  8974  oieu  8997  brwdom2  9031  brwdom3  9040  cantnflem1  9146  cardidm  9382  carddom2  9400  pm54.43  9423  pr2ne  9425  acnen  9473  acnen2  9475  alephord  9495  alephinit  9515  dfac5  9548  infdif2  9626  fictb  9661  coflim  9677  fincssdom  9739  fin23lem25  9740  isf32lem9  9777  isf34lem4  9793  fin1a2lem11  9826  axdc3lem2  9867  ficard  9981  fpwwe2lem12  10057  fpwwe2  10059  indpi  10323  nqereq  10351  1idpr  10445  ltapr  10461  leltne  10724  ltlen  10735  ltadd2  10738  addlsub  11050  addid0  11053  ltord1  11160  mul0or  11274  ldiv  11468  ltmul1  11484  mulge0b  11504  lt2msq  11519  negfi  11583  nnsub  11675  nn0sub  11941  zrevaddcl  12021  zltp1le  12026  zdiv  12046  nneo  12060  zeo2  12063  zmax  12339  zbtwnre  12340  qrevaddcl  12364  xrlttri  12526  xrleltne  12532  xralrple  12592  xltneg  12604  xleadd1  12642  xlemul1  12677  supxrunb1  12706  supxrunb2  12707  ioo0  12757  iccid  12777  ico0  12778  ioc0  12779  icc0  12780  difreicc  12864  iccsplit  12865  zltaddlt1le  12884  0fz1  12921  uzsplit  12973  fzm1  12981  fzrevral  12986  ssfzo12bi  13126  elfznelfzob  13137  flge  13169  modid2  13260  modmuladd  13275  ssnn0fi  13347  seqf1olem1  13403  hashen  13701  hashdom  13734  hash2exprb  13823  pr2pwpr  13831  hashtpg  13837  len0nnbi  13897  ccats1pfxeqbi  14098  reuccatpfxs1  14103  repsdf2  14134  scshwfzeqfzo  14182  relexpindlem  14416  shftlem  14421  shftuz  14422  abslt  14668  absle  14669  rexico  14707  cau3lem  14708  reusq0  14816  rlim2lt  14848  rlim3  14849  o1lo1  14888  rlimdm  14902  climshft  14927  o1dif  14980  isercolllem2  15016  isercoll  15018  zsum  15069  fsum  15071  fsum00  15147  incexclem  15185  zprod  15285  fprod  15289  dvdsval2  15604  moddvds  15612  negdvdsb  15620  dvdsnegb  15621  dvdscmulr  15632  dvdsmulcr  15633  dvdssub2  15645  dvdsaddre2b  15651  fzo0dvdseq  15667  mod2eq1n2dvds  15690  ltoddhalfle  15704  sumodd  15733  bitsf1ocnv  15787  sadcaddlem  15800  bitsuz  15817  dvdsgcdb  15887  gcdzeq  15896  dvdssqlem  15904  lcmeq0  15938  lcmdvdsb  15951  lcmfeq0b  15968  lcmf  15971  lcmfdvdsb  15981  coprmgcdb  15987  cncongr  16007  isprm2lem  16019  dvdsprime  16025  dvdsprm  16041  isprm7  16046  coprm  16049  euclemma  16051  rpexp  16058  prmdiveq  16117  hashgcdlem  16119  odzdvds  16126  pythagtrip  16165  pc2dvds  16209  pcprmpw2  16212  pcprmpw  16213  vdwapun  16304  ramtcl2  16341  firest  16700  mrieqv2d  16904  isacs2  16918  isssc  17084  setciso  17345  posasymb  17556  pleval2  17569  pltval3  17571  lublecllem  17592  joinle  17618  meetle  17632  lubun  17727  clatleglb  17730  latdisd  17794  letsr  17831  intopsn  17858  gsumval2a  17889  frmdss2  18022  isgrpid2  18134  isgrpinv  18150  symg1bas  18513  oddvdsnn0  18666  oddvds  18669  odeq  18672  odeq1  18681  gexdvds  18703  pgpfi  18724  pgpssslw  18733  fislw  18744  sylow3lem2  18747  lsmelvalm  18770  lsmlub  18784  lsmss1b  18786  lsmss2b  18788  efgs1b  18856  cyggenod  18997  cyggexb  19013  dprdfeq0  19138  ablsimpgfind  19226  ringinvnz1ne0  19336  ringinvnzdiv  19337  unitmulclb  19409  dvreq1  19437  f1ghm0to0  19486  f1rhm0to0OLD  19487  f1rhm0to0ALT  19488  drngmul0or  19517  isabvd  19585  issrngd  19626  lssats2  19766  lspsneq0  19778  lsmelval2  19851  lvecvs0or  19874  lspsneq  19888  lspsneu  19889  lidl1el  19985  lidldvgen  20022  isnzr2  20030  0ringnnzr  20036  0ring01eqbi  20040  rrgeq0  20057  domneq0  20064  ply1coe1eq  20460  cply1coe0bi  20462  znunit  20704  psgndif  20740  ipeq0  20776  ocvsscon  20813  pjdm2  20849  obselocv  20866  islinds4  20973  mat1dimelbas  21074  cramer  21294  toponcomb  21531  tgss3  21588  clsval2  21652  isopn3  21668  elcls3  21685  opncldf1  21686  neiint  21706  neips  21715  opnneissb  21716  opnssneib  21717  opnnei  21722  tpnei  21723  opnneiid  21728  restcld  21774  restopnb  21777  tgcn  21854  tgcnp  21855  subbascn  21856  iscnp4  21865  cnpnei  21866  cncls2  21875  cncls  21876  cnntr  21877  lmss  21900  hausnei2  21955  lpcls  21966  ordtt1  21981  cmpsub  22002  tgcmp  22003  1stcelcls  22063  locfincmp  22128  kgencn2  22159  ptpjpre1  22173  upxp  22225  txcn  22228  txlm  22250  tgqtop  22314  kqfvima  22332  isr0  22339  regr1lem2  22342  hmeoopn  22368  hmeocld  22369  ptuncnv  22409  fbunfip  22471  fgss2  22476  ufilb  22508  ufprim  22511  trufil  22512  cfinufil  22530  ufildr  22533  elfm2  22550  elfm3  22552  rnelfm  22555  fmfnfmlem4  22559  fmco  22563  flimtopon  22572  flimopn  22577  fbflim2  22579  flimrest  22585  flffbas  22597  cnpflf  22603  fclstopon  22614  fclsnei  22621  fclsbas  22623  fclsfnflim  22629  fclscmp  22632  ufilcmp  22634  isfcf  22636  fcfnei  22637  cnpfcf  22643  alexsubb  22648  alexsubALT  22653  cldsubg  22713  tgphaus  22719  tgpt0  22721  tsmsgsum  22741  tsmsres  22746  xbln0  23018  blssexps  23030  blssex  23031  isxms2  23052  prdsbl  23095  neibl  23105  metss  23112  met2ndc  23127  metrest  23128  metcnp3  23144  tngngp3  23259  nmoeq0  23339  xrsxmet  23411  reconn  23430  iccpnfcnv  23542  fgcfil  23868  iscau4  23876  cfilres  23893  iunmbl2  24152  ismbf3d  24249  mbfaddlem  24255  i1faddlem  24288  i1fmullem  24289  ellimc3  24471  tdeglem4  24648  deg1nn0clb  24678  deg1lt0  24679  dvdsq1p  24748  plypf1  24796  0dgrb  24830  plymul0or  24864  ulmshft  24972  ulmcaulem  24976  ulmcau  24977  cosord  25110  eff1olem  25126  lognegb  25167  eflogeq  25179  logdivlt  25198  efopn  25235  cxpeq0  25255  cxpeq  25332  angpieqvd  25403  dcubic  25418  asinsinb  25469  acoscosb  25470  atantanb  25496  rlimcnp  25537  isppw  25685  isppw2  25686  vmappw  25687  isnsqf  25706  ppieq0  25747  fsumdvdsdiag  25755  dvdsppwf1o  25757  fsumfldivdiag  25761  chpeq0  25778  chteq0  25779  dchrptlem1  25834  lgsdir2lem4  25898  lgsne0  25905  lgsqr  25921  lgsdchrval  25924  gausslemma2dlem1a  25935  lgsquadlem1  25950  m1lgs  25958  2sqreultblem  26018  2sqreunnltblem  26021  iscgrglt  26294  brbtwn  26679  brcgr  26680  brbtwn2  26685  axcontlem7  26750  uhgr0vb  26851  edglnl  26922  ausgrusgrb  26944  ushgredgedg  27005  ushgredgedgloop  27007  usgr0vb  27013  usgr1v  27032  nbupgr  27120  nbumgrvtx  27122  nbuhgr2vtx1edgb  27128  edgusgrnbfin  27149  nb3grprlem1  27156  uvtxnbvtxm1  27182  cusgrfilem2  27232  uhgr0edg0rgrb  27350  cusgrm1rusgr  27358  spthonepeq  27527  usgr2pth  27539  wlkiswwlks  27648  wlkiswwlkupgr  27650  wlklnwwlkn  27656  wlklnwwlknupgr  27658  wwlksnextbi  27666  wwlksnredwwlkn0  27668  wwlksnextwrd  27669  wwlksnextprop  27685  umgrwwlks2on  27730  elwspths2on  27733  usgr2wspthons3  27737  elwwlks2  27739  elwspths2spth  27740  clwlkclwwlklem3  27773  loopclwwlkn1b  27814  clwwlknon1sn  27873  clwwlknonwwlknonb  27879  umgr3v3e3cycl  27957  eupth2lem3lem4  28004  frgr0v  28035  frgr3vlem2  28047  2clwwlk2clwwlk  28123  wlkl0  28140  grpoinvf  28303  nvmul0or  28421  nvz  28440  diporthcom  28487  ubthlem3  28643  hvmul0or  28796  his6  28870  hial0  28873  hial02  28874  orthcom  28879  normgt0  28898  ocin  29067  occon3  29068  shsel3  29086  shlub  29185  chssoc  29267  h1de2bi  29325  spansncol  29339  elspansn4  29344  spansnss2  29346  sumspansn  29420  lnopcnbd  29807  lnfncnbd  29828  riesz1  29836  elpjrn  29961  cvcon3  30055  dmdmd  30071  dmdbr3  30076  dmdbr4  30077  dmdbr5  30079  mdslmd1i  30100  atcveq0  30119  chcv1  30126  atssma  30149  atcv0eq  30150  atcv1  30151  bian1d  30218  disjeq1f  30317  br8d  30355  fpwrelmap  30463  xaddeq0  30471  eliccelico  30494  elicoelioo  30495  isarchiofld  30885  unitdivcld  31139  xrge0iifcnv  31171  lmxrge0  31190  indf1ofs  31280  eulerpartlemgh  31631  dstfrvunirn  31727  loop1cycl  32379  cusgracyclt3v  32398  cvmliftmolem2  32524  cvmlift2lem12  32556  satfvsucsuc  32607  satfdm  32611  fmlasuc  32628  satffunlem1lem2  32645  satffunlem2lem2  32648  mthmb  32823  climuzcnv  32909  br8  32987  br6  32988  br4  32989  funbreq  33008  axextbdist  33040  nodenselem8  33190  dfrdg4  33407  cgrcom  33446  cgrcoml  33452  cgrdegen  33460  btwncom  33470  brsegle  33564  brsegle2  33565  colinbtwnle  33574  btwnoutside  33581  broutsideof3  33582  outsidele  33588  lineunray  33603  lineelsb2  33604  elhf2  33631  elicc3  33660  nn0prpwlem  33665  opnbnd  33668  cldbnd  33669  opnregcld  33673  cldregopn  33674  fnessref  33700  refssfne  33701  neibastop2  33704  fnemeet2  33710  fnejoin2  33712  fgmin  33713  ontgval  33774  ordtop  33779  ordcmp  33790  nndivsub  33800  bj-19.21t  34093  bj-19.23t  34094  bj-19.42t  34097  bj-sbft  34099  bj-cbv2hv  34114  bj-equsal1t  34140  bj-19.21t0  34148  bj-ceqsalt0  34195  bj-ceqsalt1  34196  bj-xpnzexb  34268  bj-idreseq  34448  bj-finsumval0  34561  bj-fvimacnv0  34562  bj-isrvec2  34575  bj-bary1  34587  dfgcd3  34599  isbasisrelowllem1  34630  isbasisrelowllem2  34631  finxpsuclem  34672  wl-lem-exsb  34796  wl-mo3t  34806  wl-ax11-lem1  34811  matunitlindf  34884  poimirlem6  34892  poimirlem7  34893  poimirlem16  34902  poimirlem19  34905  poimirlem22  34908  poimirlem23  34909  poimirlem24  34910  cnambfre  34934  itg2addnc  34940  brabg2  34985  istotbnd3  35043  sstotbnd2  35046  sstotbnd  35047  sstotbnd3  35048  ssbnd  35060  ismtybnd  35079  reheibor  35111  grpoeqdivid  35153  grpokerinj  35165  rngosn3  35196  rngoueqz  35212  1idl  35298  0rngo  35299  divrngidl  35300  igenval2  35338  ispridlc  35342  isdmn3  35346  relcnveq3  35572  iss2  35595  elrelscnveq3  35725  funALTVeq  35927  disjeq  35961  prtlem10  35995  prter2  36011  dral1-o  36034  lshpinN  36119  lsatcveq0  36162  lsatcv0eq  36177  lsatcv1  36178  islshpcv  36183  lkr0f  36224  lkrshp4  36238  lshpkrlem1  36240  lshpset2N  36249  lfl1dim  36251  lfl1dim2N  36252  lub0N  36319  glb0N  36323  oplecon3b  36330  cmtcomN  36379  cmtbr3N  36384  cmtbr4N  36385  cvrnbtwn2  36405  cvrnbtwn3  36406  cvrcon3b  36407  cvrnbtwn4  36409  cvrcmp  36413  atcvreq0  36444  atnle  36447  atlatle  36450  cvlexchb1  36460  cvlcvr1  36469  hlrelat2  36533  exatleN  36534  cvrval3  36543  cvrval4N  36544  cvrexch  36550  atcvr0eq  36556  lnnat  36557  atcvrj0  36558  atcvrj2b  36562  atltcvr  36565  atbtwn  36576  ps-1  36607  3at  36620  islln2a  36647  llncmp  36652  islpln2a  36678  lplncmp  36692  islvol2aN  36722  4at  36743  lvolcmp  36747  pmaple  36891  lncmp  36913  paddss  36975  llnexchb2lem  36998  2polcon4bN  37048  ispsubcl2N  37077  lhpat3  37176  lautcvr  37222  ltrnid  37265  trlval2  37293  trlatn0  37302  ltrnideq  37305  trlnidatb  37307  cdlemeg49lebilem  37669  trlord  37699  cdlemg1a  37700  cdlemg1cex  37718  tendoid0  37955  dva1dim  38115  cdlemm10N  38248  diarnN  38259  cdlemn  38342  dihlspsnssN  38462  dihatexv  38468  dochkrshp  38516  dochkrshp4  38519  djhlsmcl  38544  lcfl6  38630  lcfl8  38632  lcfrvalsnN  38671  lcfrlem9  38680  mapdval2N  38760  mapdordlem2  38767  mapd1o  38778  mapd0  38795  mapdheq2biN  38860  fnsnbt  39113  frlmfzowrdb  39136  frlmsnic  39142  prjspreln0  39252  elrfi  39284  diophrw  39349  eldioph2b  39353  diophin  39362  rexrabdioph  39384  rmxycomplete  39507  coprmdvdsb  39575  jm2.19  39583  jm2.26  39592  jm2.27  39598  limsuc2  39634  dgraa0p  39742  rngunsnply  39766  fiuneneq  39790  nndomog  39890  pwelg  39912  nzss  40642  dvconstbi  40659  expgrowth  40660  bcc0  40665  axc11next  40731  pm14.24  40757  sbiota1  40759  sbcim2g  40865  sineq0ALT  41264  pwssfi  41300  mapss2  41461  fsneq  41462  fsneqrn  41467  mapssbi  41469  ssmapsn  41472  rnmptbd2lem  41513  infnsuprnmpt  41515  rnmptbdlem  41520  xralrple2  41615  infxrunb2  41629  xralrple4  41634  xralrple3  41635  xrralrecnnle  41646  xrralrecnnge  41655  reclt0  41656  supxrunb3  41665  supxrleubrnmpt  41672  xrre4  41678  unb2ltle  41682  rexabslelem  41685  suprleubrnmpt  41689  infxrunb3rnmpt  41695  uzub  41698  supminfrnmpt  41712  iccintsng  41792  sqrlearg  41822  uzinico  41829  preimaiocmnf  41830  limcresiooub  41916  limclr  41929  climeldmeq  41939  limsuppnflem  41984  limsupmnflem  41994  limsupmnfuzlem  42000  limsupre3lem  42006  limsupre3uzlem  42009  liminfreuzlem  42076  dvnmul  42221  dvmptfprodlem  42222  ismbl3  42265  ismbl4  42272  fourierdlem50  42435  fourierdlem89  42474  fourierdlem91  42476  dfsalgen2  42618  sge0repnf  42662  sge0lefi  42674  sge0resplit  42682  sge0fodjrnlem  42692  voliunsge0lem  42748  hspdifhsp  42892  isvonmbl  42914  ovnovollem3  42934  vonvolmbl  42937  pimrecltpos  42981  preimaicomnf  42984  pimrecltneg  42995  issmflem  42998  issmfle  43016  issmfgt  43027  smfaddlem1  43033  issmfge  43040  smfresal  43057  smflimmpt  43078  smfinflem  43085  smflimsuplem7  43094  smflimsupmpt  43097  sigarcol  43115  confun  43169  or2expropbi  43263  rexsb  43291  euoreqb  43302  ralbinrald  43315  rlimdmafv  43370  fafv2elrnb  43428  tz6.12c-afv2  43435  dfatbrafv2b  43438  fnbrafv2b  43441  rlimdmafv2  43451  f1oresf1o2  43484  el1fzopredsuc  43519  2ffzoeq  43522  imasetpreimafvbijlemfo  43559  iccpartiun  43588  ichnfb  43619  ich2exprop  43627  sprsymrelfolem2  43649  paireqne  43667  prprelprb  43673  reupr  43678  requad01  43780  requad1  43781  requad2  43782  dfodd6  43796  dfeven4  43797  evensumeven  43866  sbgoldbalt  43940  isomushgr  43985  isomuspgr  43993  isomgrsymb  43996  isassintop  44111  uzlidlring  44194  rngciso  44247  rngcisoALTV  44259  ringciso  44298  ringcisoALTV  44322  domnmsuppn0  44411  lindslininds  44513  snlindsntor  44520  isldepslvec2  44534  affinecomb1  44683  prelrrx2b  44695  rrx2plord2  44703  eenglngeehlnm  44720  rrx2vlinest  44722  line2xlem  44734  line2x  44735  line2y  44736  itsclc0xyqsolb  44751  itsclquadb  44757