Theorem impbid 191

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

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

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 185

This theorem is referenced by:  bicom1  199  impbid1  203  impcon4bid  205  pm5.74  244  imbi1d  317  pm5.501  341  2falsed  351  impbida  830  dedlem0b  951  dedlema  952  dedlemb  953  albi  1619  exbi  1643  equequ1  1747  elequ1  1770  elequ2  1772  19.21t  1852  19.23t  1856  sbequ12  1961  cbv2h  1991  dral1  2040  dral1ALT  2041  ax12b  2059  sbequ  2090  sbft  2093  sbiedOLD  2126  sb56  2154  sbal1OLD  2194  exsb  2203  dral1-o  2226  eupickb  2366  eupickbOLD  2367  eupickbi  2368  eupickbiOLD  2369  2eu2  2388  eleq2d  2537  ceqsalt  3136  ceqex  3234  mob2  3283  reu6  3292  sbciegft  3362  eqsbc3r  3393  csbiebt  3455  sseq1  3525  reupick  3782  reupick2  3784  uneqdifeq  3915  prnebg  4208  disjeq2  4421  disjeq1  4424  disjxiun  4444  disjss3  4446  reusv2lem2  4649  reusv2lem3  4650  alxfr  4660  ralxfrd  4661  copsexg  4732  copsexgOLD  4733  euotd  4748  poeq2  4804  sotric  4826  sotrieq  4827  freq2  4850  seeq1  4851  seeq2  4852  tz7.7  4904  ordtri1  4911  ordtri3  4914  ordelinel  4976  iss  5319  iotaval  5560  funeq  5605  funssres  5626  f0dom0  5767  tz6.12c  5883  fnbrfvb  5906  ssimaex  5930  fvimacnv  5994  elpreima  5999  eldmrexrnb  6026  fsn  6057  fnsnb  6078  fmptsng  6080  fmptsnd  6081  fconst2g  6113  fconst5  6116  elunirn  6149  f1ocnvfvb  6171  foeqcnvco  6189  f1eqcocnv  6190  fliftfun  6196  soisores  6209  isofr  6224  isose  6225  isopo  6228  isoso  6230  f1oiso2  6234  eusvobj2  6275  oprabid  6306  f1opw2  6510  oneqmin  6618  ordsuc  6627  ordelsuc  6633  ordsucelsuc  6635  ordunisuc2  6657  limsuc  6662  f1ovv  6752  op1steq  6823  extmptsuppeq  6921  rntpos  6965  smoiso2  7037  seqomlem2  7113  oaord  7193  oawordex  7203  oaordex  7204  omord2  7213  om00  7221  oeord  7234  nnaord  7265  nnmord  7278  nnawordex  7283  nnaordex  7284  erexb  7333  swoord1  7337  swoord2  7338  iiner  7380  eceqoveq  7413  ralxpmap  7465  omxpenlem  7615  domtriord  7660  mapxpen  7680  mapunen  7683  ssenen  7688  nneneq  7697  onomeneq  7704  nndomo  7708  fodomfib  7796  f1opwfi  7820  fsuppunbi  7846  elfiun  7886  suplub2  7917  ordiso2  7936  ordiso  7937  oieu  7960  brwdom2  7995  brwdom3  8004  cantnflem1  8104  cantnflem1OLD  8127  cardidm  8336  carddom2  8354  pm54.43  8377  pr2ne  8379  acnen  8430  acnen2  8432  alephord  8452  alephinit  8472  dfac5  8505  infdif2  8586  fictb  8621  coflim  8637  fincssdom  8699  fin23lem25  8700  isf32lem9  8737  isf34lem4  8753  fin1a2lem11  8786  axdc3lem2  8827  ficard  8936  fpwwe2lem12  9015  fpwwe2  9017  indpi  9281  nqereq  9309  1idpr  9403  ltapr  9419  leltne  9670  ltlen  9682  ltadd2  9684  ltord1  10075  mul0or  10185  ltmul1  10388  mulge0b  10408  lt2msq  10425  nnsub  10570  nn0sub  10842  zrevaddcl  10904  zltp1le  10908  zdiv  10927  nneo  10940  zeo2  10943  zmax  11175  zbtwnre  11176  qrevaddcl  11200  xrlttri  11341  xrleltne  11347  xralrple  11400  xltneg  11412  xleadd1  11443  xlemul1  11478  supxrunb1  11507  supxrunb2  11508  ioo0  11550  iccid  11570  ico0  11571  ioc0  11572  icc0  11573  difreicc  11648  iccsplit  11649  0fz1  11701  uzsplit  11746  fzm1  11754  fzrevral  11758  ssfzo12bi  11871  elfznelfzob  11880  flge  11906  modid2  11986  ssnn0fi  12057  seqf1olem1  12109  hashen  12382  hashdom  12409  hashle00  12425  euhash1  12439  hash2prb  12477  pr2pwpr  12480  hashtpg  12483  reuccats1  12663  ccats1swrdeqbi  12680  repsdf2  12707  scshwfzeqfzo  12751  shftlem  12858  shftuz  12859  abslt  13103  absle  13104  rexico  13142  cau3lem  13143  rlim2lt  13276  rlim3  13277  o1lo1  13316  rlimdm  13330  climshft  13355  o1dif  13408  isercolllem2  13444  isercoll  13446  zsum  13496  fsum  13498  fsum00  13568  incexclem  13604  dvdsval2  13843  moddvds  13847  negdvdsb  13854  dvdsnegb  13855  dvdscmulr  13866  dvdsmulcr  13867  dvdssub2  13875  fzo0dvdseq  13891  bitsf1ocnv  13946  sadcaddlem  13959  bitsuz  13976  dvdsgcdb  14034  gcdeq  14042  dvdssqlem  14049  isprm2lem  14076  dvdsprime  14082  dvdsprm  14092  coprm  14093  euclemma  14101  rpexp  14113  prmdiveq  14168  odzdvds  14174  pythagtrip  14210  pc2dvds  14254  pcprmpw2  14257  pcprmpw  14258  vdwapun  14344  ramtcl2  14381  firest  14681  mrieqv2d  14887  isacs2  14901  isssc  15043  setciso  15269  posasymb  15432  pleval2  15445  pltval3  15447  lublecllem  15468  joinle  15494  meetle  15508  lubun  15603  clatleglb  15606  latdisd  15670  letsr  15707  gsumval2a  15822  frmdss2  15851  isgrpid2  15884  isgrpinv  15898  symg1bas  16213  oddvdsnn0  16361  oddvds  16364  odeq  16367  odeq1  16375  gexdvds  16397  pgpfi  16418  pgpssslw  16427  fislw  16438  sylow3lem2  16441  lsmelvalm  16464  lsmlub  16476  lsmss1b  16478  lsmss2b  16480  efgs1b  16547  cyggenod  16675  cyggexb  16689  dprdfeq0  16849  dprdfeq0OLD  16856  unitmulclb  17095  dvreq1  17123  f1rhm0to0  17169  f1rhm0to0ALT  17170  drngmul0or  17197  isabvd  17249  issrngd  17290  lssats2  17426  lspsneq0  17438  lsmelval2  17511  lvecvs0or  17534  lspsneq  17548  lspsneu  17549  lidl1el  17645  lidldvgen  17682  isnzr2  17690  rrgeq0  17706  domneq0  17714  ply1coe1eq  18108  cply1coe0bi  18110  znunit  18366  psgndif  18402  ipeq0  18437  ocvsscon  18470  pjdm2  18506  obselocv  18523  islinds4  18634  mat1dimelbas  18737  cramer  18957  unitg  19232  tgss3  19251  clsval2  19314  isopn3  19330  elcls3  19347  opncldf1  19348  neiint  19368  neips  19377  opnneissb  19378  opnssneib  19379  opnnei  19384  tpnei  19385  opnneiid  19390  restcld  19436  restopnb  19439  tgcn  19516  tgcnp  19517  subbascn  19518  iscnp4  19527  cnpnei  19528  cncls2  19537  cncls  19538  cnntr  19539  lmss  19562  hausnei2  19617  lpcls  19628  ordtt1  19643  cmpsub  19663  tgcmp  19664  1stcelcls  19725  kgencn2  19790  ptpjpre1  19804  upxp  19856  txcn  19859  txlm  19881  tgqtop  19945  kqfvima  19963  isr0  19970  regr1lem2  19973  hmeoopn  19999  hmeocld  20000  ptuncnv  20040  fbunfip  20102  fgss2  20107  ufilb  20139  ufprim  20142  trufil  20143  cfinufil  20161  ufildr  20164  elfm2  20181  elfm3  20183  rnelfm  20186  fmfnfmlem4  20190  fmco  20194  flimtopon  20203  flimopn  20208  fbflim2  20210  flimrest  20216  flffbas  20228  cnpflf  20234  fclstopon  20245  fclsnei  20252  fclsbas  20254  fclsfnflim  20260  fclscmp  20263  ufilcmp  20265  isfcf  20267  fcfnei  20268  cnpfcf  20274  alexsubb  20278  alexsubALT  20283  cldsubg  20341  tgphaus  20347  tgpt0  20349  tsmsgsum  20369  tsmsgsumOLD  20372  tsmsresOLD  20377  tsmsres  20378  xbln0  20649  blssexps  20661  blssex  20662  isxms2  20683  prdsbl  20726  neibl  20736  metss  20743  met2ndc  20758  metrest  20759  metcnp3  20775  nmoeq0  20975  xrsxmet  21046  reconn  21065  iccpnfcnv  21176  fgcfil  21442  iscau4  21450  cfilres  21467  iunmbl2  21699  ismbf3d  21793  mbfaddlem  21799  i1faddlem  21832  i1fmullem  21833  ellimc3  22015  tdeglem4  22190  deg1nn0clb  22222  deg1lt0  22223  dvdsq1p  22293  plypf1  22341  0dgrb  22375  plymul0or  22408  ulmshft  22516  ulmcaulem  22520  ulmcau  22521  cosord  22649  eff1olem  22665  lognegb  22699  eflogeq  22711  logdivlt  22731  efopn  22764  cxpeq0  22784  cxpeq  22856  angpieqvd  22887  dcubic  22902  asinsinb  22953  acoscosb  22954  atantanb  22980  rlimcnp  23020  isppw  23113  isppw2  23114  vmappw  23115  isnsqf  23134  ppieq0  23175  fsumdvdsdiag  23185  dvdsppwf1o  23187  fsumfldivdiag  23191  chpeq0  23208  chteq0  23209  dchrptlem1  23264  lgsdir2lem4  23326  lgsne0  23333  lgsqr  23346  lgsdchrval  23347  lgsquadlem1  23354  m1lgs  23362  brbtwn  23875  brcgr  23876  brbtwn2  23881  axcontlem7  23946  ausisusgra  24028  nbgraf1olem5  24118  edgusgranbfin  24123  nb3graprlem1  24124  cusgrarn  24132  nbcusgra  24136  cusgrafilem2  24153  uvtxnbgra  24166  uvtxnb  24170  spthonepeq  24262  3v3e3cycl  24338  wlkiswwlk  24371  wlklniswwlkn  24374  wwlknextbi  24398  wwlknredwwlkn0  24400  wwlkextwrd  24401  wwlkextprop  24417  0clwlk  24438  clwlkisclwwlklem0  24461  el2wlkonot  24542  el2spthonot  24543  el2wlkonotot0  24545  el2wlksotot  24555  usg2wlkonot  24556  usg2spthonot  24561  usg2spthonot0  24562  nbhashuvtx  24589  uvtxhashnb  24590  0eusgraiff0rgra  24612  cusgraiffrusgra  24613  eupath2lem3  24652  frgra3vlem2  24674  frgrancvvdeqlem3  24706  numclwwlkun  24753  grpoinvf  24915  rngosn3  25101  rngosn4  25102  rngoueqz  25105  rngoridfz  25110  nvmul0or  25220  nvz  25245  diporthcom  25302  ubthlem3  25461  hvmul0or  25615  his6  25689  hial0  25692  hial02  25693  orthcom  25698  normgt0  25717  ocin  25887  occon3  25888  shsel3  25906  shlub  26005  chssoc  26087  h1de2bi  26145  spansncol  26159  elspansn4  26164  spansnss2  26166  sumspansn  26240  lnopcnbd  26628  lnfncnbd  26649  riesz1  26657  elpjrn  26782  cvcon3  26876  dmdmd  26892  dmdbr3  26897  dmdbr4  26898  dmdbr5  26900  mdslmd1i  26921  atcveq0  26940  chcv1  26947  atssma  26970  atcv0eq  26971  atcv1  26972  bian1d  27039  relfi  27129  br8d  27133  fcobij  27217  resf1o  27222  fpwrelmapffslem  27224  fpwrelmap  27225  xaddeq0  27238  eliccelico  27253  elicoelioo  27254  isarchiofld  27467  pstmfval  27508  unitdivcld  27516  prsdm  27529  prsrn  27530  xrge0iifcnv  27548  lmxrge0  27567  indf1ofs  27676  eulerpartlemgh  27954  dstfrvunirn  28050  cvmliftmolem2  28364  cvmlift2lem12  28396  ghomf1olem  28506  climuzcnv  28509  relexpindlem  28534  zprod  28643  fprod  28647  br8  28759  br6  28760  br4  28761  funbreq  28775  fprb  28777  axext4dist  28807  nodenselem8  29022  dfrdg4  29174  cgrcom  29214  cgrcoml  29220  cgrdegen  29228  btwncom  29238  brsegle  29332  brsegle2  29333  colinbtwnle  29342  btwnoutside  29349  broutsideof3  29350  outsidele  29356  lineunray  29371  lineelsb2  29372  elhf2  29406  ontgval  29470  ordtop  29475  ordcmp  29486  nndivsub  29496  wl-lem-exsb  29589  wl-mo3t  29595  wl-ax11-lem1  29599  cnambfre  29638  itg2addnc  29644  elicc3  29710  nn0prpwlem  29715  opnbnd  29718  cldbnd  29719  opnregcld  29723  cldregopn  29724  fnessref  29763  refssfne  29764  locfincmp  29774  neibastop2  29780  fnemeet2  29786  fnejoin2  29788  fgmin  29789  brabg2  29807  istotbnd3  29868  sstotbnd2  29871  sstotbnd  29872  sstotbnd3  29873  ssbnd  29885  ismtybnd  29904  reheibor  29936  grpoeqdivid  29944  grpokerinj  29948  1idl  30024  0rngo  30025  divrngidl  30026  igenval2  30064  ispridlc  30068  isdmn3  30072  prtlem10  30208  prter2  30224  elrfi  30228  diophrw  30294  eldioph2b  30298  diophin  30308  rexrabdioph  30329  rmxycomplete  30455  coprmdvdsb  30527  jm2.19  30539  jm2.26  30548  jm2.27  30554  limsuc2  30590  dgraa0p  30703  rngunsnply  30727  fiuneneq  30759  hashgcdlem  30762  isprm7  30795  lcmeq0  30806  lcmdvdsb  30817  nzss  30822  dvconstbi  30839  expgrowth  30840  axc11next  30891  pm14.24  30917  sbiota1  30919  ioossioobi  31121  iccshift  31122  iocopn  31124  iooshift  31126  iccintsng  31127  icoopn  31129  limcdm0  31160  islptre  31161  islpcn  31181  limcresiooub  31184  limcresioolb  31185  limclr  31197  itgiccshift  31298  itgperiod  31299  fourierdlem32  31439  fourierdlem33  31440  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem81  31488  fourierdlem89  31496  fourierdlem91  31498  sigarcol  31548  rexsb  31640  2reu2  31659  ralbinrald  31671  rlimdmafv  31729  ralxfrd2  31770  2ffzoeq  31810  usgra2pth  31823  uhgrauhgbi  31843  uhg0v  31846  0rngnnzr  32031  domnmsuppn0  32035  lindslininds  32138  snlindsntor  32145  isldepslvec2  32159  sbcim2g  32389  sineq0ALT  32817  bnj145OLD  32862  bj-iftru  33233  bj-iffal  33234  bj-cbv2hv  33376  bj-dral1v  33407  bj-sbftv  33426  bj-sb56  33430  bj-equsal1t  33476  bj-19.21t  33484  bj-ceqsalt0  33530  bj-ceqsalt1  33531  bj-xpnzexb  33599  bj-finsumval0  33735  bj-lsub  33743  bj-ldiv  33746  bj-bary1  33753  lshpinN  33786  lsatcveq0  33829  lsatcv0eq  33844  lsatcv1  33845  islshpcv  33850  lkr0f  33891  lkrshp4  33905  lshpkrlem1  33907  lshpset2N  33916  lfl1dim  33918  lfl1dim2N  33919  lub0N  33986  glb0N  33990  oplecon3b  33997  cmtcomN  34046  cmtbr3N  34051  cmtbr4N  34052  cvrnbtwn2  34072  cvrnbtwn3  34073  cvrcon3b  34074  cvrnbtwn4  34076  cvrcmp  34080  atcvreq0  34111  atnle  34114  atlatle  34117  cvlexchb1  34127  cvlcvr1  34136  hlrelat2  34199  exatleN  34200  cvrval3  34209  cvrval4N  34210  cvrexch  34216  atcvr0eq  34222  lnnat  34223  atcvrj0  34224  atcvrj2b  34228  atltcvr  34231  atbtwn  34242  ps-1  34273  3at  34286  islln2a  34313  llncmp  34318  islpln2a  34344  lplncmp  34358  islvol2aN  34388  4at  34409  lvolcmp  34413  pmaple  34557  lncmp  34579  paddss  34641  llnexchb2lem  34664  2polcon4bN  34714  ispsubcl2N  34743  lhpat3  34842  lautcvr  34888  ltrnid  34931  trlval2  34959  trlatn0  34968  ltrnideq  34971  trlnidatb  34973  cdlemeg49lebilem  35335  trlord  35365  cdlemg1a  35366  cdlemg1cex  35384  tendoid0  35621  dva1dim  35781  cdlemm10N  35915  diarnN  35926  cdlemn  36009  dihlspsnssN  36129  dihatexv  36135  dochkrshp  36183  dochkrshp4  36186  djhlsmcl  36211  lcfl6  36297  lcfl8  36299  lcfrvalsnN  36338  lcfrlem9  36347  mapdval2N  36427  mapdordlem2  36434  mapd1o  36445  mapd0  36462  mapdheq2biN  36527