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  315  pm5.501  339  2falsed  349  impbida  830  dedlem0b  951  dedlema  952  dedlemb  953  ifptruOLD  1392  ifpfalOLD  1394  albi  1647  exbi  1674  equequ1  1806  elequ1  1829  elequ2  1831  19.21t  1912  19.23t  1917  sbequ12  2000  cbv2h  2026  dral1  2073  dral1ALT  2074  ax12b  2092  sbequ  2121  sbft  2124  sb56  2176  exsb  2216  eupickb  2291  eupickbi  2292  2eu2  2309  eleq2d  2452  ceqsalt  3057  ceqex  3155  mob2  3204  reu6  3213  sbciegft  3283  eqsbc3r  3309  csbiebt  3368  sseq1  3438  reupick  3707  reupick2  3709  uneqdifeq  3832  prnebg  4126  disjeq2  4342  disjeq1  4345  disjxiun  4364  disjss3  4366  reusv2lem2  4567  reusv2lem3  4568  alxfr  4575  ralxfrd  4576  copsexg  4647  euotd  4662  poeq2  4718  sotric  4740  sotrieq  4741  freq2  4764  seeq1  4765  seeq2  4766  tz7.7  4818  ordtri1  4825  ordtri3  4828  ordelinel  4890  iss  5233  iotaval  5471  funeq  5515  funssres  5536  f0dom0  5677  tz6.12c  5793  fnbrfvb  5814  ssimaex  5839  fvimacnv  5904  elpreima  5909  eldmrexrnb  5940  fsn  5971  fnsnb  5992  fmptsng  5994  fmptsnd  5995  tpres  6026  fconst2g  6028  fconst5  6031  elunirn  6064  f1ocnvfvb  6086  foeqcnvco  6104  f1eqcocnv  6105  fliftfun  6111  soisores  6124  isofr  6139  isose  6140  isopo  6143  isoso  6145  f1oiso2  6149  eusvobj2  6189  oprabid  6223  f1opw2  6427  oneqmin  6539  ordsuc  6548  ordelsuc  6554  ordsucelsuc  6556  ordunisuc2  6578  limsuc  6583  f1ovv  6670  op1steq  6741  fvn0elsuppb  6835  extmptsuppeq  6842  rntpos  6886  smoiso2  6958  seqomlem2  7034  oaord  7114  oawordex  7124  oaordex  7125  omord2  7134  om00  7142  oeord  7155  nnaord  7186  nnmord  7199  nnawordex  7204  nnaordex  7205  erexb  7254  swoord1  7258  swoord2  7259  iiner  7301  eceqoveq  7334  ralxpmap  7387  omxpenlem  7537  domtriord  7582  mapxpen  7602  mapunen  7605  ssenen  7610  nneneq  7619  onomeneq  7626  nndomo  7630  en1eqsnbi  7666  fodomfib  7715  f1opwfi  7739  fsuppunbi  7765  elfiun  7805  suplub2  7835  ordiso2  7855  ordiso  7856  oieu  7879  brwdom2  7914  brwdom3  7923  cantnflem1  8021  cantnflem1OLD  8044  cardidm  8253  carddom2  8271  pm54.43  8294  pr2ne  8296  acnen  8347  acnen2  8349  alephord  8369  alephinit  8389  dfac5  8422  infdif2  8503  fictb  8538  coflim  8554  fincssdom  8616  fin23lem25  8617  isf32lem9  8654  isf34lem4  8670  fin1a2lem11  8703  axdc3lem2  8744  ficard  8853  fpwwe2lem12  8930  fpwwe2  8932  indpi  9196  nqereq  9224  1idpr  9318  ltapr  9334  leltne  9585  ltlen  9597  ltadd2  9599  addlsub  9896  ltord1  9996  mul0or  10106  ltmul1  10309  mulge0b  10329  lt2msq  10345  nnsub  10491  nn0sub  10763  zrevaddcl  10826  zltp1le  10830  zdiv  10850  nneo  10863  zeo2  10866  zmax  11098  zbtwnre  11099  qrevaddcl  11123  xrlttri  11266  xrleltne  11272  xralrple  11325  xltneg  11337  xleadd1  11368  xlemul1  11403  supxrunb1  11432  supxrunb2  11433  ioo0  11475  iccid  11495  ico0  11496  ioc0  11497  icc0  11498  difreicc  11573  iccsplit  11574  0fz1  11626  uzsplit  11672  fzm1  11680  fzrevral  11685  ssfzo12bi  11806  elfznelfzob  11815  flge  11841  modid2  11924  ssnn0fi  11997  seqf1olem1  12049  hashen  12322  hashdom  12350  hashle00  12369  hash2prb  12421  pr2pwpr  12424  hashtpg  12427  reuccats1  12617  ccats1swrdeqbi  12634  repsdf2  12661  scshwfzeqfzo  12705  relexpindlem  12898  shftlem  12903  shftuz  12904  abslt  13149  absle  13150  rexico  13188  cau3lem  13189  rlim2lt  13322  rlim3  13323  o1lo1  13362  rlimdm  13376  climshft  13401  o1dif  13454  isercolllem2  13490  isercoll  13492  zsum  13542  fsum  13544  fsum00  13614  incexclem  13650  zprod  13746  fprod  13750  dvdsval2  13991  moddvds  13995  negdvdsb  14002  dvdsnegb  14003  dvdscmulr  14014  dvdsmulcr  14015  dvdssub2  14025  fzo0dvdseq  14041  bitsf1ocnv  14096  sadcaddlem  14109  bitsuz  14126  dvdsgcdb  14184  gcdeq  14192  dvdssqlem  14199  isprm2lem  14226  dvdsprime  14232  dvdsprm  14242  coprm  14243  euclemma  14251  rpexp  14263  prmdiveq  14318  odzdvds  14324  pythagtrip  14360  pc2dvds  14404  pcprmpw2  14407  pcprmpw  14408  vdwapun  14494  ramtcl2  14531  firest  14840  mrieqv2d  15046  isacs2  15060  isssc  15226  setciso  15487  posasymb  15699  pleval2  15712  pltval3  15714  lublecllem  15735  joinle  15761  meetle  15775  lubun  15870  clatleglb  15873  latdisd  15937  letsr  15974  intopsn  15999  gsumval2a  16023  frmdss2  16148  isgrpid2  16203  isgrpinv  16217  symg1bas  16538  oddvdsnn0  16685  oddvds  16688  odeq  16691  odeq1  16699  gexdvds  16721  pgpfi  16742  pgpssslw  16751  fislw  16762  sylow3lem2  16765  lsmelvalm  16788  lsmlub  16800  lsmss1b  16802  lsmss2b  16804  efgs1b  16871  cyggenod  17004  cyggexb  17018  dprdfeq0  17175  dprdfeq0OLD  17182  unitmulclb  17427  dvreq1  17455  f1rhm0to0  17502  f1rhm0to0ALT  17503  drngmul0or  17530  isabvd  17582  issrngd  17623  lssats2  17759  lspsneq0  17771  lsmelval2  17844  lvecvs0or  17867  lspsneq  17881  lspsneu  17882  lidl1el  17979  lidldvgen  18016  isnzr2  18024  0ringnnzr  18030  0ring01eqbi  18034  rrgeq0  18051  domneq0  18059  ply1coe1eq  18453  cply1coe0bi  18455  znunit  18693  psgndif  18729  ipeq0  18764  ocvsscon  18797  pjdm2  18833  obselocv  18850  islinds4  18955  mat1dimelbas  19058  cramer  19278  unitgOLD  19554  tgss3  19573  clsval2  19636  isopn3  19653  elcls3  19670  opncldf1  19671  neiint  19691  neips  19700  opnneissb  19701  opnssneib  19702  opnnei  19707  tpnei  19708  opnneiid  19713  restcld  19759  restopnb  19762  tgcn  19839  tgcnp  19840  subbascn  19841  iscnp4  19850  cnpnei  19851  cncls2  19860  cncls  19861  cnntr  19862  lmss  19885  hausnei2  19940  lpcls  19951  ordtt1  19966  cmpsub  19986  tgcmp  19987  1stcelcls  20047  locfincmp  20112  kgencn2  20143  ptpjpre1  20157  upxp  20209  txcn  20212  txlm  20234  tgqtop  20298  kqfvima  20316  isr0  20323  regr1lem2  20326  hmeoopn  20352  hmeocld  20353  ptuncnv  20393  fbunfip  20455  fgss2  20460  ufilb  20492  ufprim  20495  trufil  20496  cfinufil  20514  ufildr  20517  elfm2  20534  elfm3  20536  rnelfm  20539  fmfnfmlem4  20543  fmco  20547  flimtopon  20556  flimopn  20561  fbflim2  20563  flimrest  20569  flffbas  20581  cnpflf  20587  fclstopon  20598  fclsnei  20605  fclsbas  20607  fclsfnflim  20613  fclscmp  20616  ufilcmp  20618  isfcf  20620  fcfnei  20621  cnpfcf  20627  alexsubb  20631  alexsubALT  20636  cldsubg  20694  tgphaus  20700  tgpt0  20702  tsmsgsum  20722  tsmsgsumOLD  20725  tsmsresOLD  20730  tsmsres  20731  xbln0  21002  blssexps  21014  blssex  21015  isxms2  21036  prdsbl  21079  neibl  21089  metss  21096  met2ndc  21111  metrest  21112  metcnp3  21128  nmoeq0  21328  xrsxmet  21399  reconn  21418  iccpnfcnv  21529  fgcfil  21795  iscau4  21803  cfilres  21820  iunmbl2  22052  ismbf3d  22146  mbfaddlem  22152  i1faddlem  22185  i1fmullem  22186  ellimc3  22368  tdeglem4  22543  deg1nn0clb  22575  deg1lt0  22576  dvdsq1p  22646  plypf1  22694  0dgrb  22728  plymul0or  22762  ulmshft  22870  ulmcaulem  22874  ulmcau  22875  cosord  23004  eff1olem  23020  lognegb  23062  eflogeq  23074  logdivlt  23093  efopn  23126  cxpeq0  23146  cxpeq  23218  angpieqvd  23278  dcubic  23293  asinsinb  23344  acoscosb  23345  atantanb  23371  rlimcnp  23412  isppw  23505  isppw2  23506  vmappw  23507  isnsqf  23526  ppieq0  23567  fsumdvdsdiag  23577  dvdsppwf1o  23579  fsumfldivdiag  23583  chpeq0  23600  chteq0  23601  dchrptlem1  23656  lgsdir2lem4  23718  lgsne0  23725  lgsqr  23738  lgsdchrval  23739  lgsquadlem1  23746  m1lgs  23754  brbtwn  24323  brcgr  24324  brbtwn2  24329  axcontlem7  24394  ausisusgra  24476  nbgraf1olem5  24566  edgusgranbfin  24571  nb3graprlem1  24572  cusgrarn  24580  nbcusgra  24584  cusgrafilem2  24601  uvtxnbgra  24614  uvtxnb  24618  spthonepeq  24710  3v3e3cycl  24786  wlkiswwlk  24819  wlklniswwlkn  24822  wwlknextbi  24846  wwlknredwwlkn0  24848  wwlkextwrd  24849  wwlkextprop  24865  0clwlk  24886  clwlkisclwwlklem0  24909  el2wlkonot  24990  el2spthonot  24991  el2wlkonotot0  24993  el2wlksotot  25003  usg2wlkonot  25004  usg2spthonot  25009  usg2spthonot0  25010  nbhashuvtx  25037  uvtxhashnb  25038  0eusgraiff0rgra  25060  cusgraiffrusgra  25061  eupath2lem3  25100  frgra3vlem2  25122  frgrancvvdeqlem3  25153  numclwwlkun  25200  grpoinvf  25359  rngosn3  25545  rngoueqz  25549  rngoridfz  25554  nvmul0or  25664  nvz  25689  diporthcom  25746  ubthlem3  25905  hvmul0or  26059  his6  26133  hial0  26136  hial02  26137  orthcom  26142  normgt0  26161  ocin  26331  occon3  26332  shsel3  26350  shlub  26449  chssoc  26531  h1de2bi  26589  spansncol  26603  elspansn4  26608  spansnss2  26610  sumspansn  26684  lnopcnbd  27071  lnfncnbd  27092  riesz1  27100  elpjrn  27225  cvcon3  27319  dmdmd  27335  dmdbr3  27340  dmdbr4  27341  dmdbr5  27343  mdslmd1i  27364  atcveq0  27383  chcv1  27390  atssma  27413  atcv0eq  27414  atcv1  27415  bian1d  27483  br8d  27597  fpwrelmap  27706  xaddeq0  27723  eliccelico  27741  elicoelioo  27742  isarchiofld  27961  unitdivcld  28037  xrge0iifcnv  28069  lmxrge0  28088  indf1ofs  28174  eulerpartlemgh  28500  dstfrvunirn  28596  cvmliftmolem2  28916  cvmlift2lem12  28948  mthmb  29130  ghomf1olem  29223  climuzcnv  29226  br8  29351  br6  29352  br4  29353  funbreq  29366  fprb  29368  axext4dist  29398  nodenselem8  29613  dfrdg4  29753  cgrcom  29793  cgrcoml  29799  cgrdegen  29807  btwncom  29817  brsegle  29911  brsegle2  29912  colinbtwnle  29921  btwnoutside  29928  broutsideof3  29929  outsidele  29935  lineunray  29950  lineelsb2  29951  elhf2  29985  ontgval  30049  ordtop  30054  ordcmp  30065  nndivsub  30075  wl-lem-exsb  30180  wl-mo3t  30186  wl-ax11-lem1  30190  cnambfre  30228  itg2addnc  30235  elicc3  30301  nn0prpwlem  30306  opnbnd  30309  cldbnd  30310  opnregcld  30314  cldregopn  30315  fnessref  30341  refssfne  30342  neibastop2  30345  fnemeet2  30351  fnejoin2  30353  fgmin  30354  brabg2  30372  istotbnd3  30433  sstotbnd2  30436  sstotbnd  30437  sstotbnd3  30438  ssbnd  30450  ismtybnd  30469  reheibor  30501  grpoeqdivid  30509  grpokerinj  30513  1idl  30589  0rngo  30590  divrngidl  30591  igenval2  30629  ispridlc  30633  isdmn3  30637  prtlem10  30772  prter2  30788  elrfi  30792  diophrw  30857  eldioph2b  30861  diophin  30871  rexrabdioph  30893  rmxycomplete  31018  coprmdvdsb  31090  jm2.19  31101  jm2.26  31110  jm2.27  31116  limsuc2  31152  dgraa0p  31266  rngunsnply  31290  fiuneneq  31322  hashgcdlem  31325  isprm7  31360  lcmeq0  31374  lcmdvdsb  31385  nzss  31390  dvconstbi  31407  expgrowth  31408  bcc0  31413  axc11next  31481  pm14.24  31507  sbiota1  31509  iccintsng  31729  limcresiooub  31814  limclr  31827  dvnmul  31906  dvmptfprodlem  31907  fourierdlem50  32105  fourierdlem89  32144  fourierdlem91  32146  sigarcol  32247  rexsb  32339  2reu2  32358  ralbinrald  32370  rlimdmafv  32428  mod2eq1n2dvds  32462  dfodd6  32480  dfeven4  32481  gcdzeq  32506  ccats1pfxeqbi  32606  reuccatpfxs1  32609  ralxfrd2  32624  2ffzoeq  32661  usgra2pth  32672  uhgrauhgbi  32692  uhg0v  32695  isassintop  32852  uzlidlring  32935  rngciso  32990  rngcisoALTV  33002  ringciso  33041  ringcisoALTV  33065  domnmsuppn0  33162  lindslininds  33265  snlindsntor  33272  isldepslvec2  33286  sbcim2g  33645  sineq0ALT  34084  bnj145OLD  34129  bj-cbv2hv  34641  bj-dral1v  34673  bj-sbftv  34692  bj-sb56  34696  bj-equsal1t  34742  bj-19.21t  34750  bj-ceqsalt0  34796  bj-ceqsalt1  34797  bj-xpnzexb  34866  bj-finsumval0  35010  bj-ldiv  35018  bj-bary1  35025  dral1-o  35046  lshpinN  35127  lsatcveq0  35170  lsatcv0eq  35185  lsatcv1  35186  islshpcv  35191  lkr0f  35232  lkrshp4  35246  lshpkrlem1  35248  lshpset2N  35257  lfl1dim  35259  lfl1dim2N  35260  lub0N  35327  glb0N  35331  oplecon3b  35338  cmtcomN  35387  cmtbr3N  35392  cmtbr4N  35393  cvrnbtwn2  35413  cvrnbtwn3  35414  cvrcon3b  35415  cvrnbtwn4  35417  cvrcmp  35421  atcvreq0  35452  atnle  35455  atlatle  35458  cvlexchb1  35468  cvlcvr1  35477  hlrelat2  35540  exatleN  35541  cvrval3  35550  cvrval4N  35551  cvrexch  35557  atcvr0eq  35563  lnnat  35564  atcvrj0  35565  atcvrj2b  35569  atltcvr  35572  atbtwn  35583  ps-1  35614  3at  35627  islln2a  35654  llncmp  35659  islpln2a  35685  lplncmp  35699  islvol2aN  35729  4at  35750  lvolcmp  35754  pmaple  35898  lncmp  35920  paddss  35982  llnexchb2lem  36005  2polcon4bN  36055  ispsubcl2N  36084  lhpat3  36183  lautcvr  36229  ltrnid  36272  trlval2  36301  trlatn0  36310  ltrnideq  36313  trlnidatb  36315  cdlemeg49lebilem  36678  trlord  36708  cdlemg1a  36709  cdlemg1cex  36727  tendoid0  36964  dva1dim  37124  cdlemm10N  37258  diarnN  37269  cdlemn  37352  dihlspsnssN  37472  dihatexv  37478  dochkrshp  37526  dochkrshp4  37529  djhlsmcl  37554  lcfl6  37640  lcfl8  37642  lcfrvalsnN  37681  lcfrlem9  37690  mapdval2N  37770  mapdordlem2  37777  mapd1o  37788  mapd0  37805  mapdheq2biN  37870  pwelg  38174