Theorem impbid 193

Description: Deduce an equivalence from two implications. Deduction associated with impbi 189 and impbii 190. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 192. (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 192	. 2 |- ( ph -> ( ph -> ( ps <-> ch ) ) )
4	3	pm2.43i 49	1 |- ( ph -> ( ps <-> ch ) )

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

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 188

This theorem is referenced by:  bicom1  202  impbid1  206  impcon4bid  208  pm5.74  247  imbi1d  318  pm5.501  342  2falsed  352  impbida  840  dedlem0b  961  dedlema  962  dedlemb  963  albi  1684  alexbii  1699  exbiOLD  1711  equequ1  1852  elequ1  1875  elequ2  1877  19.21t  1963  19.23tOLD  1969  sbequ12  2051  cbv2h  2077  dral1  2126  dral1ALT  2127  ax12b  2145  sbequ  2174  sbft  2177  sb56  2227  exsb  2267  eupickb  2337  eupickbi  2338  2eu2  2353  eleq2dOLD  2493  ceqsalt  3104  ceqex  3201  mob2  3250  reu6  3259  sbciegft  3330  eqsbc3r  3356  csbiebt  3415  sseq1  3485  reupick  3757  reupick2  3759  uneqdifeq  3886  eqoreldif  4041  prnebg  4182  disjeq2  4398  disjeq1  4401  disjxiun  4420  disjss3  4422  reusv2lem2  4626  reusv2lem3  4627  alxfr  4634  ralxfrd  4635  copsexg  4706  euotd  4721  poeq2  4778  sotric  4800  sotrieq  4801  freq2  4824  seeq1  4825  seeq2  4826  iss  5171  tz7.7  5468  ordtri1  5475  ordtri3  5478  ordelinel  5540  iotaval  5576  funeq  5620  funssres  5641  f0dom0  5784  tz6.12c  5900  fnbrfvb  5921  ssimaex  5946  fvimacnv  6012  elpreima  6017  eldmrexrnb  6044  fsn  6076  fnsnb  6098  fmptsng  6100  fmptsnd  6101  tpres  6132  fconst2g  6134  fconst5  6137  elunirn  6171  f1ocnvfvb  6193  foeqcnvco  6213  f1eqcocnv  6214  fliftfun  6220  soisores  6233  isofr  6248  isose  6249  isopo  6252  isoso  6254  f1oiso2  6258  eusvobj2  6298  oprabid  6332  f1opw2  6536  oneqmin  6646  ordsuc  6655  ordelsuc  6661  ordsucelsuc  6663  ordunisuc2  6685  limsuc  6690  f1ovv  6778  op1steq  6849  fvn0elsuppb  6943  extmptsuppeq  6950  rntpos  6997  smoiso2  7099  seqomlem2  7179  oaord  7259  oawordex  7269  oaordex  7270  omord2  7279  om00  7287  oeord  7300  nnaord  7331  nnmord  7344  nnawordex  7349  nnaordex  7350  erexb  7399  swoord1  7403  swoord2  7404  iiner  7446  eceqoveq  7479  ralxpmap  7532  omxpenlem  7682  domtriord  7727  mapxpen  7747  mapunen  7750  ssenen  7755  nneneq  7764  onomeneq  7771  nndomo  7775  en1eqsnbi  7811  fodomfib  7860  f1opwfi  7887  fsuppunbi  7913  elfiun  7953  suplub2  7984  ordiso2  8039  ordiso  8040  oieu  8063  brwdom2  8097  brwdom3  8106  cantnflem1  8202  cardidm  8401  carddom2  8419  pm54.43  8442  pr2ne  8444  acnen  8491  acnen2  8493  alephord  8513  alephinit  8533  dfac5  8566  infdif2  8647  fictb  8682  coflim  8698  fincssdom  8760  fin23lem25  8761  isf32lem9  8798  isf34lem4  8814  fin1a2lem11  8847  axdc3lem2  8888  ficard  8997  fpwwe2lem12  9073  fpwwe2  9075  indpi  9339  nqereq  9367  1idpr  9461  ltapr  9477  leltne  9730  ltlen  9742  ltadd2  9745  addlsub  10045  ltord1  10147  mul0or  10259  ltmul1  10462  mulge0b  10482  lt2msq  10498  negfi  10561  nnsub  10655  nn0sub  10927  zrevaddcl  10989  zltp1le  10993  zdiv  11013  nneo  11026  zeo2  11029  zmax  11268  zbtwnre  11269  qrevaddcl  11293  xrlttri  11445  xrleltne  11451  xralrple  11505  xltneg  11517  xleadd1  11548  xlemul1  11583  supxrunb1  11612  supxrunb2  11613  ioo0  11668  iccid  11688  ico0  11689  ioc0  11690  icc0  11691  difreicc  11771  iccsplit  11772  0fz1  11826  uzsplit  11873  fzm1  11881  fzrevral  11886  ssfzo12bi  12012  elfznelfzob  12021  flge  12047  modid2  12130  ssnn0fi  12203  seqf1olem1  12258  hashen  12536  hashdom  12564  hashle00  12583  hash2exprb  12636  pr2pwpr  12640  hashtpg  12645  reuccats1  12839  ccats1swrdeqbi  12856  repsdf2  12883  scshwfzeqfzo  12927  relexpindlem  13126  shftlem  13131  shftuz  13132  abslt  13377  absle  13378  rexico  13416  cau3lem  13417  rlim2lt  13560  rlim3  13561  o1lo1  13600  rlimdm  13614  climshft  13639  o1dif  13692  isercolllem2  13728  isercoll  13730  zsum  13783  fsum  13785  fsum00  13857  incexclem  13893  zprod  13990  fprod  13994  dvdsval2  14307  moddvds  14311  negdvdsb  14318  dvdsnegb  14319  dvdscmulr  14330  dvdsmulcr  14331  dvdssub2  14341  fzo0dvdseq  14357  bitsf1ocnv  14417  sadcaddlem  14430  bitsuz  14447  dvdsgcdb  14511  gcdeq  14519  dvdssqlem  14526  lcmeq0  14564  lcmdvdsb  14577  lcmfeq0b  14602  lcmf  14605  lcmfdvdsb  14615  isprm2lem  14630  dvdsprime  14636  dvdsprm  14646  coprmgcdb  14653  coprm  14656  euclemma  14664  rpexp  14671  prmdiveq  14733  odzdvds  14739  odzdvdsOLD  14745  pythagtrip  14783  pc2dvds  14827  pcprmpw2  14830  pcprmpw  14831  vdwapun  14923  ramtcl2  14965  ramtcl2OLD  14966  firest  15330  mrieqv2d  15544  isacs2  15558  isssc  15724  setciso  15985  posasymb  16197  pleval2  16210  pltval3  16212  lublecllem  16233  joinle  16259  meetle  16273  lubun  16368  clatleglb  16371  latdisd  16435  letsr  16472  intopsn  16497  gsumval2a  16521  frmdss2  16646  isgrpid2  16701  isgrpinv  16715  symg1bas  17036  oddvdsnn0  17192  oddvds  17195  odeq  17198  odeq1  17210  gexdvds  17234  pgpfi  17256  pgpssslw  17265  fislw  17276  sylow3lem2  17279  lsmelvalm  17302  lsmlub  17314  lsmss1b  17316  lsmss2b  17318  efgs1b  17385  cyggenod  17518  cyggexb  17532  dprdfeq0  17654  unitmulclb  17892  dvreq1  17920  f1rhm0to0  17967  f1rhm0to0ALT  17968  drngmul0or  17995  isabvd  18047  issrngd  18088  lssats2  18222  lspsneq0  18234  lsmelval2  18307  lvecvs0or  18330  lspsneq  18344  lspsneu  18345  lidl1el  18441  lidldvgen  18478  isnzr2  18486  0ringnnzr  18492  0ring01eqbi  18496  rrgeq0  18513  domneq0  18520  ply1coe1eq  18891  cply1coe0bi  18893  znunit  19132  psgndif  19168  ipeq0  19203  ocvsscon  19236  pjdm2  19272  obselocv  19289  islinds4  19391  mat1dimelbas  19494  cramer  19714  unitgOLD  19981  tgss3  20000  clsval2  20063  isopn3  20080  elcls3  20097  opncldf1  20098  neiint  20118  neips  20127  opnneissb  20128  opnssneib  20129  opnnei  20134  tpnei  20135  opnneiid  20140  restcld  20186  restopnb  20189  tgcn  20266  tgcnp  20267  subbascn  20268  iscnp4  20277  cnpnei  20278  cncls2  20287  cncls  20288  cnntr  20289  lmss  20312  hausnei2  20367  lpcls  20378  ordtt1  20393  cmpsub  20413  tgcmp  20414  1stcelcls  20474  locfincmp  20539  kgencn2  20570  ptpjpre1  20584  upxp  20636  txcn  20639  txlm  20661  tgqtop  20725  kqfvima  20743  isr0  20750  regr1lem2  20753  hmeoopn  20779  hmeocld  20780  ptuncnv  20820  fbunfip  20882  fgss2  20887  ufilb  20919  ufprim  20922  trufil  20923  cfinufil  20941  ufildr  20944  elfm2  20961  elfm3  20963  rnelfm  20966  fmfnfmlem4  20970  fmco  20974  flimtopon  20983  flimopn  20988  fbflim2  20990  flimrest  20996  flffbas  21008  cnpflf  21014  fclstopon  21025  fclsnei  21032  fclsbas  21034  fclsfnflim  21040  fclscmp  21043  ufilcmp  21045  isfcf  21047  fcfnei  21048  cnpfcf  21054  alexsubb  21059  alexsubALT  21064  cldsubg  21123  tgphaus  21129  tgpt0  21131  tsmsgsum  21151  tsmsres  21156  xbln0  21427  blssexps  21439  blssex  21440  isxms2  21461  prdsbl  21504  neibl  21514  metss  21521  met2ndc  21536  metrest  21537  metcnp3  21553  nmoeq0  21755  xrsxmet  21825  reconn  21844  iccpnfcnv  21970  fgcfil  22239  iscau4  22247  cfilres  22264  iunmbl2  22508  ismbf3d  22608  mbfaddlem  22614  i1faddlem  22649  i1fmullem  22650  ellimc3  22832  tdeglem4  23007  deg1nn0clb  23037  deg1lt0  23038  dvdsq1p  23109  plypf1  23164  0dgrb  23198  plymul0or  23232  ulmshft  23343  ulmcaulem  23347  ulmcau  23348  cosord  23479  eff1olem  23495  lognegb  23537  eflogeq  23549  logdivlt  23568  efopn  23601  cxpeq0  23621  cxpeq  23695  angpieqvd  23755  dcubic  23770  asinsinb  23821  acoscosb  23822  atantanb  23848  rlimcnp  23889  isppw  24039  isppw2  24040  vmappw  24041  isnsqf  24060  ppieq0  24101  fsumdvdsdiag  24111  dvdsppwf1o  24113  fsumfldivdiag  24117  chpeq0  24134  chteq0  24135  dchrptlem1  24190  lgsdir2lem4  24252  lgsne0  24259  lgsqr  24272  lgsdchrval  24273  lgsquadlem1  24280  m1lgs  24288  iscgrglt  24557  brbtwn  24927  brcgr  24928  brbtwn2  24933  axcontlem7  24998  ausisusgra  25080  nbgraf1olem5  25171  edgusgranbfin  25176  nb3graprlem1  25177  cusgrarn  25185  nbcusgra  25189  cusgrafilem2  25206  uvtxnbgra  25219  uvtxnb  25223  spthonepeq  25315  3v3e3cycl  25391  wlkiswwlk  25424  wlklniswwlkn  25427  wwlknextbi  25451  wwlknredwwlkn0  25453  wwlkextwrd  25454  wwlkextprop  25470  0clwlk  25491  clwlkisclwwlklem0  25514  el2wlkonot  25595  el2spthonot  25596  el2wlkonotot0  25598  el2wlksotot  25608  usg2wlkonot  25609  usg2spthonot  25614  usg2spthonot0  25615  nbhashuvtx  25642  uvtxhashnb  25643  0eusgraiff0rgra  25665  cusgraiffrusgra  25666  eupath2lem3  25705  frgra3vlem2  25727  frgrancvvdeqlem3  25758  numclwwlkun  25805  grpoinvf  25966  rngosn3  26152  rngoueqz  26156  rngoridfz  26161  nvmul0or  26271  nvz  26296  diporthcom  26353  ubthlem3  26512  hvmul0or  26676  his6  26750  hial0  26753  hial02  26754  orthcom  26759  normgt0  26778  ocin  26947  occon3  26948  shsel3  26966  shlub  27065  chssoc  27147  h1de2bi  27205  spansncol  27219  elspansn4  27224  spansnss2  27226  sumspansn  27300  lnopcnbd  27687  lnfncnbd  27708  riesz1  27716  elpjrn  27841  cvcon3  27935  dmdmd  27951  dmdbr3  27956  dmdbr4  27957  dmdbr5  27959  mdslmd1i  27980  atcveq0  27999  chcv1  28006  atssma  28029  atcv0eq  28030  atcv1  28031  bian1d  28098  disjeq1f  28186  br8d  28220  fpwrelmap  28324  xaddeq0  28336  eliccelico  28365  elicoelioo  28366  isarchiofld  28588  unitdivcld  28715  xrge0iifcnv  28747  lmxrge0  28766  indf1ofs  28855  eulerpartlemgh  29219  dstfrvunirn  29315  bnj145OLD  29543  cvmliftmolem2  30013  cvmlift2lem12  30045  mthmb  30227  ghomf1olem  30320  climuzcnv  30323  br8  30403  br6  30404  br4  30405  funbreq  30418  fprb  30420  axext4dist  30454  nodenselem8  30582  dfrdg4  30723  cgrcom  30762  cgrcoml  30768  cgrdegen  30776  btwncom  30786  brsegle  30880  brsegle2  30881  colinbtwnle  30890  btwnoutside  30897  broutsideof3  30898  outsidele  30904  lineunray  30919  lineelsb2  30920  elhf2  30947  elicc3  30978  nn0prpwlem  30983  opnbnd  30986  cldbnd  30987  opnregcld  30991  cldregopn  30992  fnessref  31018  refssfne  31019  neibastop2  31022  fnemeet2  31028  fnejoin2  31030  fgmin  31031  ontgval  31096  ordtop  31101  ordcmp  31112  nndivsub  31122  bj-cbv2hv  31294  bj-dral1v  31325  bj-sbftv  31344  bj-sb56  31348  bj-equsal1t  31394  bj-19.21t  31402  bj-ceqsalt0  31452  bj-ceqsalt1  31453  bj-xpnzexb  31522  bj-finsumval0  31666  bj-ldiv  31674  bj-bary1  31681  isbasisrelowllem1  31722  isbasisrelowllem2  31723  finxpsuclem  31753  wl-lem-exsb  31859  wl-mo3t  31869  wl-ax11-lem1  31879  poimirlem6  31910  poimirlem7  31911  poimirlem16  31920  poimirlem19  31923  poimirlem22  31926  poimirlem23  31927  poimirlem24  31928  cnambfre  31953  itg2addnc  31960  brabg2  32006  istotbnd3  32067  sstotbnd2  32070  sstotbnd  32071  sstotbnd3  32072  ssbnd  32084  ismtybnd  32103  reheibor  32135  grpoeqdivid  32143  grpokerinj  32147  1idl  32223  0rngo  32224  divrngidl  32225  igenval2  32263  ispridlc  32267  isdmn3  32271  prtlem10  32405  prter2  32421  dral1-o  32443  lshpinN  32524  lsatcveq0  32567  lsatcv0eq  32582  lsatcv1  32583  islshpcv  32588  lkr0f  32629  lkrshp4  32643  lshpkrlem1  32645  lshpset2N  32654  lfl1dim  32656  lfl1dim2N  32657  lub0N  32724  glb0N  32728  oplecon3b  32735  cmtcomN  32784  cmtbr3N  32789  cmtbr4N  32790  cvrnbtwn2  32810  cvrnbtwn3  32811  cvrcon3b  32812  cvrnbtwn4  32814  cvrcmp  32818  atcvreq0  32849  atnle  32852  atlatle  32855  cvlexchb1  32865  cvlcvr1  32874  hlrelat2  32937  exatleN  32938  cvrval3  32947  cvrval4N  32948  cvrexch  32954  atcvr0eq  32960  lnnat  32961  atcvrj0  32962  atcvrj2b  32966  atltcvr  32969  atbtwn  32980  ps-1  33011  3at  33024  islln2a  33051  llncmp  33056  islpln2a  33082  lplncmp  33096  islvol2aN  33126  4at  33147  lvolcmp  33151  pmaple  33295  lncmp  33317  paddss  33379  llnexchb2lem  33402  2polcon4bN  33452  ispsubcl2N  33481  lhpat3  33580  lautcvr  33626  ltrnid  33669  trlval2  33698  trlatn0  33707  ltrnideq  33710  trlnidatb  33712  cdlemeg49lebilem  34075  trlord  34105  cdlemg1a  34106  cdlemg1cex  34124  tendoid0  34361  dva1dim  34521  cdlemm10N  34655  diarnN  34666  cdlemn  34749  dihlspsnssN  34869  dihatexv  34875  dochkrshp  34923  dochkrshp4  34926  djhlsmcl  34951  lcfl6  35037  lcfl8  35039  lcfrvalsnN  35078  lcfrlem9  35087  mapdval2N  35167  mapdordlem2  35174  mapd1o  35185  mapd0  35202  mapdheq2biN  35267  elrfi  35505  diophrw  35570  eldioph2b  35574  diophin  35584  rexrabdioph  35606  rmxycomplete  35735  coprmdvdsb  35807  jm2.19  35818  jm2.26  35827  jm2.27  35833  limsuc2  35869  dgraa0p  35985  rngunsnply  36009  fiuneneq  36041  hashgcdlem  36044  pwelg  36134  isprm7  36630  nzss  36636  dvconstbi  36653  expgrowth  36654  bcc0  36659  axc11next  36727  pm14.24  36753  sbiota1  36755  sbcim2g  36869  sineq0ALT  37307  pwssfi  37354  xralrple2  37531  iccintsng  37573  limcresiooub  37663  limclr  37676  dvnmul  37758  dvmptfprodlem  37759  fourierdlem50  37960  fourierdlem89  37999  fourierdlem91  38001  sge0repnf  38136  sge0lefi  38148  sge0resplit  38156  sge0fodjrnlem  38166  sigarcol  38344  confun  38398  rexsb  38460  2reu2  38479  ralbinrald  38491  rlimdmafv  38549  el1fzopredsuc  38592  mod2eq1n2dvds  38595  iccpartiun  38618  dfodd6  38637  dfeven4  38638  gcdzeq  38663  evensumeven  38704  sgoldbalt  38752  ccats1pfxeqbi  38842  reuccatpfxs1  38845  ralxfrd2  38872  2ffzoeq  38918  uhgrauhgrbi  38991  uhgr0v  38994  ausgrusgrb  39046  usgredgedga  39090  usgr0vb  39093  usgr1v  39106  nbumgr  39178  nbusgrvtx  39180  nbuhgr2vtx1edgb  39184  edgusgrnbfin  39210  nb3grprlem1  39213  uvtxnbgrb  39232  cusgrfilem2  39273  usgra2pth  39287  uhgrauhgbi  39305  uhg0v  39308  isassintop  39465  uzlidlring  39548  rngciso  39603  rngcisoALTV  39615  ringciso  39654  ringcisoALTV  39678  domnmsuppn0  39775  lindslininds  39878  snlindsntor  39885  isldepslvec2  39899