Theorem impbid 215

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bicom1  224  impbid1  228  impcon4bid  230  pm5.74  273  imbi1d  345  pm5.501  370  2falsedOLD  381  impbida  800  dedlem0b  1040  dedlema  1041  dedlemb  1042  albi  1820  alexbii  1834  equequ1  2032  equequ2  2033  spsbbi  2078  elequ1  2118  elequ2  2126  sbequ12  2250  sbft  2267  sb56OLD  2275  cbv2w  2346  exsb  2367  dral1v  2376  cbv2  2412  cbv2h  2415  ax12b  2435  dral1  2450  dral1ALT  2451  sbequ12ALT  2557  sbftALT  2569  sbequALT  2573  eupickb  2697  eupickbi  2698  2eu2  2714  ralbi  3135  ceqsalt  3474  vtoclgft  3501  rspcebdv  3565  ceqex  3593  mob2  3654  reu6  3665  sbciegft  3756  2reu2  3827  csbiebt  3857  sseq1  3940  ss2abdv  3991  ssdifsym  4190  reupick  4239  reupick2  4241  uneqdifeq  4396  prnebg  4746  preqsnd  4749  prel12g  4754  iuneqconst  4892  disjeq2  4999  disjeq1  5002  disjss3  5029  reusv2lem2  5265  reusv2lem3  5266  alxfr  5273  ralxfrd  5274  ralxfrd2  5278  copsexgw  5346  copsexg  5347  snopeqop  5361  euotd  5368  poeq2  5442  sotric  5465  sotrieq  5466  freq2  5490  seeq1  5491  seeq2  5492  iss  5870  tz7.7  6185  ordtri1  6192  ordelinel  6257  iotaval  6298  funeq  6344  funssres  6368  f0dom0  6537  tz6.12c  6670  fnbrfvb  6693  ssimaex  6723  fvimacnv  6800  elpreima  6805  eldmrexrnb  6835  fsn  6874  fnsnb  6905  fmptsng  6907  fmptsnd  6908  fprb  6933  tpres  6940  fconst2g  6942  fconst5  6945  elunirn  6988  f1ocnvfvb  7014  f1prex  7018  foeqcnvco  7034  f1eqcocnv  7035  f1eqcocnvOLD  7036  fliftfun  7044  soisores  7059  isofr  7074  isose  7075  isopo  7078  isoso  7080  f1oiso2  7084  eusvobj2  7128  oprabidw  7166  oprabid  7167  f1opw2  7380  oneqmin  7500  ordsuc  7509  ordelsuc  7515  ordsucelsuc  7517  ordunisuc2  7539  limsuc  7544  f1ovv  7641  op1steq  7715  opreuopreu  7716  funeldmdif  7729  fvn0elsuppb  7830  extmptsuppeq  7837  rntpos  7888  smoiso2  7989  seqomlem2  8070  oaord  8156  oawordex  8166  oaordex  8167  omord2  8176  om00  8184  oeord  8197  nnaord  8228  nnmord  8241  nnawordex  8246  nnaordex  8247  erexb  8297  swoord1  8303  swoord2  8304  iiner  8352  eceqoveq  8385  mapsnd  8433  ralxpmap  8443  omxpenlem  8601  domtriord  8647  mapxpen  8667  mapunen  8670  ssenen  8675  nneneq  8684  nndomog  8692  onomeneq  8693  en1eqsnbi  8733  fodomfib  8782  f1opwfi  8812  fsuppunbi  8838  elfiun  8878  suplub2  8909  ordiso2  8963  ordiso  8964  oieu  8987  brwdom2  9021  brwdom3  9030  cantnflem1  9136  cardidm  9372  carddom2  9390  pm54.43  9414  pr2ne  9416  acnen  9464  acnen2  9466  alephord  9486  alephinit  9506  dfac5  9539  infdif2  9621  fictb  9656  coflim  9672  fincssdom  9734  fin23lem25  9735  isf32lem9  9772  isf34lem4  9788  fin1a2lem11  9821  axdc3lem2  9862  ficard  9976  fpwwe2lem12  10052  fpwwe2  10054  indpi  10318  nqereq  10346  1idpr  10440  ltapr  10456  leltne  10719  ltlen  10730  ltadd2  10733  addlsub  11045  addid0  11048  ltord1  11155  mul0or  11269  ldiv  11463  ltmul1  11479  mulge0b  11499  lt2msq  11514  negfi  11577  nnsub  11669  nn0sub  11935  zrevaddcl  12015  zltp1le  12020  zdiv  12040  nneo  12054  zeo2  12057  zmax  12333  zbtwnre  12334  qrevaddcl  12358  xrlttri  12520  xrleltne  12526  xralrple  12586  xltneg  12598  xleadd1  12636  xlemul1  12671  supxrunb1  12700  supxrunb2  12701  ioo0  12751  iccid  12771  ico0  12772  ioc0  12773  icc0  12774  difreicc  12862  iccsplit  12863  zltaddlt1le  12883  0fz1  12922  uzsplit  12974  fzm1  12982  fzrevral  12987  ssfzo12bi  13127  elfznelfzob  13138  flge  13170  modid2  13261  modmuladd  13276  ssnn0fi  13348  seqf1olem1  13405  hashen  13703  hashdom  13736  hash2exprb  13825  pr2pwpr  13833  hashtpg  13839  len0nnbi  13894  ccats1pfxeqbi  14095  reuccatpfxs1  14100  repsdf2  14131  scshwfzeqfzo  14179  relexpindlem  14414  shftlem  14419  shftuz  14420  abslt  14666  absle  14667  rexico  14705  cau3lem  14706  reusq0  14814  rlim2lt  14846  rlim3  14847  o1lo1  14886  rlimdm  14900  climshft  14925  o1dif  14978  isercolllem2  15014  isercoll  15016  zsum  15067  fsum  15069  fsum00  15145  incexclem  15183  zprod  15283  fprod  15287  dvdsval2  15602  moddvds  15610  negdvdsb  15618  dvdsnegb  15619  dvdscmulr  15630  dvdsmulcr  15631  dvdssub2  15643  dvdsaddre2b  15649  fzo0dvdseq  15665  mod2eq1n2dvds  15688  ltoddhalfle  15702  sumodd  15729  bitsf1ocnv  15783  sadcaddlem  15796  bitsuz  15813  dvdsgcdb  15883  gcdzeq  15892  dvdssqlem  15900  lcmeq0  15934  lcmdvdsb  15947  lcmfeq0b  15964  lcmf  15967  lcmfdvdsb  15977  coprmgcdb  15983  cncongr  16003  isprm2lem  16015  dvdsprime  16021  dvdsprm  16037  isprm7  16042  coprm  16045  euclemma  16047  rpexp  16054  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  pythagtrip  16161  pc2dvds  16205  pcprmpw2  16208  pcprmpw  16209  vdwapun  16300  ramtcl2  16337  firest  16698  mrieqv2d  16902  isacs2  16916  isssc  17082  setciso  17343  posasymb  17554  pleval2  17567  pltval3  17569  lublecllem  17590  joinle  17616  meetle  17630  lubun  17725  clatleglb  17728  latdisd  17792  letsr  17829  intopsn  17856  gsumval2a  17887  frmdss2  18020  isgrpid2  18132  isgrpinv  18148  symg1bas  18511  oddvdsnn0  18664  oddvds  18667  odeq  18670  odeq1  18679  gexdvds  18701  pgpfi  18722  pgpssslw  18731  fislw  18742  sylow3lem2  18745  lsmelvalm  18768  lsmlub  18782  lsmss1b  18784  lsmss2b  18786  efgs1b  18854  cyggenod  18996  cyggexb  19012  dprdfeq0  19137  ablsimpgfind  19225  ringinvnz1ne0  19338  ringinvnzdiv  19339  unitmulclb  19411  dvreq1  19439  f1ghm0to0  19488  f1rhm0to0ALT  19489  drngmul0or  19516  isabvd  19584  issrngd  19625  lssats2  19765  lspsneq0  19777  lsmelval2  19850  lvecvs0or  19873  lspsneq  19887  lspsneu  19888  lidl1el  19984  lidldvgen  20021  isnzr2  20029  0ringnnzr  20035  0ring01eqbi  20039  rrgeq0  20056  domneq0  20063  znunit  20255  psgndif  20291  ipeq0  20327  ocvsscon  20364  pjdm2  20400  obselocv  20417  islinds4  20524  ply1coe1eq  20927  cply1coe0bi  20929  mat1dimelbas  21076  cramer  21296  toponcomb  21534  tgss3  21591  clsval2  21655  isopn3  21671  elcls3  21688  opncldf1  21689  neiint  21709  neips  21718  opnneissb  21719  opnssneib  21720  opnnei  21725  tpnei  21726  opnneiid  21731  restcld  21777  restopnb  21780  tgcn  21857  tgcnp  21858  subbascn  21859  iscnp4  21868  cnpnei  21869  cncls2  21878  cncls  21879  cnntr  21880  lmss  21903  hausnei2  21958  lpcls  21969  ordtt1  21984  cmpsub  22005  tgcmp  22006  1stcelcls  22066  locfincmp  22131  kgencn2  22162  ptpjpre1  22176  upxp  22228  txcn  22231  txlm  22253  tgqtop  22317  kqfvima  22335  isr0  22342  regr1lem2  22345  hmeoopn  22371  hmeocld  22372  ptuncnv  22412  fbunfip  22474  fgss2  22479  ufilb  22511  ufprim  22514  trufil  22515  cfinufil  22533  ufildr  22536  elfm2  22553  elfm3  22555  rnelfm  22558  fmfnfmlem4  22562  fmco  22566  flimtopon  22575  flimopn  22580  fbflim2  22582  flimrest  22588  flffbas  22600  cnpflf  22606  fclstopon  22617  fclsnei  22624  fclsbas  22626  fclsfnflim  22632  fclscmp  22635  ufilcmp  22637  isfcf  22639  fcfnei  22640  cnpfcf  22646  alexsubb  22651  alexsubALT  22656  cldsubg  22716  tgphaus  22722  tgpt0  22724  tsmsgsum  22744  tsmsres  22749  xbln0  23021  blssexps  23033  blssex  23034  isxms2  23055  prdsbl  23098  neibl  23108  metss  23115  met2ndc  23130  metrest  23131  metcnp3  23147  tngngp3  23262  nmoeq0  23342  xrsxmet  23414  reconn  23433  iccpnfcnv  23549  fgcfil  23875  iscau4  23883  cfilres  23900  iunmbl2  24161  ismbf3d  24258  mbfaddlem  24264  i1faddlem  24297  i1fmullem  24298  ellimc3  24482  tdeglem4  24661  deg1nn0clb  24691  deg1lt0  24692  dvdsq1p  24761  plypf1  24809  0dgrb  24843  plymul0or  24877  ulmshft  24985  ulmcaulem  24989  ulmcau  24990  cosord  25123  eff1olem  25140  lognegb  25181  eflogeq  25193  logdivlt  25212  efopn  25249  cxpeq0  25269  cxpeq  25346  angpieqvd  25417  dcubic  25432  asinsinb  25483  acoscosb  25484  atantanb  25510  rlimcnp  25551  isppw  25699  isppw2  25700  vmappw  25701  isnsqf  25720  ppieq0  25761  fsumdvdsdiag  25769  dvdsppwf1o  25771  fsumfldivdiag  25775  chpeq0  25792  chteq0  25793  dchrptlem1  25848  lgsdir2lem4  25912  lgsne0  25919  lgsqr  25935  lgsdchrval  25938  gausslemma2dlem1a  25949  lgsquadlem1  25964  m1lgs  25972  2sqreultblem  26032  2sqreunnltblem  26035  iscgrglt  26308  brbtwn  26693  brcgr  26694  brbtwn2  26699  axcontlem7  26764  uhgr0vb  26865  edglnl  26936  ausgrusgrb  26958  ushgredgedg  27019  ushgredgedgloop  27021  usgr0vb  27027  usgr1v  27046  nbupgr  27134  nbumgrvtx  27136  nbuhgr2vtx1edgb  27142  edgusgrnbfin  27163  nb3grprlem1  27170  uvtxnbvtxm1  27196  cusgrfilem2  27246  uhgr0edg0rgrb  27364  cusgrm1rusgr  27372  spthonepeq  27541  usgr2pth  27553  wlkiswwlks  27662  wlkiswwlkupgr  27664  wlklnwwlkn  27670  wlklnwwlknupgr  27672  wwlksnextbi  27680  wwlksnredwwlkn0  27682  wwlksnextwrd  27683  wwlksnextprop  27698  umgrwwlks2on  27743  elwspths2on  27746  usgr2wspthons3  27750  elwwlks2  27752  elwspths2spth  27753  clwlkclwwlklem3  27786  loopclwwlkn1b  27827  clwwlknon1sn  27885  clwwlknonwwlknonb  27891  umgr3v3e3cycl  27969  eupth2lem3lem4  28016  frgr0v  28047  frgr3vlem2  28059  2clwwlk2clwwlk  28135  wlkl0  28152  grpoinvf  28315  nvmul0or  28433  nvz  28452  diporthcom  28499  ubthlem3  28655  hvmul0or  28808  his6  28882  hial0  28885  hial02  28886  orthcom  28891  normgt0  28910  ocin  29079  occon3  29080  shsel3  29098  shlub  29197  chssoc  29279  h1de2bi  29337  spansncol  29351  elspansn4  29356  spansnss2  29358  sumspansn  29432  lnopcnbd  29819  lnfncnbd  29840  riesz1  29848  elpjrn  29973  cvcon3  30067  dmdmd  30083  dmdbr3  30088  dmdbr4  30089  dmdbr5  30091  mdslmd1i  30112  atcveq0  30131  chcv1  30138  atssma  30161  atcv0eq  30162  atcv1  30163  bian1d  30230  disjeq1f  30336  br8d  30374  fpwrelmap  30495  xaddeq0  30503  eliccelico  30526  elicoelioo  30527  isarchiofld  30941  unitdivcld  31254  xrge0iifcnv  31286  lmxrge0  31305  indf1ofs  31395  eulerpartlemgh  31746  dstfrvunirn  31842  fnrelpredd  32472  loop1cycl  32497  cusgracyclt3v  32516  cvmliftmolem2  32642  cvmlift2lem12  32674  satfvsucsuc  32725  satfdm  32729  fmlasuc  32746  satffunlem1lem2  32763  satffunlem2lem2  32766  mthmb  32941  climuzcnv  33027  br8  33105  br6  33106  br4  33107  funbreq  33126  axextbdist  33158  nodenselem8  33308  dfrdg4  33525  cgrcom  33564  cgrcoml  33570  cgrdegen  33578  btwncom  33588  brsegle  33682  brsegle2  33683  colinbtwnle  33692  btwnoutside  33699  broutsideof3  33700  outsidele  33706  lineunray  33721  lineelsb2  33722  elhf2  33749  elicc3  33778  nn0prpwlem  33783  opnbnd  33786  cldbnd  33787  opnregcld  33791  cldregopn  33792  fnessref  33818  refssfne  33819  neibastop2  33822  fnemeet2  33828  fnejoin2  33830  fgmin  33831  ontgval  33892  ordtop  33897  ordcmp  33908  nndivsub  33918  bj-19.21t  34213  bj-19.23t  34214  bj-19.42t  34217  bj-sbft  34219  bj-cbv2hv  34234  bj-equsal1t  34260  bj-19.21t0  34268  bj-ceqsalt0  34324  bj-ceqsalt1  34325  bj-xpnzexb  34397  bj-idreseq  34577  bj-imdiridlem  34600  bj-finsumval0  34700  bj-fvimacnv0  34701  bj-isrvec2  34714  bj-bary1  34726  dfgcd3  34738  isbasisrelowllem1  34772  isbasisrelowllem2  34773  finxpsuclem  34814  wl-lem-exsb  34967  wl-mo3t  34977  wl-ax11-lem1  34982  matunitlindf  35055  poimirlem6  35063  poimirlem7  35064  poimirlem16  35073  poimirlem19  35076  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  cnambfre  35105  itg2addnc  35111  brabg2  35154  istotbnd3  35209  sstotbnd2  35212  sstotbnd  35213  sstotbnd3  35214  ssbnd  35226  ismtybnd  35245  reheibor  35277  grpoeqdivid  35319  grpokerinj  35331  rngosn3  35362  rngoueqz  35378  1idl  35464  0rngo  35465  divrngidl  35466  igenval2  35504  ispridlc  35508  isdmn3  35512  relcnveq3  35738  iss2  35761  elrelscnveq3  35891  funALTVeq  36093  disjeq  36127  prtlem10  36161  prter2  36177  dral1-o  36200  lshpinN  36285  lsatcveq0  36328  lsatcv0eq  36343  lsatcv1  36344  islshpcv  36349  lkr0f  36390  lkrshp4  36404  lshpkrlem1  36406  lshpset2N  36415  lfl1dim  36417  lfl1dim2N  36418  lub0N  36485  glb0N  36489  oplecon3b  36496  cmtcomN  36545  cmtbr3N  36550  cmtbr4N  36551  cvrnbtwn2  36571  cvrnbtwn3  36572  cvrcon3b  36573  cvrnbtwn4  36575  cvrcmp  36579  atcvreq0  36610  atnle  36613  atlatle  36616  cvlexchb1  36626  cvlcvr1  36635  hlrelat2  36699  exatleN  36700  cvrval3  36709  cvrval4N  36710  cvrexch  36716  atcvr0eq  36722  lnnat  36723  atcvrj0  36724  atcvrj2b  36728  atltcvr  36731  atbtwn  36742  ps-1  36773  3at  36786  islln2a  36813  llncmp  36818  islpln2a  36844  lplncmp  36858  islvol2aN  36888  4at  36909  lvolcmp  36913  pmaple  37057  lncmp  37079  paddss  37141  llnexchb2lem  37164  2polcon4bN  37214  ispsubcl2N  37243  lhpat3  37342  lautcvr  37388  ltrnid  37431  trlval2  37459  trlatn0  37468  ltrnideq  37471  trlnidatb  37473  cdlemeg49lebilem  37835  trlord  37865  cdlemg1a  37866  cdlemg1cex  37884  tendoid0  38121  dva1dim  38281  cdlemm10N  38414  diarnN  38425  cdlemn  38508  dihlspsnssN  38628  dihatexv  38634  dochkrshp  38682  dochkrshp4  38685  djhlsmcl  38710  lcfl6  38796  lcfl8  38798  lcfrvalsnN  38837  lcfrlem9  38846  mapdval2N  38926  mapdordlem2  38933  mapd1o  38944  mapd0  38961  mapdheq2biN  39026  nnproddivdvdsd  39289  fnsnbt  39414  frlmfzowrdb  39438  frlmsnic  39453  mulgt0b2d  39585  prjspreln0  39603  elrfi  39635  diophrw  39700  eldioph2b  39704  diophin  39713  rexrabdioph  39735  rmxycomplete  39858  coprmdvdsb  39926  jm2.19  39934  jm2.26  39943  jm2.27  39949  limsuc2  39985  dgraa0p  40093  rngunsnply  40117  fiuneneq  40141  pwelg  40259  nzss  41021  dvconstbi  41038  expgrowth  41039  bcc0  41044  axc11next  41110  pm14.24  41136  sbiota1  41138  sbcim2g  41244  sineq0ALT  41643  pwssfi  41679  mapss2  41834  fsneq  41835  fsneqrn  41840  mapssbi  41842  ssmapsn  41845  rnmptbd2lem  41886  infnsuprnmpt  41888  rnmptbdlem  41893  xralrple2  41986  infxrunb2  42000  xralrple4  42005  xralrple3  42006  xrralrecnnle  42017  xrralrecnnge  42026  reclt0  42027  supxrunb3  42036  supxrleubrnmpt  42043  xrre4  42048  unb2ltle  42052  rexabslelem  42055  suprleubrnmpt  42059  infxrunb3rnmpt  42065  uzub  42068  supminfrnmpt  42082  iccintsng  42160  sqrlearg  42190  uzinico  42197  preimaiocmnf  42198  limcresiooub  42284  limclr  42297  climeldmeq  42307  limsuppnflem  42352  limsupmnflem  42362  limsupmnfuzlem  42368  limsupre3lem  42374  limsupre3uzlem  42377  liminfreuzlem  42444  dvnmul  42585  dvmptfprodlem  42586  ismbl3  42628  ismbl4  42635  fourierdlem50  42798  fourierdlem89  42837  fourierdlem91  42839  dfsalgen2  42981  sge0repnf  43025  sge0lefi  43037  sge0resplit  43045  sge0fodjrnlem  43055  voliunsge0lem  43111  hspdifhsp  43255  isvonmbl  43277  ovnovollem3  43297  vonvolmbl  43300  pimrecltpos  43344  preimaicomnf  43347  pimrecltneg  43358  issmflem  43361  issmfle  43379  issmfgt  43390  smfaddlem1  43396  issmfge  43403  smfresal  43420  smflimmpt  43441  smfinflem  43448  smflimsuplem7  43457  smflimsupmpt  43460  sigarcol  43478  confun  43532  or2expropbi  43626  rexsb  43654  euoreqb  43665  ralbinrald  43678  rlimdmafv  43733  fafv2elrnb  43791  tz6.12c-afv2  43798  dfatbrafv2b  43801  fnbrafv2b  43804  rlimdmafv2  43814  f1oresf1o2  43847  el1fzopredsuc  43882  2ffzoeq  43885  imasetpreimafvbijlemfo  43922  iccpartiun  43951  ichnfb  43982  ich2exprop  43988  sprsymrelfolem2  44010  paireqne  44028  prprelprb  44034  reupr  44039  requad01  44139  requad1  44140  requad2  44141  dfodd6  44155  dfeven4  44156  evensumeven  44225  sbgoldbalt  44299  isomushgr  44344  isomuspgr  44352  isomgrsymb  44355  isassintop  44470  uzlidlring  44553  rngciso  44606  rngcisoALTV  44618  ringciso  44657  ringcisoALTV  44681  domnmsuppn0  44771  lindslininds  44873  snlindsntor  44880  isldepslvec2  44894  affinecomb1  45116  prelrrx2b  45128  rrx2plord2  45136  eenglngeehlnm  45153  rrx2vlinest  45155  line2xlem  45167  line2x  45168  line2y  45169  itsclc0xyqsolb  45184  itsclquadb  45190