Theorem impbid 191

Description: Deduce an equivalence from two implications. (Contributed by NM, 24-Jan-1993.) (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  828  dedlem0b  944  dedlema  945  dedlemb  946  albi  1609  exbi  1633  equequ1  1736  elequ1  1759  elequ2  1761  19.21t  1837  19.23t  1841  sbequ12  1936  cbv2h  1966  dral1  2017  dral1ALT  2018  ax12b  2036  sbequ  2067  sbft  2070  sbiedOLD  2103  sb56  2132  sbal1OLD  2172  exsb  2180  dral1-o  2203  eupickb  2342  eupickbOLD  2343  eupickbi  2344  eupickbiOLD  2345  2eu2  2362  ceqsalt  2990  ceqex  3085  mob2  3134  reu6  3143  sbciegft  3212  eqsbc3r  3243  csbiebt  3303  sseq1  3372  reupick  3629  reupick2  3631  uneqdifeq  3762  prnebg  4049  disjeq2  4261  disjeq1  4264  disjxiun  4284  disjss3  4286  reusv2lem2  4489  reusv2lem3  4490  alxfr  4500  ralxfrd  4501  copsexg  4571  copsexgOLD  4572  euotd  4587  poeq2  4640  sotric  4662  sotrieq  4663  freq2  4686  seeq1  4687  seeq2  4688  tz7.7  4740  ordtri1  4747  ordtri3  4750  ordelinel  4812  iss  5149  iotaval  5387  funeq  5432  funssres  5453  f0dom0  5590  tz6.12c  5704  fnbrfvb  5727  ssimaex  5751  fvimacnv  5813  elpreima  5818  eldmrexrnb  5845  fsn  5876  fnsnb  5893  fmptsng  5895  fconst2g  5927  fconst5  5930  elunirn  5963  f1ocnvfvb  5981  foeqcnvco  5993  f1eqcocnv  5994  fliftfun  6000  soisores  6013  isofr  6028  isose  6029  isopo  6032  isoso  6034  f1oiso2  6038  eusvobj2  6079  oprabid  6110  f1opw2  6308  oneqmin  6411  ordsuc  6420  ordelsuc  6426  ordsucelsuc  6428  ordunisuc2  6450  limsuc  6455  f1ovv  6543  op1steq  6613  extmptsuppeq  6708  rntpos  6753  smoiso2  6822  seqomlem2  6898  oaord  6978  oawordex  6988  oaordex  6989  omord2  6998  om00  7006  oeord  7019  nnaord  7050  nnmord  7063  nnawordex  7068  nnaordex  7069  erexb  7118  swoord1  7122  swoord2  7123  iiner  7164  eceqoveq  7197  ralxpmap  7254  omxpenlem  7404  domtriord  7449  mapxpen  7469  mapunen  7472  ssenen  7477  nneneq  7486  onomeneq  7492  nndomo  7496  fodomfib  7583  f1opwfi  7607  fsuppunbi  7633  elfiun  7672  suplub2  7703  ordiso2  7721  ordiso  7722  oieu  7745  brwdom2  7780  brwdom3  7789  cantnflem1  7889  cantnflem1OLD  7912  cardidm  8121  carddom2  8139  pm54.43  8162  pr2ne  8164  acnen  8215  acnen2  8217  alephord  8237  alephinit  8257  dfac5  8290  infdif2  8371  fictb  8406  coflim  8422  fincssdom  8484  fin23lem25  8485  isf32lem9  8522  isf34lem4  8538  fin1a2lem11  8571  axdc3lem2  8612  ficard  8721  fpwwe2lem12  8800  fpwwe2  8802  indpi  9068  nqereq  9096  1idpr  9190  ltapr  9206  leltne  9456  ltlen  9468  ltadd2  9470  ltord1  9858  mul0or  9968  ltmul1  10171  mulge0b  10191  lt2msq  10208  nnsub  10352  nn0sub  10622  zrevaddcl  10682  zltp1le  10686  zdiv  10704  nneo  10717  zeo2  10720  zmax  10942  zbtwnre  10943  qrevaddcl  10967  xrlttri  11108  xrleltne  11114  xralrple  11167  xltneg  11179  xleadd1  11210  xlemul1  11245  supxrunb1  11274  supxrunb2  11275  ioo0  11317  iccid  11337  ico0  11338  ioc0  11339  icc0  11340  difreicc  11409  iccsplit  11410  0fz1  11461  uzsplit  11522  fzm1  11532  fzrevral  11536  ssfzo12bi  11614  elfznelfzob  11623  flge  11647  modid2  11727  seqf1olem1  11837  hashen  12110  hashdom  12134  hashle00  12150  euhash1  12164  hash2prb  12172  pr2pwpr  12175  hashtpg  12178  ccats1swrdeqbi  12381  repsdf2  12408  shftlem  12549  shftuz  12550  abslt  12794  absle  12795  rexico  12833  cau3lem  12834  rlim2lt  12967  rlim3  12968  o1lo1  13007  rlimdm  13021  climshft  13046  o1dif  13099  isercolllem2  13135  isercoll  13137  zsum  13187  fsum  13189  fsum00  13253  incexclem  13291  dvdsval2  13530  moddvds  13534  negdvdsb  13541  dvdsnegb  13542  dvdscmulr  13553  dvdsmulcr  13554  dvdssub2  13562  fzo0dvdseq  13578  bitsf1ocnv  13632  sadcaddlem  13645  bitsuz  13662  dvdsgcdb  13720  gcdeq  13728  dvdssqlem  13735  isprm2lem  13762  dvdsprime  13768  dvdsprm  13777  coprm  13778  euclemma  13786  rpexp  13798  prmdiveq  13853  odzdvds  13859  pythagtrip  13893  pc2dvds  13937  pcprmpw2  13940  pcprmpw  13941  vdwapun  14027  ramtcl2  14064  firest  14363  mrieqv2d  14569  isacs2  14583  isssc  14725  setciso  14951  posasymb  15114  pleval2  15127  pltval3  15129  lublecllem  15150  joinle  15176  meetle  15190  lubun  15285  clatleglb  15288  latdisd  15352  letsr  15389  gsumval2a  15503  frmdss2  15532  isgrpid2  15565  isgrpinv  15579  symg1bas  15892  oddvdsnn0  16038  oddvds  16041  odeq  16044  odeq1  16052  gexdvds  16074  pgpfi  16095  pgpssslw  16104  fislw  16115  sylow3lem2  16118  lsmelvalm  16141  lsmlub  16153  lsmss1b  16155  lsmss2b  16157  efgs1b  16224  cyggenod  16352  cyggexb  16366  dprdfeq0  16500  dprdfeq0OLD  16507  unitmulclb  16745  dvreq1  16773  drngmul0or  16831  isabvd  16883  issrngd  16924  lssats2  17058  lspsneq0  17070  lsmelval2  17143  lvecvs0or  17166  lspsneq  17180  lspsneu  17181  lidl1el  17277  lidldvgen  17314  isnzr2  17322  rrgeq0  17338  domneq0  17346  znunit  17971  psgndif  18007  ipeq0  18042  ocvsscon  18075  pjdm2  18111  obselocv  18128  islinds4  18239  cramer  18472  unitg  18547  tgss3  18566  clsval2  18629  isopn3  18645  elcls3  18662  opncldf1  18663  neiint  18683  neips  18692  opnneissb  18693  opnssneib  18694  opnnei  18699  tpnei  18700  opnneiid  18705  restcld  18751  restopnb  18754  tgcn  18831  tgcnp  18832  subbascn  18833  iscnp4  18842  cnpnei  18843  cncls2  18852  cncls  18853  cnntr  18854  lmss  18877  hausnei2  18932  lpcls  18943  ordtt1  18958  cmpsub  18978  tgcmp  18979  1stcelcls  19040  kgencn2  19105  ptpjpre1  19119  upxp  19171  txcn  19174  txlm  19196  tgqtop  19260  kqfvima  19278  isr0  19285  regr1lem2  19288  hmeoopn  19314  hmeocld  19315  ptuncnv  19355  fbunfip  19417  fgss2  19422  ufilb  19454  ufprim  19457  trufil  19458  cfinufil  19476  ufildr  19479  elfm2  19496  elfm3  19498  rnelfm  19501  fmfnfmlem4  19505  fmco  19509  flimtopon  19518  flimopn  19523  fbflim2  19525  flimrest  19531  flffbas  19543  cnpflf  19549  fclstopon  19560  fclsnei  19567  fclsbas  19569  fclsfnflim  19575  fclscmp  19578  ufilcmp  19580  isfcf  19582  fcfnei  19583  cnpfcf  19589  alexsubb  19593  alexsubALT  19598  cldsubg  19656  tgphaus  19662  tgpt0  19664  tsmsgsum  19684  tsmsgsumOLD  19687  tsmsresOLD  19692  tsmsres  19693  xbln0  19964  blssexps  19976  blssex  19977  isxms2  19998  prdsbl  20041  neibl  20051  metss  20058  met2ndc  20073  metrest  20074  metcnp3  20090  nmoeq0  20290  xrsxmet  20361  reconn  20380  iccpnfcnv  20491  fgcfil  20757  iscau4  20765  cfilres  20782  iunmbl2  21013  ismbf3d  21107  mbfaddlem  21113  i1faddlem  21146  i1fmullem  21147  ellimc3  21329  tdeglem4  21504  deg1nn0clb  21536  deg1lt0  21537  dvdsq1p  21607  plypf1  21655  0dgrb  21689  plymul0or  21722  ulmshft  21830  ulmcaulem  21834  ulmcau  21835  cosord  21963  eff1olem  21979  lognegb  22013  eflogeq  22025  logdivlt  22045  efopn  22078  cxpeq0  22098  cxpeq  22170  angpieqvd  22201  dcubic  22216  asinsinb  22267  acoscosb  22268  atantanb  22294  rlimcnp  22334  isppw  22427  isppw2  22428  vmappw  22429  isnsqf  22448  ppieq0  22489  fsumdvdsdiag  22499  dvdsppwf1o  22501  fsumfldivdiag  22505  chpeq0  22522  chteq0  22523  dchrptlem1  22578  lgsdir2lem4  22640  lgsne0  22647  lgsqr  22660  lgsdchrval  22661  lgsquadlem1  22668  m1lgs  22676  brbtwn  23096  brcgr  23097  brbtwn2  23102  axcontlem7  23167  ausisusgra  23230  nbgraf1olem5  23305  edgusgranbfin  23309  nb3graprlem1  23310  cusgrarn  23318  nbcusgra  23322  cusgrafilem2  23339  uvtxnbgra  23352  spthonepeq  23437  3v3e3cycl  23502  eupath2lem3  23551  grpoinvf  23678  rngosn3  23864  rngosn4  23865  rngoueqz  23868  rngoridfz  23873  nvmul0or  23983  nvz  24008  diporthcom  24065  ubthlem3  24224  hvmul0or  24378  his6  24452  hial0  24455  hial02  24456  orthcom  24461  normgt0  24480  ocin  24650  occon3  24651  shsel3  24669  shlub  24768  chssoc  24850  h1de2bi  24908  spansncol  24922  elspansn4  24927  spansnss2  24929  sumspansn  25003  lnopcnbd  25391  lnfncnbd  25412  riesz1  25420  elpjrn  25545  cvcon3  25639  dmdmd  25655  dmdbr3  25660  dmdbr4  25661  dmdbr5  25663  mdslmd1i  25684  atcveq0  25703  chcv1  25710  atssma  25733  atcv0eq  25734  atcv1  25735  bian1d  25802  relfi  25891  br8d  25893  fcobij  25976  resf1o  25981  fpwrelmapffslem  25983  fpwrelmap  25984  xaddeq0  25997  eliccelico  26018  elicoelioo  26019  isarchiofld  26236  pstmfval  26275  unitdivcld  26283  prsdm  26296  prsrn  26297  xrge0iifcnv  26315  lmxrge0  26334  indf1ofs  26434  eulerpartlemgh  26713  dstfrvunirn  26809  cvmliftmolem2  27123  cvmlift2lem12  27155  ghomf1olem  27264  climuzcnv  27267  relexpindlem  27292  zprod  27401  fprod  27405  br8  27517  br6  27518  br4  27519  funbreq  27533  fprb  27535  axext4dist  27565  nodenselem8  27780  dfrdg4  27932  cgrcom  27972  cgrcoml  27978  cgrdegen  27986  btwncom  27996  brsegle  28090  brsegle2  28091  colinbtwnle  28100  btwnoutside  28107  broutsideof3  28108  outsidele  28114  lineunray  28129  lineelsb2  28130  elhf2  28164  ontgval  28229  ordtop  28234  ordcmp  28245  nndivsub  28255  wl-lem-exsb  28342  wl-mo3t  28350  wl-ax11-lem1  28354  cnambfre  28393  itg2addnc  28399  elicc3  28465  nn0prpwlem  28470  opnbnd  28473  cldbnd  28474  opnregcld  28478  cldregopn  28479  fnessref  28518  refssfne  28519  locfincmp  28529  neibastop2  28535  fnemeet2  28541  fnejoin2  28543  fgmin  28544  brabg2  28562  istotbnd3  28623  sstotbnd2  28626  sstotbnd  28627  sstotbnd3  28628  ssbnd  28640  ismtybnd  28659  reheibor  28691  grpoeqdivid  28699  grpokerinj  28703  1idl  28779  0rngo  28780  divrngidl  28781  igenval2  28819  ispridlc  28823  isdmn3  28827  prtlem10  28963  prter2  28979  elrfi  28983  diophrw  29050  eldioph2b  29054  diophin  29064  rexrabdioph  29085  rmxycomplete  29211  coprmdvdsb  29283  jm2.19  29295  jm2.26  29304  jm2.27  29310  limsuc2  29346  dgraa0p  29459  rngunsnply  29483  fiuneneq  29515  hashgcdlem  29518  dvconstbi  29561  expgrowth  29562  axc11next  29613  pm14.24  29639  sbiota1  29641  sigarcol  29853  rexsb  29945  2reu2  29964  ralbinrald  29976  rlimdmafv  30036  ralxfrd2  30090  2ffzoeq  30167  reuccats1  30214  uvtxnb  30231  usgra2pth  30254  wlkiswwlk  30285  wlklniswwlkn  30288  wwlknextbi  30310  wwlknredwwlkn0  30312  wwlkextwrd  30313  el2wlkonot  30341  el2spthonot  30342  el2wlkonotot0  30344  el2wlksotot  30354  usg2wlkonot  30355  usg2spthonot  30360  usg2spthonot0  30361  0clwlk  30381  clwlkisclwwlklem0  30403  scshwfzeqfzo  30445  nbhashuvtx  30487  uvtxhashnb  30488  0eusgraiff0rgra  30505  cusgraiffrusgra  30506  wwlkextprop  30516  frgra3vlem2  30546  frgrancvvdeqlem3  30578  numclwwlkun  30625  fmptsnd  30674  ssnn0fi  30697  0rngnnzr  30729  domnmsuppn0  30733  mat1dimelbas  30790  lindslininds  30887  snlindsntor  30894  isldepslvec2  30908  sbcim2g  31132  sineq0ALT  31560  bnj145OLD  31605  bj-iftru  31974  bj-iffal  31975  bj-cbv2hv  32087  bj-dral1v  32118  bj-sbftv  32137  bj-sb56  32141  bj-equsal1t  32186  bj-19.21t  32194  bj-ceqsalt0  32233  bj-ceqsalt1  32234  bj-xpnzexb  32300  bj-finsumval0  32426  bj-lsub  32433  bj-ldiv  32436  bj-bary1  32443  lshpinN  32474  lsatcveq0  32517  lsatcv0eq  32532  lsatcv1  32533  islshpcv  32538  lkr0f  32579  lkrshp4  32593  lshpkrlem1  32595  lshpset2N  32604  lfl1dim  32606  lfl1dim2N  32607  lub0N  32674  glb0N  32678  oplecon3b  32685  cmtcomN  32734  cmtbr3N  32739  cmtbr4N  32740  cvrnbtwn2  32760  cvrnbtwn3  32761  cvrcon3b  32762  cvrnbtwn4  32764  cvrcmp  32768  atcvreq0  32799  atnle  32802  atlatle  32805  cvlexchb1  32815  cvlcvr1  32824  hlrelat2  32887  exatleN  32888  cvrval3  32897  cvrval4N  32898  cvrexch  32904  atcvr0eq  32910  lnnat  32911  atcvrj0  32912  atcvrj2b  32916  atltcvr  32919  atbtwn  32930  ps-1  32961  3at  32974  islln2a  33001  llncmp  33006  islpln2a  33032  lplncmp  33046  islvol2aN  33076  4at  33097  lvolcmp  33101  pmaple  33245  lncmp  33267  paddss  33329  llnexchb2lem  33352  2polcon4bN  33402  ispsubcl2N  33431  lhpat3  33530  lautcvr  33576  ltrnid  33619  trlval2  33647  trlatn0  33656  ltrnideq  33659  trlnidatb  33661  cdlemeg49lebilem  34023  trlord  34053  cdlemg1a  34054  cdlemg1cex  34072  tendoid0  34309  dva1dim  34469  cdlemm10N  34603  diarnN  34614  cdlemn  34697  dihlspsnssN  34817  dihatexv  34823  dochkrshp  34871  dochkrshp4  34874  djhlsmcl  34899  lcfl6  34985  lcfl8  34987  lcfrvalsnN  35026  lcfrlem9  35035  mapdval2N  35115  mapdordlem2  35122  mapd1o  35133  mapd0  35150  mapdheq2biN  35215