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  1686  exbi  1713  equequ1  1850  elequ1  1873  elequ2  1875  19.21t  1961  19.23tOLD  1967  sbequ12  2049  cbv2h  2075  dral1  2123  dral1ALT  2124  ax12b  2142  sbequ  2171  sbft  2174  sb56  2224  exsb  2264  eupickb  2338  eupickbi  2339  2eu2  2356  eleq2d  2499  ceqsalt  3110  ceqex  3208  mob2  3257  reu6  3266  sbciegft  3336  eqsbc3r  3362  csbiebt  3421  sseq1  3491  reupick  3763  reupick2  3765  uneqdifeq  3890  eqoreldif  4044  prnebg  4185  disjeq2  4401  disjeq1  4404  disjxiun  4423  disjss3  4425  reusv2lem2  4627  reusv2lem3  4628  alxfr  4635  ralxfrd  4636  copsexg  4707  euotd  4722  poeq2  4779  sotric  4801  sotrieq  4802  freq2  4825  seeq1  4826  seeq2  4827  iss  5172  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  6994  smoiso2  7096  seqomlem2  7176  oaord  7256  oawordex  7266  oaordex  7267  omord2  7276  om00  7284  oeord  7297  nnaord  7328  nnmord  7341  nnawordex  7346  nnaordex  7347  erexb  7396  swoord1  7400  swoord2  7401  iiner  7443  eceqoveq  7476  ralxpmap  7529  omxpenlem  7679  domtriord  7724  mapxpen  7744  mapunen  7747  ssenen  7752  nneneq  7761  onomeneq  7768  nndomo  7772  en1eqsnbi  7808  fodomfib  7857  f1opwfi  7884  fsuppunbi  7910  elfiun  7950  suplub2  7981  ordiso2  8030  ordiso  8031  oieu  8054  brwdom2  8088  brwdom3  8097  cantnflem1  8193  cardidm  8392  carddom2  8410  pm54.43  8433  pr2ne  8435  acnen  8482  acnen2  8484  alephord  8504  alephinit  8524  dfac5  8557  infdif2  8638  fictb  8673  coflim  8689  fincssdom  8751  fin23lem25  8752  isf32lem9  8789  isf34lem4  8805  fin1a2lem11  8838  axdc3lem2  8879  ficard  8988  fpwwe2lem12  9065  fpwwe2  9067  indpi  9331  nqereq  9359  1idpr  9453  ltapr  9469  leltne  9722  ltlen  9734  ltadd2  9737  addlsub  10037  ltord1  10139  mul0or  10251  ltmul1  10454  mulge0b  10474  lt2msq  10490  negfi  10554  nnsub  10648  nn0sub  10920  zrevaddcl  10982  zltp1le  10986  zdiv  11006  nneo  11019  zeo2  11022  zmax  11261  zbtwnre  11262  qrevaddcl  11286  xrlttri  11438  xrleltne  11444  xralrple  11498  xltneg  11510  xleadd1  11541  xlemul1  11576  supxrunb1  11605  supxrunb2  11606  ioo0  11661  iccid  11681  ico0  11682  ioc0  11683  icc0  11684  difreicc  11762  iccsplit  11763  0fz1  11817  uzsplit  11864  fzm1  11872  fzrevral  11877  ssfzo12bi  12003  elfznelfzob  12012  flge  12038  modid2  12121  ssnn0fi  12194  seqf1olem1  12249  hashen  12527  hashdom  12555  hashle00  12574  hash2prb  12626  pr2pwpr  12629  hashtpg  12632  reuccats1  12822  ccats1swrdeqbi  12839  repsdf2  12866  scshwfzeqfzo  12910  relexpindlem  13105  shftlem  13110  shftuz  13111  abslt  13356  absle  13357  rexico  13395  cau3lem  13396  rlim2lt  13539  rlim3  13540  o1lo1  13579  rlimdm  13593  climshft  13618  o1dif  13671  isercolllem2  13707  isercoll  13709  zsum  13762  fsum  13764  fsum00  13836  incexclem  13872  zprod  13969  fprod  13973  dvdsval2  14286  moddvds  14290  negdvdsb  14297  dvdsnegb  14298  dvdscmulr  14309  dvdsmulcr  14310  dvdssub2  14320  fzo0dvdseq  14336  bitsf1ocnv  14392  sadcaddlem  14405  bitsuz  14422  dvdsgcdb  14483  gcdeq  14491  dvdssqlem  14498  lcmeq0  14536  lcmdvdsb  14549  lcmfeq0b  14574  lcmf  14577  lcmfdvdsb  14587  isprm2lem  14602  dvdsprime  14608  dvdsprm  14618  coprmgcdb  14625  coprm  14628  euclemma  14636  rpexp  14643  prmdiveq  14703  odzdvds  14709  pythagtrip  14747  pc2dvds  14791  pcprmpw2  14794  pcprmpw  14795  vdwapun  14887  ramtcl2  14929  ramtcl2OLD  14930  firest  15290  mrieqv2d  15496  isacs2  15510  isssc  15676  setciso  15937  posasymb  16149  pleval2  16162  pltval3  16164  lublecllem  16185  joinle  16211  meetle  16225  lubun  16320  clatleglb  16323  latdisd  16387  letsr  16424  intopsn  16449  gsumval2a  16473  frmdss2  16598  isgrpid2  16653  isgrpinv  16667  symg1bas  16988  oddvdsnn0  17135  oddvds  17138  odeq  17141  odeq1  17149  gexdvds  17171  pgpfi  17192  pgpssslw  17201  fislw  17212  sylow3lem2  17215  lsmelvalm  17238  lsmlub  17250  lsmss1b  17252  lsmss2b  17254  efgs1b  17321  cyggenod  17454  cyggexb  17468  dprdfeq0  17590  unitmulclb  17828  dvreq1  17856  f1rhm0to0  17903  f1rhm0to0ALT  17904  drngmul0or  17931  isabvd  17983  issrngd  18024  lssats2  18158  lspsneq0  18170  lsmelval2  18243  lvecvs0or  18266  lspsneq  18280  lspsneu  18281  lidl1el  18377  lidldvgen  18414  isnzr2  18422  0ringnnzr  18428  0ring01eqbi  18432  rrgeq0  18449  domneq0  18456  ply1coe1eq  18827  cply1coe0bi  18829  znunit  19065  psgndif  19101  ipeq0  19136  ocvsscon  19169  pjdm2  19205  obselocv  19222  islinds4  19324  mat1dimelbas  19427  cramer  19647  unitgOLD  19914  tgss3  19933  clsval2  19996  isopn3  20013  elcls3  20030  opncldf1  20031  neiint  20051  neips  20060  opnneissb  20061  opnssneib  20062  opnnei  20067  tpnei  20068  opnneiid  20073  restcld  20119  restopnb  20122  tgcn  20199  tgcnp  20200  subbascn  20201  iscnp4  20210  cnpnei  20211  cncls2  20220  cncls  20221  cnntr  20222  lmss  20245  hausnei2  20300  lpcls  20311  ordtt1  20326  cmpsub  20346  tgcmp  20347  1stcelcls  20407  locfincmp  20472  kgencn2  20503  ptpjpre1  20517  upxp  20569  txcn  20572  txlm  20594  tgqtop  20658  kqfvima  20676  isr0  20683  regr1lem2  20686  hmeoopn  20712  hmeocld  20713  ptuncnv  20753  fbunfip  20815  fgss2  20820  ufilb  20852  ufprim  20855  trufil  20856  cfinufil  20874  ufildr  20877  elfm2  20894  elfm3  20896  rnelfm  20899  fmfnfmlem4  20903  fmco  20907  flimtopon  20916  flimopn  20921  fbflim2  20923  flimrest  20929  flffbas  20941  cnpflf  20947  fclstopon  20958  fclsnei  20965  fclsbas  20967  fclsfnflim  20973  fclscmp  20976  ufilcmp  20978  isfcf  20980  fcfnei  20981  cnpfcf  20987  alexsubb  20992  alexsubALT  20997  cldsubg  21056  tgphaus  21062  tgpt0  21064  tsmsgsum  21084  tsmsres  21089  xbln0  21360  blssexps  21372  blssex  21373  isxms2  21394  prdsbl  21437  neibl  21447  metss  21454  met2ndc  21469  metrest  21470  metcnp3  21486  nmoeq0  21668  xrsxmet  21738  reconn  21757  iccpnfcnv  21868  fgcfil  22134  iscau4  22142  cfilres  22159  iunmbl2  22387  ismbf3d  22487  mbfaddlem  22493  i1faddlem  22528  i1fmullem  22529  ellimc3  22711  tdeglem4  22886  deg1nn0clb  22916  deg1lt0  22917  dvdsq1p  22986  plypf1  23034  0dgrb  23068  plymul0or  23102  ulmshft  23210  ulmcaulem  23214  ulmcau  23215  cosord  23346  eff1olem  23362  lognegb  23404  eflogeq  23416  logdivlt  23435  efopn  23468  cxpeq0  23488  cxpeq  23562  angpieqvd  23622  dcubic  23637  asinsinb  23688  acoscosb  23689  atantanb  23715  rlimcnp  23756  isppw  23904  isppw2  23905  vmappw  23906  isnsqf  23925  ppieq0  23966  fsumdvdsdiag  23976  dvdsppwf1o  23978  fsumfldivdiag  23982  chpeq0  23999  chteq0  24000  dchrptlem1  24055  lgsdir2lem4  24117  lgsne0  24124  lgsqr  24137  lgsdchrval  24138  lgsquadlem1  24145  m1lgs  24153  brbtwn  24775  brcgr  24776  brbtwn2  24781  axcontlem7  24846  ausisusgra  24928  nbgraf1olem5  25018  edgusgranbfin  25023  nb3graprlem1  25024  cusgrarn  25032  nbcusgra  25036  cusgrafilem2  25053  uvtxnbgra  25066  uvtxnb  25070  spthonepeq  25162  3v3e3cycl  25238  wlkiswwlk  25271  wlklniswwlkn  25274  wwlknextbi  25298  wwlknredwwlkn0  25300  wwlkextwrd  25301  wwlkextprop  25317  0clwlk  25338  clwlkisclwwlklem0  25361  el2wlkonot  25442  el2spthonot  25443  el2wlkonotot0  25445  el2wlksotot  25455  usg2wlkonot  25456  usg2spthonot  25461  usg2spthonot0  25462  nbhashuvtx  25489  uvtxhashnb  25490  0eusgraiff0rgra  25512  cusgraiffrusgra  25513  eupath2lem3  25552  frgra3vlem2  25574  frgrancvvdeqlem3  25605  numclwwlkun  25652  grpoinvf  25813  rngosn3  25999  rngoueqz  26003  rngoridfz  26008  nvmul0or  26118  nvz  26143  diporthcom  26200  ubthlem3  26359  hvmul0or  26513  his6  26587  hial0  26590  hial02  26591  orthcom  26596  normgt0  26615  ocin  26784  occon3  26785  shsel3  26803  shlub  26902  chssoc  26984  h1de2bi  27042  spansncol  27056  elspansn4  27061  spansnss2  27063  sumspansn  27137  lnopcnbd  27524  lnfncnbd  27545  riesz1  27553  elpjrn  27678  cvcon3  27772  dmdmd  27788  dmdbr3  27793  dmdbr4  27794  dmdbr5  27796  mdslmd1i  27817  atcveq0  27836  chcv1  27843  atssma  27866  atcv0eq  27867  atcv1  27868  bian1d  27935  disjeq1f  28023  br8d  28057  fpwrelmap  28161  xaddeq0  28173  eliccelico  28195  elicoelioo  28196  isarchiofld  28419  unitdivcld  28546  xrge0iifcnv  28578  lmxrge0  28597  indf1ofs  28686  eulerpartlemgh  29037  dstfrvunirn  29133  bnj145OLD  29323  cvmliftmolem2  29793  cvmlift2lem12  29825  mthmb  30007  ghomf1olem  30100  climuzcnv  30103  br8  30183  br6  30184  br4  30185  funbreq  30198  fprb  30200  axext4dist  30234  nodenselem8  30362  dfrdg4  30503  cgrcom  30542  cgrcoml  30548  cgrdegen  30556  btwncom  30566  brsegle  30660  brsegle2  30661  colinbtwnle  30670  btwnoutside  30677  broutsideof3  30678  outsidele  30684  lineunray  30699  lineelsb2  30700  elhf2  30727  elicc3  30758  nn0prpwlem  30763  opnbnd  30766  cldbnd  30767  opnregcld  30771  cldregopn  30772  fnessref  30798  refssfne  30799  neibastop2  30802  fnemeet2  30808  fnejoin2  30810  fgmin  30811  ontgval  30876  ordtop  30881  ordcmp  30892  nndivsub  30902  bj-cbv2hv  31074  bj-dral1v  31106  bj-sbftv  31125  bj-sb56  31129  bj-equsal1t  31175  bj-19.21t  31183  bj-ceqsalt0  31233  bj-ceqsalt1  31234  bj-xpnzexb  31303  bj-finsumval0  31447  bj-ldiv  31455  bj-bary1  31462  isbasisrelowllem1  31492  isbasisrelowllem2  31493  wl-lem-exsb  31602  wl-mo3t  31608  wl-ax11-lem1  31618  poimirlem6  31649  poimirlem7  31650  poimirlem16  31659  poimirlem19  31662  poimirlem22  31665  poimirlem23  31666  poimirlem24  31667  cnambfre  31692  itg2addnc  31699  brabg2  31745  istotbnd3  31806  sstotbnd2  31809  sstotbnd  31810  sstotbnd3  31811  ssbnd  31823  ismtybnd  31842  reheibor  31874  grpoeqdivid  31882  grpokerinj  31886  1idl  31962  0rngo  31963  divrngidl  31964  igenval2  32002  ispridlc  32006  isdmn3  32010  prtlem10  32144  prter2  32160  dral1-o  32182  lshpinN  32263  lsatcveq0  32306  lsatcv0eq  32321  lsatcv1  32322  islshpcv  32327  lkr0f  32368  lkrshp4  32382  lshpkrlem1  32384  lshpset2N  32393  lfl1dim  32395  lfl1dim2N  32396  lub0N  32463  glb0N  32467  oplecon3b  32474  cmtcomN  32523  cmtbr3N  32528  cmtbr4N  32529  cvrnbtwn2  32549  cvrnbtwn3  32550  cvrcon3b  32551  cvrnbtwn4  32553  cvrcmp  32557  atcvreq0  32588  atnle  32591  atlatle  32594  cvlexchb1  32604  cvlcvr1  32613  hlrelat2  32676  exatleN  32677  cvrval3  32686  cvrval4N  32687  cvrexch  32693  atcvr0eq  32699  lnnat  32700  atcvrj0  32701  atcvrj2b  32705  atltcvr  32708  atbtwn  32719  ps-1  32750  3at  32763  islln2a  32790  llncmp  32795  islpln2a  32821  lplncmp  32835  islvol2aN  32865  4at  32886  lvolcmp  32890  pmaple  33034  lncmp  33056  paddss  33118  llnexchb2lem  33141  2polcon4bN  33191  ispsubcl2N  33220  lhpat3  33319  lautcvr  33365  ltrnid  33408  trlval2  33437  trlatn0  33446  ltrnideq  33449  trlnidatb  33451  cdlemeg49lebilem  33814  trlord  33844  cdlemg1a  33845  cdlemg1cex  33863  tendoid0  34100  dva1dim  34260  cdlemm10N  34394  diarnN  34405  cdlemn  34488  dihlspsnssN  34608  dihatexv  34614  dochkrshp  34662  dochkrshp4  34665  djhlsmcl  34690  lcfl6  34776  lcfl8  34778  lcfrvalsnN  34817  lcfrlem9  34826  mapdval2N  34906  mapdordlem2  34913  mapd1o  34924  mapd0  34941  mapdheq2biN  35006  elrfi  35244  diophrw  35309  eldioph2b  35313  diophin  35323  rexrabdioph  35345  rmxycomplete  35470  coprmdvdsb  35542  jm2.19  35553  jm2.26  35562  jm2.27  35568  limsuc2  35604  dgraa0p  35713  rngunsnply  35737  fiuneneq  35769  hashgcdlem  35772  pwelg  35862  isprm7  36296  nzss  36302  dvconstbi  36319  expgrowth  36320  bcc0  36325  axc11next  36393  pm14.24  36419  sbiota1  36421  sbcim2g  36535  sineq0ALT  36973  pwssfi  37020  iccintsng  37208  limcresiooub  37294  limclr  37307  dvnmul  37386  dvmptfprodlem  37387  fourierdlem50  37587  fourierdlem89  37626  fourierdlem91  37628  sge0repnf  37761  sge0lefi  37773  sge0resplit  37781  sge0fodjrnlem  37791  sigarcol  37872  confun  37919  rexsb  37979  2reu2  37998  ralbinrald  38010  rlimdmafv  38068  el1fzopredsuc  38111  mod2eq1n2dvds  38114  iccpartiun  38137  dfodd6  38156  dfeven4  38157  gcdzeq  38182  evensumeven  38223  sgoldbalt  38271  ccats1pfxeqbi  38361  reuccatpfxs1  38364  ralxfrd2  38379  2ffzoeq  38412  usgra2pth  38423  uhgrauhgbi  38443  uhg0v  38446  isassintop  38603  uzlidlring  38686  rngciso  38741  rngcisoALTV  38753  ringciso  38792  ringcisoALTV  38816  domnmsuppn0  38913  lindslininds  39016  snlindsntor  39023  isldepslvec2  39037