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  828  dedlem0b  944  dedlema  945  dedlemb  946  albi  1610  exbi  1634  equequ1  1738  elequ1  1761  elequ2  1763  19.21t  1843  19.23t  1847  sbequ12  1948  cbv2h  1978  dral1  2027  dral1ALT  2028  ax12b  2046  sbequ  2077  sbft  2080  sbiedOLD  2113  sb56  2141  sbal1OLD  2181  exsb  2190  dral1-o  2213  eupickb  2353  eupickbOLD  2354  eupickbi  2355  eupickbiOLD  2356  2eu2  2375  eleq2d  2524  hbralbida  2836  ceqsalt  3101  ceqex  3197  mob2  3246  reu6  3255  sbciegft  3325  eqsbc3r  3356  csbiebt  3416  sseq1  3486  reupick  3743  reupick2  3745  uneqdifeq  3876  prnebg  4163  disjeq2  4375  disjeq1  4378  disjxiun  4398  disjss3  4400  reusv2lem2  4603  reusv2lem3  4604  alxfr  4614  ralxfrd  4615  copsexg  4685  copsexgOLD  4686  euotd  4701  poeq2  4754  sotric  4776  sotrieq  4777  freq2  4800  seeq1  4801  seeq2  4802  tz7.7  4854  ordtri1  4861  ordtri3  4864  ordelinel  4926  iss  5263  iotaval  5501  funeq  5546  funssres  5567  f0dom0  5704  tz6.12c  5819  fnbrfvb  5842  ssimaex  5866  fvimacnv  5928  elpreima  5933  eldmrexrnb  5960  fsn  5991  fnsnb  6008  fmptsng  6010  fconst2g  6042  fconst5  6045  elunirn  6078  f1ocnvfvb  6096  foeqcnvco  6108  f1eqcocnv  6109  fliftfun  6115  soisores  6128  isofr  6143  isose  6144  isopo  6147  isoso  6149  f1oiso2  6153  eusvobj2  6194  oprabid  6225  f1opw2  6424  oneqmin  6527  ordsuc  6536  ordelsuc  6542  ordsucelsuc  6544  ordunisuc2  6566  limsuc  6571  f1ovv  6659  op1steq  6729  extmptsuppeq  6824  rntpos  6869  smoiso2  6941  seqomlem2  7017  oaord  7097  oawordex  7107  oaordex  7108  omord2  7117  om00  7125  oeord  7138  nnaord  7169  nnmord  7182  nnawordex  7187  nnaordex  7188  erexb  7237  swoord1  7241  swoord2  7242  iiner  7283  eceqoveq  7316  ralxpmap  7373  omxpenlem  7523  domtriord  7568  mapxpen  7588  mapunen  7591  ssenen  7596  nneneq  7605  onomeneq  7612  nndomo  7616  fodomfib  7703  f1opwfi  7727  fsuppunbi  7753  elfiun  7792  suplub2  7823  ordiso2  7841  ordiso  7842  oieu  7865  brwdom2  7900  brwdom3  7909  cantnflem1  8009  cantnflem1OLD  8032  cardidm  8241  carddom2  8259  pm54.43  8282  pr2ne  8284  acnen  8335  acnen2  8337  alephord  8357  alephinit  8377  dfac5  8410  infdif2  8491  fictb  8526  coflim  8542  fincssdom  8604  fin23lem25  8605  isf32lem9  8642  isf34lem4  8658  fin1a2lem11  8691  axdc3lem2  8732  ficard  8841  fpwwe2lem12  8920  fpwwe2  8922  indpi  9188  nqereq  9216  1idpr  9310  ltapr  9326  leltne  9576  ltlen  9588  ltadd2  9590  ltord1  9978  mul0or  10088  ltmul1  10291  mulge0b  10311  lt2msq  10328  nnsub  10472  nn0sub  10742  zrevaddcl  10802  zltp1le  10806  zdiv  10824  nneo  10837  zeo2  10840  zmax  11062  zbtwnre  11063  qrevaddcl  11087  xrlttri  11228  xrleltne  11234  xralrple  11287  xltneg  11299  xleadd1  11330  xlemul1  11365  supxrunb1  11394  supxrunb2  11395  ioo0  11437  iccid  11457  ico0  11458  ioc0  11459  icc0  11460  difreicc  11535  iccsplit  11536  0fz1  11587  uzsplit  11648  fzm1  11658  fzrevral  11662  ssfzo12bi  11740  elfznelfzob  11749  flge  11773  modid2  11853  seqf1olem1  11963  hashen  12236  hashdom  12261  hashle00  12277  euhash1  12291  hash2prb  12299  pr2pwpr  12302  hashtpg  12305  ccats1swrdeqbi  12508  repsdf2  12535  shftlem  12676  shftuz  12677  abslt  12921  absle  12922  rexico  12960  cau3lem  12961  rlim2lt  13094  rlim3  13095  o1lo1  13134  rlimdm  13148  climshft  13173  o1dif  13226  isercolllem2  13262  isercoll  13264  zsum  13314  fsum  13316  fsum00  13380  incexclem  13418  dvdsval2  13657  moddvds  13661  negdvdsb  13668  dvdsnegb  13669  dvdscmulr  13680  dvdsmulcr  13681  dvdssub2  13689  fzo0dvdseq  13705  bitsf1ocnv  13759  sadcaddlem  13772  bitsuz  13789  dvdsgcdb  13847  gcdeq  13855  dvdssqlem  13862  isprm2lem  13889  dvdsprime  13895  dvdsprm  13904  coprm  13905  euclemma  13913  rpexp  13925  prmdiveq  13980  odzdvds  13986  pythagtrip  14020  pc2dvds  14064  pcprmpw2  14067  pcprmpw  14068  vdwapun  14154  ramtcl2  14191  firest  14491  mrieqv2d  14697  isacs2  14711  isssc  14853  setciso  15079  posasymb  15242  pleval2  15255  pltval3  15257  lublecllem  15278  joinle  15304  meetle  15318  lubun  15413  clatleglb  15416  latdisd  15480  letsr  15517  gsumval2a  15632  frmdss2  15661  isgrpid2  15694  isgrpinv  15708  symg1bas  16021  oddvdsnn0  16169  oddvds  16172  odeq  16175  odeq1  16183  gexdvds  16205  pgpfi  16226  pgpssslw  16235  fislw  16246  sylow3lem2  16249  lsmelvalm  16272  lsmlub  16284  lsmss1b  16286  lsmss2b  16288  efgs1b  16355  cyggenod  16483  cyggexb  16497  dprdfeq0  16635  dprdfeq0OLD  16642  unitmulclb  16881  dvreq1  16909  f1rhm0to0  16952  f1rhm0to0ALT  16953  drngmul0or  16977  isabvd  17029  issrngd  17070  lssats2  17205  lspsneq0  17217  lsmelval2  17290  lvecvs0or  17313  lspsneq  17327  lspsneu  17328  lidl1el  17424  lidldvgen  17461  isnzr2  17469  rrgeq0  17485  domneq0  17493  znunit  18122  psgndif  18158  ipeq0  18193  ocvsscon  18226  pjdm2  18262  obselocv  18279  islinds4  18390  cramer  18630  unitg  18705  tgss3  18724  clsval2  18787  isopn3  18803  elcls3  18820  opncldf1  18821  neiint  18841  neips  18850  opnneissb  18851  opnssneib  18852  opnnei  18857  tpnei  18858  opnneiid  18863  restcld  18909  restopnb  18912  tgcn  18989  tgcnp  18990  subbascn  18991  iscnp4  19000  cnpnei  19001  cncls2  19010  cncls  19011  cnntr  19012  lmss  19035  hausnei2  19090  lpcls  19101  ordtt1  19116  cmpsub  19136  tgcmp  19137  1stcelcls  19198  kgencn2  19263  ptpjpre1  19277  upxp  19329  txcn  19332  txlm  19354  tgqtop  19418  kqfvima  19436  isr0  19443  regr1lem2  19446  hmeoopn  19472  hmeocld  19473  ptuncnv  19513  fbunfip  19575  fgss2  19580  ufilb  19612  ufprim  19615  trufil  19616  cfinufil  19634  ufildr  19637  elfm2  19654  elfm3  19656  rnelfm  19659  fmfnfmlem4  19663  fmco  19667  flimtopon  19676  flimopn  19681  fbflim2  19683  flimrest  19689  flffbas  19701  cnpflf  19707  fclstopon  19718  fclsnei  19725  fclsbas  19727  fclsfnflim  19733  fclscmp  19736  ufilcmp  19738  isfcf  19740  fcfnei  19741  cnpfcf  19747  alexsubb  19751  alexsubALT  19756  cldsubg  19814  tgphaus  19820  tgpt0  19822  tsmsgsum  19842  tsmsgsumOLD  19845  tsmsresOLD  19850  tsmsres  19851  xbln0  20122  blssexps  20134  blssex  20135  isxms2  20156  prdsbl  20199  neibl  20209  metss  20216  met2ndc  20231  metrest  20232  metcnp3  20248  nmoeq0  20448  xrsxmet  20519  reconn  20538  iccpnfcnv  20649  fgcfil  20915  iscau4  20923  cfilres  20940  iunmbl2  21172  ismbf3d  21266  mbfaddlem  21272  i1faddlem  21305  i1fmullem  21306  ellimc3  21488  tdeglem4  21663  deg1nn0clb  21695  deg1lt0  21696  dvdsq1p  21766  plypf1  21814  0dgrb  21848  plymul0or  21881  ulmshft  21989  ulmcaulem  21993  ulmcau  21994  cosord  22122  eff1olem  22138  lognegb  22172  eflogeq  22184  logdivlt  22204  efopn  22237  cxpeq0  22257  cxpeq  22329  angpieqvd  22360  dcubic  22375  asinsinb  22426  acoscosb  22427  atantanb  22453  rlimcnp  22493  isppw  22586  isppw2  22587  vmappw  22588  isnsqf  22607  ppieq0  22648  fsumdvdsdiag  22658  dvdsppwf1o  22660  fsumfldivdiag  22664  chpeq0  22681  chteq0  22682  dchrptlem1  22737  lgsdir2lem4  22799  lgsne0  22806  lgsqr  22819  lgsdchrval  22820  lgsquadlem1  22827  m1lgs  22835  brbtwn  23298  brcgr  23299  brbtwn2  23304  axcontlem7  23369  ausisusgra  23432  nbgraf1olem5  23507  edgusgranbfin  23511  nb3graprlem1  23512  cusgrarn  23520  nbcusgra  23524  cusgrafilem2  23541  uvtxnbgra  23554  spthonepeq  23639  3v3e3cycl  23704  eupath2lem3  23753  grpoinvf  23880  rngosn3  24066  rngosn4  24067  rngoueqz  24070  rngoridfz  24075  nvmul0or  24185  nvz  24210  diporthcom  24267  ubthlem3  24426  hvmul0or  24580  his6  24654  hial0  24657  hial02  24658  orthcom  24663  normgt0  24682  ocin  24852  occon3  24853  shsel3  24871  shlub  24970  chssoc  25052  h1de2bi  25110  spansncol  25124  elspansn4  25129  spansnss2  25131  sumspansn  25205  lnopcnbd  25593  lnfncnbd  25614  riesz1  25622  elpjrn  25747  cvcon3  25841  dmdmd  25857  dmdbr3  25862  dmdbr4  25863  dmdbr5  25865  mdslmd1i  25886  atcveq0  25905  chcv1  25912  atssma  25935  atcv0eq  25936  atcv1  25937  bian1d  26004  relfi  26092  br8d  26094  fcobij  26177  resf1o  26182  fpwrelmapffslem  26184  fpwrelmap  26185  xaddeq0  26198  eliccelico  26213  elicoelioo  26214  isarchiofld  26431  pstmfval  26469  unitdivcld  26477  prsdm  26490  prsrn  26491  xrge0iifcnv  26509  lmxrge0  26528  indf1ofs  26628  eulerpartlemgh  26906  dstfrvunirn  27002  cvmliftmolem2  27316  cvmlift2lem12  27348  ghomf1olem  27458  climuzcnv  27461  relexpindlem  27486  zprod  27595  fprod  27599  br8  27711  br6  27712  br4  27713  funbreq  27727  fprb  27729  axext4dist  27759  nodenselem8  27974  dfrdg4  28126  cgrcom  28166  cgrcoml  28172  cgrdegen  28180  btwncom  28190  brsegle  28284  brsegle2  28285  colinbtwnle  28294  btwnoutside  28301  broutsideof3  28302  outsidele  28308  lineunray  28323  lineelsb2  28324  elhf2  28358  ontgval  28422  ordtop  28427  ordcmp  28438  nndivsub  28448  wl-lem-exsb  28540  wl-mo3t  28546  wl-ax11-lem1  28550  cnambfre  28589  itg2addnc  28595  elicc3  28661  nn0prpwlem  28666  opnbnd  28669  cldbnd  28670  opnregcld  28674  cldregopn  28675  fnessref  28714  refssfne  28715  locfincmp  28725  neibastop2  28731  fnemeet2  28737  fnejoin2  28739  fgmin  28740  brabg2  28758  istotbnd3  28819  sstotbnd2  28822  sstotbnd  28823  sstotbnd3  28824  ssbnd  28836  ismtybnd  28855  reheibor  28887  grpoeqdivid  28895  grpokerinj  28899  1idl  28975  0rngo  28976  divrngidl  28977  igenval2  29015  ispridlc  29019  isdmn3  29023  prtlem10  29159  prter2  29175  elrfi  29179  diophrw  29246  eldioph2b  29250  diophin  29260  rexrabdioph  29281  rmxycomplete  29407  coprmdvdsb  29479  jm2.19  29491  jm2.26  29500  jm2.27  29506  limsuc2  29542  dgraa0p  29655  rngunsnply  29679  fiuneneq  29711  hashgcdlem  29714  dvconstbi  29757  expgrowth  29758  axc11next  29809  pm14.24  29835  sbiota1  29837  sigarcol  30049  rexsb  30141  2reu2  30160  ralbinrald  30172  rlimdmafv  30232  ralxfrd2  30286  2ffzoeq  30363  reuccats1  30410  uvtxnb  30427  usgra2pth  30450  wlkiswwlk  30481  wlklniswwlkn  30484  wwlknextbi  30506  wwlknredwwlkn0  30508  wwlkextwrd  30509  el2wlkonot  30537  el2spthonot  30538  el2wlkonotot0  30540  el2wlksotot  30550  usg2wlkonot  30551  usg2spthonot  30556  usg2spthonot0  30557  0clwlk  30577  clwlkisclwwlklem0  30599  scshwfzeqfzo  30641  nbhashuvtx  30683  uvtxhashnb  30684  0eusgraiff0rgra  30701  cusgraiffrusgra  30702  wwlkextprop  30712  frgra3vlem2  30742  frgrancvvdeqlem3  30774  numclwwlkun  30821  fmptsnd  30871  ssnn0fi  30895  0rngnnzr  30927  domnmsuppn0  30931  ply1coe1eq  30990  cply1coe0bi  31005  scmatscmidbi  31026  scmatscmids  31027  mat1dimelbas  31034  lindslininds  31131  snlindsntor  31138  isldepslvec2  31152  sbcim2g  31578  sineq0ALT  32006  bnj145OLD  32051  bj-iftru  32422  bj-iffal  32423  bj-cbv2hv  32563  bj-dral1v  32594  bj-sbftv  32613  bj-sb56  32617  bj-equsal1t  32663  bj-19.21t  32671  bj-ceqsalt0  32717  bj-ceqsalt1  32718  bj-xpnzexb  32786  bj-finsumval0  32922  bj-lsub  32930  bj-ldiv  32933  bj-bary1  32940  lshpinN  32973  lsatcveq0  33016  lsatcv0eq  33031  lsatcv1  33032  islshpcv  33037  lkr0f  33078  lkrshp4  33092  lshpkrlem1  33094  lshpset2N  33103  lfl1dim  33105  lfl1dim2N  33106  lub0N  33173  glb0N  33177  oplecon3b  33184  cmtcomN  33233  cmtbr3N  33238  cmtbr4N  33239  cvrnbtwn2  33259  cvrnbtwn3  33260  cvrcon3b  33261  cvrnbtwn4  33263  cvrcmp  33267  atcvreq0  33298  atnle  33301  atlatle  33304  cvlexchb1  33314  cvlcvr1  33323  hlrelat2  33386  exatleN  33387  cvrval3  33396  cvrval4N  33397  cvrexch  33403  atcvr0eq  33409  lnnat  33410  atcvrj0  33411  atcvrj2b  33415  atltcvr  33418  atbtwn  33429  ps-1  33460  3at  33473  islln2a  33500  llncmp  33505  islpln2a  33531  lplncmp  33545  islvol2aN  33575  4at  33596  lvolcmp  33600  pmaple  33744  lncmp  33766  paddss  33828  llnexchb2lem  33851  2polcon4bN  33901  ispsubcl2N  33930  lhpat3  34029  lautcvr  34075  ltrnid  34118  trlval2  34146  trlatn0  34155  ltrnideq  34158  trlnidatb  34160  cdlemeg49lebilem  34522  trlord  34552  cdlemg1a  34553  cdlemg1cex  34571  tendoid0  34808  dva1dim  34968  cdlemm10N  35102  diarnN  35113  cdlemn  35196  dihlspsnssN  35316  dihatexv  35322  dochkrshp  35370  dochkrshp4  35373  djhlsmcl  35398  lcfl6  35484  lcfl8  35486  lcfrvalsnN  35525  lcfrlem9  35534  mapdval2N  35614  mapdordlem2  35621  mapd1o  35632  mapd0  35649  mapdheq2biN  35714