Theorem impbid 204

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  bicom1  213  impbid1  217  impcon4bid  219  pm5.74  262  imbi1d  334  pm5.501  359  2falsed  369  impbida  788  dedlem0b  1025  dedlema  1026  dedlemb  1027  albi  1781  alexbii  1795  equequ1  1982  equequ2  1983  spsbbi  2024  elequ1  2057  elequ2  2064  sbbidOLD  2175  sbequ12  2179  sbft  2198  sb56OLD  2207  sbequvvOLD  2256  exsb  2292  cbv2  2336  cbv2h  2339  ax12b  2360  dral1  2375  dral1ALT  2376  sbequOLD  2401  exsbOLD  2422  sbbidvOLD  2437  sbequ12ALT  2508  sbftALT  2520  sbequALT  2524  eupickb  2666  eupickbi  2667  2eu2  2683  ralbi  3117  ceqsalt  3448  rspcebdv  3540  ceqex  3560  mob2  3622  reu6  3631  sbciegft  3714  2reu2  3787  csbiebt  3810  sseq1  3884  ssdifsym  4129  reupick  4176  reupick2  4178  uneqdifeq  4322  prnebg  4661  preqsnd  4664  prel12g  4669  disjeq2  4902  disjeq1  4905  disjss3  4929  reusv2lem2  5154  reusv2lem3  5155  alxfr  5162  ralxfrd  5163  ralxfrd2  5167  copsexg  5239  snopeqop  5253  euotd  5260  poeq2  5331  sotric  5354  sotrieq  5355  freq2  5379  seeq1  5380  seeq2  5381  iss  5750  tz7.7  6057  ordtri1  6064  ordelinel  6129  iotaval  6165  funeq  6210  funssres  6233  f0dom0  6394  tz6.12c  6526  fnbrfvb  6550  ssimaex  6578  fvimacnv  6650  elpreima  6655  eldmrexrnb  6685  fsn  6722  fnsnb  6753  fmptsng  6755  fmptsnd  6756  fprb  6785  tpres  6792  fconst2g  6794  fconst5  6797  elunirn  6837  f1ocnvfvb  6863  f1prex  6867  foeqcnvco  6883  f1eqcocnv  6884  fliftfun  6890  soisores  6905  isofr  6920  isose  6921  isopo  6924  isoso  6926  f1oiso2  6930  eusvobj2  6971  oprabid  7009  f1opw2  7220  oneqmin  7338  ordsuc  7347  ordelsuc  7353  ordsucelsuc  7355  ordunisuc2  7377  limsuc  7382  f1ovv  7473  op1steq  7547  opreuopreu  7548  fvn0elsuppb  7652  extmptsuppeq  7659  rntpos  7710  smoiso2  7812  seqomlem2  7892  oaord  7976  oawordex  7986  oaordex  7987  omord2  7996  om00  8004  oeord  8017  nnaord  8048  nnmord  8061  nnawordex  8066  nnaordex  8067  erexb  8116  swoord1  8122  swoord2  8123  iiner  8171  eceqoveq  8204  mapsnd  8250  ralxpmap  8260  omxpenlem  8416  domtriord  8461  mapxpen  8481  mapunen  8484  ssenen  8489  nneneq  8498  onomeneq  8505  nndomo  8509  en1eqsnbi  8546  fodomfib  8595  f1opwfi  8625  fsuppunbi  8651  elfiun  8691  suplub2  8722  ordiso2  8776  ordiso  8777  oieu  8800  brwdom2  8834  brwdom3  8843  cantnflem1  8948  cardidm  9184  carddom2  9202  pm54.43  9225  pr2ne  9227  acnen  9275  acnen2  9277  alephord  9297  alephinit  9317  dfac5  9350  infdif2  9432  fictb  9467  coflim  9483  fincssdom  9545  fin23lem25  9546  isf32lem9  9583  isf34lem4  9599  fin1a2lem11  9632  axdc3lem2  9673  ficard  9787  fpwwe2lem12  9863  fpwwe2  9865  indpi  10129  nqereq  10157  1idpr  10251  ltapr  10267  leltne  10532  ltlen  10543  ltadd2  10546  addlsub  10859  addid0  10862  ltord1  10969  mul0or  11083  ldiv  11277  ltmul1  11293  mulge0b  11313  lt2msq  11328  negfi  11392  nnsub  11487  nn0sub  11762  zrevaddcl  11843  zltp1le  11848  zdiv  11868  nneo  11882  zeo2  11885  zmax  12162  zbtwnre  12163  qrevaddcl  12188  xrlttri  12352  xrleltne  12358  xralrple  12418  xltneg  12430  xleadd1  12467  xlemul1  12502  supxrunb1  12531  supxrunb2  12532  ioo0  12582  iccid  12602  ico0  12603  ioc0  12604  icc0  12605  difreicc  12689  iccsplit  12690  zltaddlt1le  12709  0fz1  12746  uzsplit  12798  fzm1  12806  fzrevral  12811  ssfzo12bi  12950  elfznelfzob  12961  flge  12993  modid2  13084  modmuladd  13099  ssnn0fi  13171  seqf1olem1  13227  hashen  13525  hashdom  13556  hash2exprb  13643  pr2pwpr  13651  hashtpg  13657  len0nnbi  13717  reuccats1OLD  13924  ccats1pfxeqbi  13952  ccats1swrdeqbiOLD  13953  reuccatpfxs1  13959  repsdf2  14000  scshwfzeqfzo  14053  relexpindlem  14286  shftlem  14291  shftuz  14292  abslt  14538  absle  14539  rexico  14577  cau3lem  14578  reusq0  14686  rlim2lt  14718  rlim3  14719  o1lo1  14758  rlimdm  14772  climshft  14797  o1dif  14850  isercolllem2  14886  isercoll  14888  zsum  14938  fsum  14940  fsum00  15016  incexclem  15054  zprod  15154  fprod  15158  dvdsval2  15473  moddvds  15481  negdvdsb  15489  dvdsnegb  15490  dvdscmulr  15501  dvdsmulcr  15502  dvdssub2  15514  dvdsaddre2b  15520  fzo0dvdseq  15536  mod2eq1n2dvds  15559  ltoddhalfle  15573  sumodd  15602  bitsf1ocnv  15656  sadcaddlem  15669  bitsuz  15686  dvdsgcdb  15752  gcdzeq  15761  dvdssqlem  15769  lcmeq0  15803  lcmdvdsb  15816  lcmfeq0b  15833  lcmf  15836  lcmfdvdsb  15846  coprmgcdb  15852  cncongr  15872  isprm2lem  15884  dvdsprime  15890  dvdsprm  15906  isprm7  15911  coprm  15914  euclemma  15916  rpexp  15923  prmdiveq  15982  hashgcdlem  15984  odzdvds  15991  pythagtrip  16030  pc2dvds  16074  pcprmpw2  16077  pcprmpw  16078  vdwapun  16169  ramtcl2  16206  firest  16565  mrieqv2d  16771  isacs2  16785  isssc  16951  setciso  17212  posasymb  17423  pleval2  17436  pltval3  17438  lublecllem  17459  joinle  17485  meetle  17499  lubun  17594  clatleglb  17597  latdisd  17661  letsr  17698  intopsn  17724  gsumval2a  17750  frmdss2  17872  isgrpid2  17930  isgrpinv  17946  symg1bas  18288  oddvdsnn0  18437  oddvds  18440  odeq  18443  odeq1  18451  gexdvds  18473  pgpfi  18494  pgpssslw  18503  fislw  18514  sylow3lem2  18517  lsmelvalm  18540  lsmlub  18552  lsmss1b  18554  lsmss2b  18556  efgs1b  18623  cyggenod  18762  cyggexb  18776  dprdfeq0  18897  ringinvnz1ne0  19068  ringinvnzdiv  19069  unitmulclb  19141  dvreq1  19169  f1ghm0to0  19218  f1rhm0to0OLD  19219  f1rhm0to0ALT  19220  drngmul0or  19249  isabvd  19316  issrngd  19357  lssats2  19497  lspsneq0  19509  lsmelval2  19582  lvecvs0or  19605  lspsneq  19619  lspsneu  19620  lidl1el  19715  lidldvgen  19752  isnzr2  19760  0ringnnzr  19766  0ring01eqbi  19770  rrgeq0  19787  domneq0  19794  ply1coe1eq  20172  cply1coe0bi  20174  znunit  20415  psgndif  20451  ipeq0  20487  ocvsscon  20524  pjdm2  20560  obselocv  20577  islinds4  20684  mat1dimelbas  20787  cramer  21007  toponcomb  21244  tgss3  21301  clsval2  21365  isopn3  21381  elcls3  21398  opncldf1  21399  neiint  21419  neips  21428  opnneissb  21429  opnssneib  21430  opnnei  21435  tpnei  21436  opnneiid  21441  restcld  21487  restopnb  21490  tgcn  21567  tgcnp  21568  subbascn  21569  iscnp4  21578  cnpnei  21579  cncls2  21588  cncls  21589  cnntr  21590  lmss  21613  hausnei2  21668  lpcls  21679  ordtt1  21694  cmpsub  21715  tgcmp  21716  1stcelcls  21776  locfincmp  21841  kgencn2  21872  ptpjpre1  21886  upxp  21938  txcn  21941  txlm  21963  tgqtop  22027  kqfvima  22045  isr0  22052  regr1lem2  22055  hmeoopn  22081  hmeocld  22082  ptuncnv  22122  fbunfip  22184  fgss2  22189  ufilb  22221  ufprim  22224  trufil  22225  cfinufil  22243  ufildr  22246  elfm2  22263  elfm3  22265  rnelfm  22268  fmfnfmlem4  22272  fmco  22276  flimtopon  22285  flimopn  22290  fbflim2  22292  flimrest  22298  flffbas  22310  cnpflf  22316  fclstopon  22327  fclsnei  22334  fclsbas  22336  fclsfnflim  22342  fclscmp  22345  ufilcmp  22347  isfcf  22349  fcfnei  22350  cnpfcf  22356  alexsubb  22361  alexsubALT  22366  cldsubg  22425  tgphaus  22431  tgpt0  22433  tsmsgsum  22453  tsmsres  22458  xbln0  22730  blssexps  22742  blssex  22743  isxms2  22764  prdsbl  22807  neibl  22817  metss  22824  met2ndc  22839  metrest  22840  metcnp3  22856  tngngp3  22971  nmoeq0  23051  xrsxmet  23123  reconn  23142  iccpnfcnv  23254  fgcfil  23580  iscau4  23588  cfilres  23605  iunmbl2  23864  ismbf3d  23961  mbfaddlem  23967  i1faddlem  24000  i1fmullem  24001  ellimc3  24183  tdeglem4  24360  deg1nn0clb  24390  deg1lt0  24391  dvdsq1p  24460  plypf1  24508  0dgrb  24542  plymul0or  24576  ulmshft  24684  ulmcaulem  24688  ulmcau  24689  cosord  24820  eff1olem  24836  lognegb  24877  eflogeq  24889  logdivlt  24908  efopn  24945  cxpeq0  24965  cxpeq  25042  angpieqvd  25113  dcubic  25128  asinsinb  25179  acoscosb  25180  atantanb  25206  rlimcnp  25248  isppw  25396  isppw2  25397  vmappw  25398  isnsqf  25417  ppieq0  25458  fsumdvdsdiag  25466  dvdsppwf1o  25468  fsumfldivdiag  25472  chpeq0  25489  chteq0  25490  dchrptlem1  25545  lgsdir2lem4  25609  lgsne0  25616  lgsqr  25632  lgsdchrval  25635  gausslemma2dlem1a  25646  lgsquadlem1  25661  m1lgs  25669  2sqreultblem  25729  2sqreunnltblem  25732  iscgrglt  26005  brbtwn  26391  brcgr  26392  brbtwn2  26397  axcontlem7  26462  uhgr0vb  26563  edglnl  26634  ausgrusgrb  26656  ushgredgedg  26717  ushgredgedgloop  26719  usgr0vb  26725  usgr1v  26744  nbupgr  26832  nbumgrvtx  26834  nbuhgr2vtx1edgb  26840  edgusgrnbfin  26861  nb3grprlem1  26868  uvtxnbvtxm1  26894  cusgrfilem2  26944  uhgr0edg0rgrb  27062  cusgrm1rusgr  27070  spthonepeq  27244  usgr2pth  27256  wlkiswwlks  27365  wlkiswwlkupgr  27367  wlklnwwlkn  27374  wlklnwwlknupgr  27376  wwlksnextbi  27385  wwlksnextbiOLD  27386  wwlksnredwwlkn0  27389  wwlksnredwwlkn0OLD  27390  wwlksnextwrd  27391  wwlksnextwrdOLD  27396  wwlksnextprop  27418  wwlksnextpropOLD  27419  umgrwwlks2on  27466  elwspths2on  27469  usgr2wspthons3  27473  elwwlks2  27475  elwspths2spth  27476  clwlkclwwlklem3  27510  loopclwwlkn1b  27561  clwwlknon1sn  27631  clwwlknonwwlknonb  27637  umgr3v3e3cycl  27716  eupth2lem3lem4  27764  frgr0v  27798  frgr3vlem2  27811  2clwwlk2clwwlk  27890  2clwwlk2clwwlkOLD  27891  wlkl0  27923  grpoinvf  28089  nvmul0or  28207  nvz  28226  diporthcom  28273  ubthlem3  28430  hvmul0or  28584  his6  28658  hial0  28661  hial02  28662  orthcom  28667  normgt0  28686  ocin  28857  occon3  28858  shsel3  28876  shlub  28975  chssoc  29057  h1de2bi  29115  spansncol  29129  elspansn4  29134  spansnss2  29136  sumspansn  29210  lnopcnbd  29597  lnfncnbd  29618  riesz1  29626  elpjrn  29751  cvcon3  29845  dmdmd  29861  dmdbr3  29866  dmdbr4  29867  dmdbr5  29869  mdslmd1i  29890  atcveq0  29909  chcv1  29916  atssma  29939  atcv0eq  29940  atcv1  29941  bian1d  30008  disjeq1f  30093  br8d  30128  fpwrelmap  30224  xaddeq0  30232  eliccelico  30255  elicoelioo  30256  isarchiofld  30569  unitdivcld  30788  xrge0iifcnv  30820  lmxrge0  30839  indf1ofs  30929  eulerpartlemgh  31281  dstfrvunirn  31378  cvmliftmolem2  32114  cvmlift2lem12  32146  fmlasuc  32196  mthmb  32348  climuzcnv  32434  br8  32512  br6  32513  br4  32514  funbreq  32533  axext4dist  32566  nodenselem8  32716  dfrdg4  32933  cgrcom  32972  cgrcoml  32978  cgrdegen  32986  btwncom  32996  brsegle  33090  brsegle2  33091  colinbtwnle  33100  btwnoutside  33107  broutsideof3  33108  outsidele  33114  lineunray  33129  lineelsb2  33130  elhf2  33157  elicc3  33186  nn0prpwlem  33191  opnbnd  33194  cldbnd  33195  opnregcld  33199  cldregopn  33200  fnessref  33226  refssfne  33227  neibastop2  33230  fnemeet2  33236  fnejoin2  33238  fgmin  33239  ontgval  33299  ordtop  33304  ordcmp  33315  nndivsub  33325  bj-ssbft  33503  bj-cbv2hv  33578  bj-dral1v  33593  bj-equsal1t  33636  bj-19.21t  33644  bj-ceqsalt0  33693  bj-ceqsalt1  33694  bj-xpnzexb  33769  bj-finsumval0  34030  bj-bary1  34041  dfgcd3  34047  isbasisrelowllem1  34078  isbasisrelowllem2  34079  finxpsuclem  34119  wl-lem-exsb  34243  wl-mo3t  34253  wl-ax11-lem1  34258  matunitlindf  34331  poimirlem6  34339  poimirlem7  34340  poimirlem16  34349  poimirlem19  34352  poimirlem22  34355  poimirlem23  34356  poimirlem24  34357  cnambfre  34381  itg2addnc  34387  brabg2  34433  istotbnd3  34491  sstotbnd2  34494  sstotbnd  34495  sstotbnd3  34496  ssbnd  34508  ismtybnd  34527  reheibor  34559  grpoeqdivid  34601  grpokerinj  34613  rngosn3  34644  rngoueqz  34660  1idl  34746  0rngo  34747  divrngidl  34748  igenval2  34786  ispridlc  34790  isdmn3  34794  relcnveq3  35022  iss2  35047  elrelscnveq3  35176  funALTVeq  35378  disjeq  35412  prtlem10  35446  prter2  35462  dral1-o  35485  lshpinN  35570  lsatcveq0  35613  lsatcv0eq  35628  lsatcv1  35629  islshpcv  35634  lkr0f  35675  lkrshp4  35689  lshpkrlem1  35691  lshpset2N  35700  lfl1dim  35702  lfl1dim2N  35703  lub0N  35770  glb0N  35774  oplecon3b  35781  cmtcomN  35830  cmtbr3N  35835  cmtbr4N  35836  cvrnbtwn2  35856  cvrnbtwn3  35857  cvrcon3b  35858  cvrnbtwn4  35860  cvrcmp  35864  atcvreq0  35895  atnle  35898  atlatle  35901  cvlexchb1  35911  cvlcvr1  35920  hlrelat2  35984  exatleN  35985  cvrval3  35994  cvrval4N  35995  cvrexch  36001  atcvr0eq  36007  lnnat  36008  atcvrj0  36009  atcvrj2b  36013  atltcvr  36016  atbtwn  36027  ps-1  36058  3at  36071  islln2a  36098  llncmp  36103  islpln2a  36129  lplncmp  36143  islvol2aN  36173  4at  36194  lvolcmp  36198  pmaple  36342  lncmp  36364  paddss  36426  llnexchb2lem  36449  2polcon4bN  36499  ispsubcl2N  36528  lhpat3  36627  lautcvr  36673  ltrnid  36716  trlval2  36744  trlatn0  36753  ltrnideq  36756  trlnidatb  36758  cdlemeg49lebilem  37120  trlord  37150  cdlemg1a  37151  cdlemg1cex  37169  tendoid0  37406  dva1dim  37566  cdlemm10N  37699  diarnN  37710  cdlemn  37793  dihlspsnssN  37913  dihatexv  37919  dochkrshp  37967  dochkrshp4  37970  djhlsmcl  37995  lcfl6  38081  lcfl8  38083  lcfrvalsnN  38122  lcfrlem9  38131  mapdval2N  38211  mapdordlem2  38218  mapd1o  38229  mapd0  38246  mapdheq2biN  38311  fnsnbt  38565  frlmfzowrdb  38580  frlmsnic  38586  prjspreln0  38666  elrfi  38686  diophrw  38751  eldioph2b  38755  diophin  38765  rexrabdioph  38787  rmxycomplete  38910  coprmdvdsb  38978  jm2.19  38986  jm2.26  38995  jm2.27  39001  limsuc2  39037  dgraa0p  39145  rngunsnply  39169  fiuneneq  39193  pwelg  39281  ablsimpgfind  40045  nzss  40065  dvconstbi  40082  expgrowth  40083  bcc0  40088  axc11next  40155  pm14.24  40181  sbiota1  40183  sbcim2g  40291  sineq0ALT  40690  pwssfi  40726  mapss2  40894  fsneq  40895  fsneqrn  40900  mapssbi  40902  ssmapsn  40905  rnmptbd2lem  40949  infnsuprnmpt  40951  rnmptbdlem  40956  xralrple2  41052  infxrunb2  41066  xralrple4  41071  xralrple3  41072  xrralrecnnle  41084  xrralrecnnge  41093  reclt0  41094  supxrunb3  41103  supxrleubrnmpt  41111  xrre4  41117  unb2ltle  41121  rexabslelem  41124  suprleubrnmpt  41128  infxrunb3rnmpt  41134  uzub  41137  supminfrnmpt  41151  iccintsng  41231  sqrlearg  41261  uzinico  41268  preimaiocmnf  41269  limcresiooub  41355  limclr  41368  climeldmeq  41378  limsuppnflem  41423  limsupmnflem  41433  limsupmnfuzlem  41439  limsupre3lem  41445  limsupre3uzlem  41448  liminfreuzlem  41515  dvnmul  41659  dvmptfprodlem  41660  ismbl3  41703  ismbl4  41710  fourierdlem50  41873  fourierdlem89  41912  fourierdlem91  41914  dfsalgen2  42056  sge0repnf  42100  sge0lefi  42112  sge0resplit  42120  sge0fodjrnlem  42130  voliunsge0lem  42186  hspdifhsp  42330  isvonmbl  42352  ovnovollem3  42372  vonvolmbl  42375  pimrecltpos  42419  preimaicomnf  42422  pimrecltneg  42433  issmflem  42436  issmfle  42454  issmfgt  42465  smfaddlem1  42471  issmfge  42478  smfresal  42495  smflimmpt  42516  smfinflem  42523  smflimsuplem7  42532  smflimsupmpt  42535  sigarcol  42553  confun  42606  or2expropbi  42675  rexsb  42704  euoreqb  42715  ralbinrald  42728  rlimdmafv  42783  fafv2elrnb  42841  tz6.12c-afv2  42848  dfatbrafv2b  42851  fnbrafv2b  42854  rlimdmafv2  42864  f1oresf1o2  42897  el1fzopredsuc  42932  2ffzoeq  42935  iccpartiun  42967  ichnfb  42996  ich2exprop  43002  sprsymrelfolem2  43024  paireqne  43042  prprelprb  43048  reupr  43053  requad01  43155  requad1  43156  requad2  43157  dfodd6  43171  dfeven4  43172  evensumeven  43241  sbgoldbalt  43315  isomushgr  43360  isomuspgr  43368  isomgrsymb  43371  isassintop  43482  uzlidlring  43565  rngciso  43618  rngcisoALTV  43630  ringciso  43669  ringcisoALTV  43693  domnmsuppn0  43784  lindslininds  43887  snlindsntor  43894  isldepslvec2  43908  affinecomb1  44058  prelrrx2b  44070  rrx2plord2  44078  eenglngeehlnm  44095  rrx2vlinest  44097  line2xlem  44109  line2x  44110  line2y  44111  itsclc0xyqsolb  44126  itsclquadb  44132