Theorem impbid 202

Description: Deduce an equivalence from two implications. Deduction associated with impbi 198 and impbii 199. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 201. (Revised by Wolf Lammen, 3-Nov-2012.)

Hypotheses

Ref	Expression
impbid.1	|- ( ph -> ( ps -> ch ) )
impbid.2	|- ( ph -> ( ch -> ps ) )

Assertion

Ref	Expression
impbid	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		impbid.2	. . 3 |- ( ph -> ( ch -> ps ) )
3	1, 2	impbid21d 201	. 2 |- ( ph -> ( ph -> ( ps <-> ch ) ) )
4	3	pm2.43i 52	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  bicom1  211  impbid1  215  impcon4bid  217  pm5.74  259  imbi1d  331  pm5.501  356  2falsed  366  impbida  877  dedlem0b  1001  dedlema  1002  dedlemb  1003  albi  1746  alexbii  1760  equequ1  1952  equequ2  1953  elequ1  1997  elequ2  2004  19.21tOLDOLD  2074  sbequ12  2111  sb56  2150  19.21tOLD  2213  cbv2h  2269  dral1  2325  dral1ALT  2326  ax12b  2345  sbequ  2376  sbft  2379  exsb  2468  eupickb  2538  eupickbi  2539  2eu2  2554  ceqsalt  3228  rspcebdv  3314  ceqex  3333  mob2  3386  reu6  3395  sbciegft  3466  eqsbc3rOLD  3493  csbiebt  3553  sseq1  3626  ssdifsym  3863  reupick  3911  reupick2  3913  uneqdifeq  4057  uneqdifeqOLD  4058  eqoreldifOLD  4226  prnebg  4389  disjeq2  4624  disjeq1  4627  disjxiunOLD  4650  disjss3  4652  reusv2lem2  4869  reusv2lem2OLD  4870  reusv2lem3  4871  alxfr  4878  ralxfrd  4879  ralxfrdOLD  4880  ralxfrd2  4884  copsexg  4956  euotd  4975  poeq2  5039  sotric  5061  sotrieq  5062  freq2  5085  seeq1  5086  seeq2  5087  iss  5447  tz7.7  5749  ordtri1  5756  ordtri3OLD  5760  ordelinel  5825  ordelinelOLD  5826  iotaval  5862  funeq  5908  funssres  5930  f0dom0  6089  tz6.12c  6213  fnbrfvb  6236  ssimaex  6263  fvimacnv  6332  elpreima  6337  eldmrexrnb  6366  fsn  6402  fnsnb  6432  fmptsng  6434  fmptsnd  6435  tpres  6466  fconst2g  6468  fconst5  6471  elunirn  6509  f1ocnvfvb  6535  foeqcnvco  6555  f1eqcocnv  6556  fliftfun  6562  soisores  6577  isofr  6592  isose  6593  isopo  6596  isoso  6598  f1oiso2  6602  eusvobj2  6643  oprabid  6677  f1opw2  6888  oneqmin  7005  ordsuc  7014  ordelsuc  7020  ordsucelsuc  7022  ordunisuc2  7044  limsuc  7049  f1ovv  7137  op1steq  7210  fvn0elsuppb  7312  extmptsuppeq  7319  rntpos  7365  smoiso2  7466  seqomlem2  7546  oaord  7627  oawordex  7637  oaordex  7638  omord2  7647  om00  7655  oeord  7668  nnaord  7699  nnmord  7712  nnawordex  7717  nnaordex  7718  erexb  7767  swoord1  7773  swoord2  7774  iiner  7819  eceqoveq  7853  ralxpmap  7907  omxpenlem  8061  domtriord  8106  mapxpen  8126  mapunen  8129  ssenen  8134  nneneq  8143  onomeneq  8150  nndomo  8154  en1eqsnbi  8191  fodomfib  8240  f1opwfi  8270  fsuppunbi  8296  elfiun  8336  suplub2  8367  ordiso2  8420  ordiso  8421  oieu  8444  brwdom2  8478  brwdom3  8487  cantnflem1  8586  cardidm  8785  carddom2  8803  pm54.43  8826  pr2ne  8828  acnen  8876  acnen2  8878  alephord  8898  alephinit  8918  dfac5  8951  infdif2  9032  fictb  9067  coflim  9083  fincssdom  9145  fin23lem25  9146  isf32lem9  9183  isf34lem4  9199  fin1a2lem11  9232  axdc3lem2  9273  ficard  9387  fpwwe2lem12  9463  fpwwe2  9465  indpi  9729  nqereq  9757  1idpr  9851  ltapr  9867  leltne  10127  ltlen  10138  ltadd2  10141  addlsub  10447  addid0  10450  ltord1  10554  mul0or  10667  ltmul1  10873  mulge0b  10893  lt2msq  10908  negfi  10971  nnsub  11059  nn0sub  11343  zrevaddcl  11422  zltp1le  11427  zdiv  11447  nneo  11461  zeo2  11464  zmax  11785  zbtwnre  11786  qrevaddcl  11810  xrlttri  11972  xrleltne  11978  xralrple  12036  xltneg  12048  xleadd1  12085  xlemul1  12120  supxrunb1  12149  supxrunb2  12150  ioo0  12200  iccid  12220  ico0  12221  ioc0  12222  icc0  12223  difreicc  12304  iccsplit  12305  zltaddlt1le  12324  0fz1  12361  uzsplit  12412  fzm1  12420  fzrevral  12425  ssfzo12bi  12563  elfznelfzob  12574  flge  12606  modid2  12697  modmuladd  12712  ssnn0fi  12784  seqf1olem1  12840  hashen  13135  hashdom  13168  hash2exprb  13253  pr2pwpr  13261  hashtpg  13267  reuccats1  13480  ccats1swrdeqbi  13498  repsdf2  13525  scshwfzeqfzo  13572  relexpindlem  13803  shftlem  13808  shftuz  13809  abslt  14054  absle  14055  rexico  14093  cau3lem  14094  rlim2lt  14228  rlim3  14229  o1lo1  14268  rlimdm  14282  climshft  14307  o1dif  14360  isercolllem2  14396  isercoll  14398  zsum  14449  fsum  14451  fsum00  14530  incexclem  14568  zprod  14667  fprod  14671  dvdsval2  14986  moddvds  14991  negdvdsb  14998  dvdsnegb  14999  dvdscmulr  15010  dvdsmulcr  15011  dvdssub2  15023  dvdsaddre2b  15029  fzo0dvdseq  15045  mod2eq1n2dvds  15071  ltoddhalfle  15085  sumodd  15111  bitsf1ocnv  15166  sadcaddlem  15179  bitsuz  15196  dvdsgcdb  15262  gcdzeq  15271  dvdssqlem  15279  lcmeq0  15313  lcmdvdsb  15326  lcmfeq0b  15343  lcmf  15346  lcmfdvdsb  15356  coprmgcdb  15362  cncongr  15383  isprm2lem  15394  dvdsprime  15400  dvdsprm  15415  isprm7  15420  coprm  15423  euclemma  15425  rpexp  15432  prmdiveq  15491  hashgcdlem  15493  odzdvds  15500  pythagtrip  15539  pc2dvds  15583  pcprmpw2  15586  pcprmpw  15587  vdwapun  15678  ramtcl2  15715  firest  16093  mrieqv2d  16299  isacs2  16314  isssc  16480  setciso  16741  posasymb  16952  pleval2  16965  pltval3  16967  lublecllem  16988  joinle  17014  meetle  17028  lubun  17123  clatleglb  17126  latdisd  17190  letsr  17227  intopsn  17253  gsumval2a  17279  frmdss2  17400  isgrpid2  17458  isgrpinv  17472  symg1bas  17816  oddvdsnn0  17963  oddvds  17966  odeq  17969  odeq1  17977  gexdvds  17999  pgpfi  18020  pgpssslw  18029  fislw  18040  sylow3lem2  18043  lsmelvalm  18066  lsmlub  18078  lsmss1b  18080  lsmss2b  18082  efgs1b  18149  cyggenod  18286  cyggexb  18300  dprdfeq0  18421  ringinvnz1ne0  18592  ringinvnzdiv  18593  unitmulclb  18665  dvreq1  18693  f1rhm0to0  18740  f1rhm0to0ALT  18741  drngmul0or  18768  isabvd  18820  issrngd  18861  lssats2  19000  lspsneq0  19012  lsmelval2  19085  lvecvs0or  19108  lspsneq  19122  lspsneu  19123  lidl1el  19218  lidldvgen  19255  isnzr2  19263  0ringnnzr  19269  0ring01eqbi  19273  rrgeq0  19290  domneq0  19297  ply1coe1eq  19668  cply1coe0bi  19670  znunit  19912  psgndif  19948  ipeq0  19983  ocvsscon  20019  pjdm2  20055  obselocv  20072  islinds4  20174  mat1dimelbas  20277  cramer  20497  toponcomb  20733  tgss3  20790  clsval2  20854  isopn3  20870  elcls3  20887  opncldf1  20888  neiint  20908  neips  20917  opnneissb  20918  opnssneib  20919  opnnei  20924  tpnei  20925  opnneiid  20930  restcld  20976  restopnb  20979  tgcn  21056  tgcnp  21057  subbascn  21058  iscnp4  21067  cnpnei  21068  cncls2  21077  cncls  21078  cnntr  21079  lmss  21102  hausnei2  21157  lpcls  21168  ordtt1  21183  cmpsub  21203  tgcmp  21204  1stcelcls  21264  locfincmp  21329  kgencn2  21360  ptpjpre1  21374  upxp  21426  txcn  21429  txlm  21451  tgqtop  21515  kqfvima  21533  isr0  21540  regr1lem2  21543  hmeoopn  21569  hmeocld  21570  ptuncnv  21610  fbunfip  21673  fgss2  21678  ufilb  21710  ufprim  21713  trufil  21714  cfinufil  21732  ufildr  21735  elfm2  21752  elfm3  21754  rnelfm  21757  fmfnfmlem4  21761  fmco  21765  flimtopon  21774  flimopn  21779  fbflim2  21781  flimrest  21787  flffbas  21799  cnpflf  21805  fclstopon  21816  fclsnei  21823  fclsbas  21825  fclsfnflim  21831  fclscmp  21834  ufilcmp  21836  isfcf  21838  fcfnei  21839  cnpfcf  21845  alexsubb  21850  alexsubALT  21855  cldsubg  21914  tgphaus  21920  tgpt0  21922  tsmsgsum  21942  tsmsres  21947  xbln0  22219  blssexps  22231  blssex  22232  isxms2  22253  prdsbl  22296  neibl  22306  metss  22313  met2ndc  22328  metrest  22329  metcnp3  22345  tngngp3  22460  nmoeq0  22540  xrsxmet  22612  reconn  22631  iccpnfcnv  22743  fgcfil  23069  iscau4  23077  cfilres  23094  iunmbl2  23325  ismbf3d  23421  mbfaddlem  23427  i1faddlem  23460  i1fmullem  23461  ellimc3  23643  tdeglem4  23820  deg1nn0clb  23850  deg1lt0  23851  dvdsq1p  23920  plypf1  23968  0dgrb  24002  plymul0or  24036  ulmshft  24144  ulmcaulem  24148  ulmcau  24149  cosord  24278  eff1olem  24294  lognegb  24336  eflogeq  24348  logdivlt  24367  efopn  24404  cxpeq0  24424  cxpeq  24498  angpieqvd  24558  dcubic  24573  asinsinb  24624  acoscosb  24625  atantanb  24651  rlimcnp  24692  isppw  24840  isppw2  24841  vmappw  24842  isnsqf  24861  ppieq0  24902  fsumdvdsdiag  24910  dvdsppwf1o  24912  fsumfldivdiag  24916  chpeq0  24933  chteq0  24934  dchrptlem1  24989  lgsdir2lem4  25053  lgsne0  25060  lgsqr  25076  lgsdchrval  25079  gausslemma2dlem1a  25090  lgsquadlem1  25105  m1lgs  25113  iscgrglt  25409  brbtwn  25779  brcgr  25780  brbtwn2  25785  axcontlem7  25850  uhgr0vb  25967  edglnl  26038  ausgrusgrb  26060  ushgredgedg  26121  ushgredgedgloop  26123  usgr0vb  26129  usgr1v  26148  nbupgr  26240  nbumgrvtx  26242  nbuhgr2vtx1edgb  26248  edgusgrnbfin  26275  nb3grprlem1  26282  nbusgrvtxm1uvtx  26306  uvtxnbvtxm1  26307  cusgrfilem2  26352  uhgr0edg0rgrb  26470  cusgrm1rusgr  26478  spthonepeq  26648  usgr2pth  26660  wlkiswwlks  26762  wlkiswwlkupgr  26764  wlklnwwlkn  26770  wlklnwwlknupgr  26772  wwlksnextbi  26789  wwlksnredwwlkn0  26791  wwlksnextwrd  26792  wwlksnextprop  26807  wwlksnwwlksnon  26810  elwwlks2ons3  26848  umgrwwlks2on  26850  elwspths2on  26853  usgr2wspthons3  26857  elwwlks2  26861  elwspths2spth  26862  clwlkclwwlklem3  26902  clwwlksnun  26974  umgr3v3e3cycl  27044  eupth2lem3lem4  27091  frgr0v  27125  frgr3vlem2  27138  grpoinvf  27386  nvmul0or  27505  nvz  27524  diporthcom  27571  ubthlem3  27728  hvmul0or  27882  his6  27956  hial0  27959  hial02  27960  orthcom  27965  normgt0  27984  ocin  28155  occon3  28156  shsel3  28174  shlub  28273  chssoc  28355  h1de2bi  28413  spansncol  28427  elspansn4  28432  spansnss2  28434  sumspansn  28508  lnopcnbd  28895  lnfncnbd  28916  riesz1  28924  elpjrn  29049  cvcon3  29143  dmdmd  29159  dmdbr3  29164  dmdbr4  29165  dmdbr5  29167  mdslmd1i  29188  atcveq0  29207  chcv1  29214  atssma  29237  atcv0eq  29238  atcv1  29239  bian1d  29306  disjeq1f  29387  br8d  29422  fpwrelmap  29508  xaddeq0  29518  eliccelico  29539  elicoelioo  29540  isarchiofld  29817  unitdivcld  29947  xrge0iifcnv  29979  lmxrge0  29998  indf1ofs  30088  eulerpartlemgh  30440  dstfrvunirn  30536  bnj145OLD  30795  cvmliftmolem2  31264  cvmlift2lem12  31296  mthmb  31478  climuzcnv  31565  br8  31646  br6  31647  br4  31648  funbreq  31668  fprb  31669  axext4dist  31706  nodenselem8  31841  dfrdg4  32058  cgrcom  32097  cgrcoml  32103  cgrdegen  32111  btwncom  32121  brsegle  32215  brsegle2  32216  colinbtwnle  32225  btwnoutside  32232  broutsideof3  32233  outsidele  32239  lineunray  32254  lineelsb2  32255  elhf2  32282  elicc3  32311  nn0prpwlem  32317  opnbnd  32320  cldbnd  32321  opnregcld  32325  cldregopn  32326  fnessref  32352  refssfne  32353  neibastop2  32356  fnemeet2  32362  fnejoin2  32364  fgmin  32365  ontgval  32430  ordtop  32435  ordcmp  32446  nndivsub  32456  bj-ssbbi  32622  bj-ssbft  32642  bj-cbv2hv  32731  bj-dral1v  32748  bj-sbftv  32763  bj-equsal1t  32809  bj-19.21t  32817  bj-ceqsalt0  32873  bj-ceqsalt1  32874  bj-xpnzexb  32948  bj-finsumval0  33147  bj-ldiv  33155  bj-bary1  33162  dfgcd3  33170  isbasisrelowllem1  33203  isbasisrelowllem2  33204  finxpsuclem  33234  wl-lem-exsb  33348  wl-mo3t  33358  wl-ax11-lem1  33362  wl-clelv2-just  33379  matunitlindf  33407  poimirlem6  33415  poimirlem7  33416  poimirlem16  33425  poimirlem19  33428  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  cnambfre  33458  itg2addnc  33464  brabg2  33510  istotbnd3  33570  sstotbnd2  33573  sstotbnd  33574  sstotbnd3  33575  ssbnd  33587  ismtybnd  33606  reheibor  33638  grpoeqdivid  33680  grpokerinj  33692  rngosn3  33723  rngoueqz  33739  1idl  33825  0rngo  33826  divrngidl  33827  igenval2  33865  ispridlc  33869  isdmn3  33873  relcnveq3  34092  iss2  34112  prtlem10  34150  prter2  34166  dral1-o  34189  lshpinN  34276  lsatcveq0  34319  lsatcv0eq  34334  lsatcv1  34335  islshpcv  34340  lkr0f  34381  lkrshp4  34395  lshpkrlem1  34397  lshpset2N  34406  lfl1dim  34408  lfl1dim2N  34409  lub0N  34476  glb0N  34480  oplecon3b  34487  cmtcomN  34536  cmtbr3N  34541  cmtbr4N  34542  cvrnbtwn2  34562  cvrnbtwn3  34563  cvrcon3b  34564  cvrnbtwn4  34566  cvrcmp  34570  atcvreq0  34601  atnle  34604  atlatle  34607  cvlexchb1  34617  cvlcvr1  34626  hlrelat2  34689  exatleN  34690  cvrval3  34699  cvrval4N  34700  cvrexch  34706  atcvr0eq  34712  lnnat  34713  atcvrj0  34714  atcvrj2b  34718  atltcvr  34721  atbtwn  34732  ps-1  34763  3at  34776  islln2a  34803  llncmp  34808  islpln2a  34834  lplncmp  34848  islvol2aN  34878  4at  34899  lvolcmp  34903  pmaple  35047  lncmp  35069  paddss  35131  llnexchb2lem  35154  2polcon4bN  35204  ispsubcl2N  35233  lhpat3  35332  lautcvr  35378  ltrnid  35421  trlval2  35450  trlatn0  35459  ltrnideq  35462  trlnidatb  35464  cdlemeg49lebilem  35827  trlord  35857  cdlemg1a  35858  cdlemg1cex  35876  tendoid0  36113  dva1dim  36273  cdlemm10N  36407  diarnN  36418  cdlemn  36501  dihlspsnssN  36621  dihatexv  36627  dochkrshp  36675  dochkrshp4  36678  djhlsmcl  36703  lcfl6  36789  lcfl8  36791  lcfrvalsnN  36830  lcfrlem9  36839  mapdval2N  36919  mapdordlem2  36926  mapd1o  36937  mapd0  36954  mapdheq2biN  37019  elrfi  37257  diophrw  37322  eldioph2b  37326  diophin  37336  rexrabdioph  37358  rmxycomplete  37482  coprmdvdsb  37552  jm2.19  37560  jm2.26  37569  jm2.27  37575  limsuc2  37611  dgraa0p  37719  rngunsnply  37743  fiuneneq  37775  pwelg  37865  nzss  38516  dvconstbi  38533  expgrowth  38534  bcc0  38539  axc11next  38607  pm14.24  38633  sbiota1  38635  sbcim2g  38748  sineq0ALT  39173  pwssfi  39211  elixpconstg  39266  mapsnd  39388  mapss2  39397  fsneq  39398  fsneqrn  39403  mapssbi  39405  ssmapsn  39408  rnmptbd2lem  39463  infnsuprnmpt  39465  rnmptbdlem  39470  xralrple2  39570  infxrunb2  39584  xralrple4  39589  xralrple3  39590  xrralrecnnle  39602  xrralrecnnge  39613  reclt0  39614  supxrunb3  39623  supxrleubrnmpt  39632  xrre4  39638  unb2ltle  39642  rexabslelem  39645  suprleubrnmpt  39649  infxrunb3rnmpt  39655  uzub  39658  supminfrnmpt  39672  iccintsng  39749  sqrlearg  39780  uzinico  39787  preimaiocmnf  39788  limcresiooub  39874  limclr  39887  climeldmeq  39897  limsuppnflem  39942  limsupmnflem  39952  limsupmnfuzlem  39958  limsupre3lem  39964  limsupre3uzlem  39967  liminfreuzlem  40034  dvnmul  40158  dvmptfprodlem  40159  ismbl3  40203  ismbl4  40210  fourierdlem50  40373  fourierdlem89  40412  fourierdlem91  40414  dfsalgen2  40559  sge0repnf  40603  sge0lefi  40615  sge0resplit  40623  sge0fodjrnlem  40633  voliunsge0lem  40689  hspdifhsp  40830  isvonmbl  40852  ovnovollem3  40872  vonvolmbl  40875  preimagelt  40912  preimalegt  40913  pimrecltpos  40919  preimaicomnf  40922  pimrecltneg  40933  issmflem  40936  issmfle  40954  issmfgt  40965  smfaddlem1  40971  issmfge  40978  smfresal  40995  smflimmpt  41016  smfinflem  41023  smflimsuplem7  41032  smflimsupmpt  41035  sigarcol  41053  confun  41106  rexsb  41168  2reu2  41187  ralbinrald  41199  rlimdmafv  41257  el1fzopredsuc  41335  2ffzoeq  41338  iccpartiun  41370  ccats1pfxeqbi  41431  reuccatpfxs1  41434  dfodd6  41550  dfeven4  41551  evensumeven  41616  sbgoldbalt  41669  sprsymrelfolem2  41743  isassintop  41846  uzlidlring  41929  rngciso  41982  rngcisoALTV  41994  ringciso  42033  ringcisoALTV  42057  domnmsuppn0  42150  lindslininds  42253  snlindsntor  42260  isldepslvec2  42274