Theorem impbid 191

Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-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  821  dedlem0b  937  dedlema  938  dedlemb  939  albi  1612  exbi  1633  equequ1  1735  elequ1  1758  elequ2  1760  19.21t  1836  19.23t  1840  sbequ12  1935  cbv2h  1965  dral1  2016  dral1ALT  2017  ax12b  2035  sbequ  2064  sbft  2067  sbiedOLD  2101  sb56  2134  sbal1OLD  2174  exsb  2182  dral1-o  2205  eupickb  2340  eupickbOLD  2341  eupickbi  2342  eupickbiOLD  2343  2eu2  2359  ceqsalt  2985  ceqex  3079  mob2  3128  reu6  3137  sbciegft  3205  eqsbc3r  3236  csbiebt  3296  sseq1  3365  reupick  3622  reupick2  3624  uneqdifeq  3755  prnebg  4042  disjeq2  4254  disjeq1  4257  disjxiun  4277  disjss3  4279  reusv2lem2  4482  reusv2lem3  4483  alxfr  4493  ralxfrd  4494  copsexg  4564  copsexgOLD  4565  euotd  4580  poeq2  4632  sotric  4654  sotrieq  4655  freq2  4678  seeq1  4679  seeq2  4680  tz7.7  4732  ordtri1  4739  ordtri3  4742  ordelinel  4804  iss  5142  iotaval  5380  funeq  5425  funssres  5446  f0dom0  5583  tz6.12c  5697  fnbrfvb  5720  ssimaex  5744  fvimacnv  5806  elpreima  5811  eldmrexrnb  5838  fsn  5868  fnsnb  5885  fmptsng  5887  fconst2g  5919  fconst5  5922  elunirnALT  5957  f1ocnvfvb  5973  foeqcnvco  5985  f1eqcocnv  5986  fliftfun  5992  soisores  6005  isofr  6020  isose  6021  isopo  6024  isoso  6026  f1oiso2  6030  eusvobj2  6072  oprabid  6104  f1opw2  6302  oneqmin  6405  ordsuc  6414  ordelsuc  6420  ordsucelsuc  6422  ordunisuc2  6444  limsuc  6449  f1ovv  6537  op1steq  6607  extmptsuppeq  6702  rntpos  6747  smoiso2  6816  seqomlem2  6892  oaord  6974  oawordex  6984  oaordex  6985  omord2  6994  om00  7002  oeord  7015  nnaord  7046  nnmord  7059  nnawordex  7064  nnaordex  7065  erexb  7114  swoord1  7118  swoord2  7119  iiner  7160  eceqoveq  7193  ralxpmap  7250  omxpenlem  7400  domtriord  7445  mapxpen  7465  mapunen  7468  ssenen  7473  nneneq  7482  onomeneq  7488  nndomo  7492  fodomfib  7579  f1opwfi  7603  fsuppunbi  7629  elfiun  7668  suplub2  7699  ordiso2  7717  ordiso  7718  oieu  7741  brwdom2  7776  brwdom3  7785  cantnflem1  7885  cantnflem1OLD  7908  cardidm  8117  carddom2  8135  pm54.43  8158  pr2ne  8160  acnen  8211  acnen2  8213  alephord  8233  alephinit  8253  dfac5  8286  infdif2  8367  fictb  8402  coflim  8418  fincssdom  8480  fin23lem25  8481  isf32lem9  8518  isf34lem4  8534  fin1a2lem11  8567  axdc3lem2  8608  ficard  8717  fpwwe2lem12  8796  fpwwe2  8798  indpi  9064  nqereq  9092  1idpr  9186  ltapr  9202  leltne  9452  ltlen  9464  ltadd2  9466  ltord1  9854  mul0or  9964  ltmul1  10167  mulge0b  10187  lt2msq  10204  nnsub  10348  nn0sub  10618  zrevaddcl  10678  zltp1le  10682  zdiv  10700  nneo  10713  zeo2  10716  zmax  10938  zbtwnre  10939  qrevaddcl  10963  xrlttri  11104  xrleltne  11110  xralrple  11163  xltneg  11175  xleadd1  11206  xlemul1  11241  supxrunb1  11270  supxrunb2  11271  ioo0  11313  iccid  11333  ico0  11334  ioc0  11335  icc0  11336  difreicc  11404  iccsplit  11405  0fz1  11456  uzsplit  11514  fzm1  11524  fzrevral  11528  ssfzo12bi  11606  elfznelfzob  11615  flge  11639  modid2  11719  seqf1olem1  11829  hashen  12102  hashdom  12126  hashle00  12142  euhash1  12156  hash2prb  12164  pr2pwpr  12167  hashtpg  12170  ccats1swrdeqbi  12373  repsdf2  12400  shftlem  12541  shftuz  12542  abslt  12786  absle  12787  rexico  12825  cau3lem  12826  rlim2lt  12959  rlim3  12960  o1lo1  12999  rlimdm  13013  climshft  13038  o1dif  13091  isercolllem2  13127  isercoll  13129  zsum  13179  fsum  13181  fsum00  13244  incexclem  13282  dvdsval2  13521  moddvds  13525  negdvdsb  13532  dvdsnegb  13533  dvdscmulr  13544  dvdsmulcr  13545  dvdssub2  13553  fzo0dvdseq  13569  bitsf1ocnv  13623  sadcaddlem  13636  bitsuz  13653  dvdsgcdb  13711  gcdeq  13719  dvdssqlem  13726  isprm2lem  13753  dvdsprime  13759  dvdsprm  13768  coprm  13769  euclemma  13777  rpexp  13789  prmdiveq  13844  odzdvds  13850  pythagtrip  13884  pc2dvds  13928  pcprmpw2  13931  pcprmpw  13932  vdwapun  14018  ramtcl2  14055  firest  14354  mrieqv2d  14560  isacs2  14574  isssc  14716  setciso  14942  posasymb  15105  pleval2  15118  pltval3  15120  lublecllem  15141  joinle  15167  meetle  15181  lubun  15276  clatleglb  15279  latdisd  15343  letsr  15380  gsumval2a  15492  frmdss2  15521  isgrpid2  15554  isgrpinv  15568  symg1bas  15881  oddvdsnn0  16027  oddvds  16030  odeq  16033  odeq1  16041  gexdvds  16063  pgpfi  16084  pgpssslw  16093  fislw  16104  sylow3lem2  16107  lsmelvalm  16130  lsmlub  16142  lsmss1b  16144  lsmss2b  16146  efgs1b  16213  cyggenod  16341  cyggexb  16355  dprdfeq0  16486  dprdfeq0OLD  16493  unitmulclb  16691  dvreq1  16719  drngmul0or  16777  isabvd  16829  issrngd  16870  lssats2  17003  lspsneq0  17015  lsmelval2  17088  lvecvs0or  17111  lspsneq  17125  lspsneu  17126  lidl1el  17222  lidldvgen  17259  isnzr2  17267  rrgeq0  17283  domneq0  17291  znunit  17838  psgndif  17874  ipeq0  17909  ocvsscon  17942  pjdm2  17978  obselocv  17995  islinds4  18106  cramer  18339  unitg  18414  tgss3  18433  clsval2  18496  isopn3  18512  elcls3  18529  opncldf1  18530  neiint  18550  neips  18559  opnneissb  18560  opnssneib  18561  opnnei  18566  tpnei  18567  opnneiid  18572  restcld  18618  restopnb  18621  tgcn  18698  tgcnp  18699  subbascn  18700  iscnp4  18709  cnpnei  18710  cncls2  18719  cncls  18720  cnntr  18721  lmss  18744  hausnei2  18799  lpcls  18810  ordtt1  18825  cmpsub  18845  tgcmp  18846  1stcelcls  18907  kgencn2  18972  ptpjpre1  18986  upxp  19038  txcn  19041  txlm  19063  tgqtop  19127  kqfvima  19145  isr0  19152  regr1lem2  19155  hmeoopn  19181  hmeocld  19182  ptuncnv  19222  fbunfip  19284  fgss2  19289  ufilb  19321  ufprim  19324  trufil  19325  cfinufil  19343  ufildr  19346  elfm2  19363  elfm3  19365  rnelfm  19368  fmfnfmlem4  19372  fmco  19376  flimtopon  19385  flimopn  19390  fbflim2  19392  flimrest  19398  flffbas  19410  cnpflf  19416  fclstopon  19427  fclsnei  19434  fclsbas  19436  fclsfnflim  19442  fclscmp  19445  ufilcmp  19447  isfcf  19449  fcfnei  19450  cnpfcf  19456  alexsubb  19460  alexsubALT  19465  cldsubg  19523  tgphaus  19529  tgpt0  19531  tsmsgsum  19551  tsmsgsumOLD  19554  tsmsresOLD  19559  tsmsres  19560  xbln0  19831  blssexps  19843  blssex  19844  isxms2  19865  prdsbl  19908  neibl  19918  metss  19925  met2ndc  19940  metrest  19941  metcnp3  19957  nmoeq0  20157  xrsxmet  20228  reconn  20247  iccpnfcnv  20358  fgcfil  20624  iscau4  20632  cfilres  20649  iunmbl2  20880  ismbf3d  20974  mbfaddlem  20980  i1faddlem  21013  i1fmullem  21014  ellimc3  21196  tdeglem4  21414  deg1nn0clb  21446  deg1lt0  21447  dvdsq1p  21517  plypf1  21565  0dgrb  21599  plymul0or  21632  ulmshft  21740  ulmcaulem  21744  ulmcau  21745  cosord  21873  eff1olem  21889  lognegb  21923  eflogeq  21935  logdivlt  21955  efopn  21988  cxpeq0  22008  cxpeq  22080  angpieqvd  22111  dcubic  22126  asinsinb  22177  acoscosb  22178  atantanb  22204  rlimcnp  22244  isppw  22337  isppw2  22338  vmappw  22339  isnsqf  22358  ppieq0  22399  fsumdvdsdiag  22409  dvdsppwf1o  22411  fsumfldivdiag  22415  chpeq0  22432  chteq0  22433  dchrptlem1  22488  lgsdir2lem4  22550  lgsne0  22557  lgsqr  22570  lgsdchrval  22571  lgsquadlem1  22578  m1lgs  22586  brbtwn  22968  brcgr  22969  brbtwn2  22974  axcontlem7  23039  ausisusgra  23102  nbgraf1olem5  23177  edgusgranbfin  23181  nb3graprlem1  23182  cusgrarn  23190  nbcusgra  23194  cusgrafilem2  23211  uvtxnbgra  23224  spthonepeq  23309  3v3e3cycl  23374  eupath2lem3  23423  grpoinvf  23550  rngosn3  23736  rngosn4  23737  rngoueqz  23740  rngoridfz  23745  nvmul0or  23855  nvz  23880  diporthcom  23937  ubthlem3  24096  hvmul0or  24250  his6  24324  hial0  24327  hial02  24328  orthcom  24333  normgt0  24352  ocin  24522  occon3  24523  shsel3  24541  shlub  24640  chssoc  24722  h1de2bi  24780  spansncol  24794  elspansn4  24799  spansnss2  24801  sumspansn  24875  lnopcnbd  25263  lnfncnbd  25284  riesz1  25292  elpjrn  25417  cvcon3  25511  dmdmd  25527  dmdbr3  25532  dmdbr4  25533  dmdbr5  25535  mdslmd1i  25556  atcveq0  25575  chcv1  25582  atssma  25605  atcv0eq  25606  atcv1  25607  bian1d  25674  relfi  25764  br8d  25766  fcobij  25849  resf1o  25855  fpwrelmapffslem  25857  fpwrelmap  25858  xaddeq0  25871  eliccelico  25890  elicoelioo  25891  isarchiofld  26138  pstmfval  26177  unitdivcld  26185  prsdm  26198  prsrn  26199  xrge0iifcnv  26217  lmxrge0  26236  indf1ofs  26336  eulerpartlemgh  26609  dstfrvunirn  26705  cvmliftmolem2  27019  cvmlift2lem12  27051  ghomf1olem  27160  climuzcnv  27163  relexpindlem  27188  zprod  27297  fprod  27301  br8  27413  br6  27414  br4  27415  funbreq  27429  fprb  27431  axext4dist  27461  nodenselem8  27676  dfrdg4  27828  cgrcom  27868  cgrcoml  27874  cgrdegen  27882  btwncom  27892  brsegle  27986  brsegle2  27987  colinbtwnle  27996  btwnoutside  28003  broutsideof3  28004  outsidele  28010  lineunray  28025  lineelsb2  28026  elhf2  28060  ontgval  28125  ordtop  28130  ordcmp  28141  nndivsub  28151  wl-mo3t  28241  wl-ax11-lem1  28245  cnambfre  28284  itg2addnc  28290  elicc3  28356  nn0prpwlem  28361  opnbnd  28364  cldbnd  28365  opnregcld  28369  cldregopn  28370  fnessref  28409  refssfne  28410  locfincmp  28420  neibastop2  28426  fnemeet2  28432  fnejoin2  28434  fgmin  28435  brabg2  28453  istotbnd3  28514  sstotbnd2  28517  sstotbnd  28518  sstotbnd3  28519  ssbnd  28531  ismtybnd  28550  reheibor  28582  grpoeqdivid  28590  grpokerinj  28594  1idl  28670  0rngo  28671  divrngidl  28672  igenval2  28710  ispridlc  28714  isdmn3  28718  prtlem10  28855  prter2  28871  elrfi  28875  diophrw  28942  eldioph2b  28946  diophin  28956  rexrabdioph  28977  rmxycomplete  29103  coprmdvdsb  29175  jm2.19  29187  jm2.26  29196  jm2.27  29202  limsuc2  29238  dgraa0p  29351  rngunsnply  29375  fiuneneq  29407  hashgcdlem  29410  dvconstbi  29453  expgrowth  29454  axc11next  29505  pm14.24  29531  sbiota1  29533  sigarcol  29746  rexsb  29838  2reu2  29857  ralbinrald  29869  rlimdmafv  29929  ralxfrd2  29983  2ffzoeq  30060  reuccats1  30107  uvtxnb  30124  usgra2pth  30147  wlkiswwlk  30178  wlklniswwlkn  30181  wwlknextbi  30203  wwlknredwwlkn0  30205  wwlkextwrd  30206  el2wlkonot  30234  el2spthonot  30235  el2wlkonotot0  30237  el2wlksotot  30247  usg2wlkonot  30248  usg2spthonot  30253  usg2spthonot0  30254  0clwlk  30274  clwlkisclwwlklem0  30296  scshwfzeqfzo  30338  nbhashuvtx  30380  uvtxhashnb  30381  0eusgraiff0rgra  30398  cusgraiffrusgra  30399  wwlkextprop  30409  frgra3vlem2  30439  frgrancvvdeqlem3  30471  numclwwlkun  30518  fmptsnd  30567  0rngnnzr  30609  domnmsuppn0  30613  lindslininds  30707  snlindsntor  30714  isldepslvec2  30728  sbcim2g  30946  sineq0ALT  31375  bnj145OLD  31420  bj-cbv2hv  31861  bj-dral1v  31892  bj-sbftv  31907  bj-equsal1t  31950  bj-19.21t  31958  bj-ceqsalt  31988  bj-xpnzexb  32036  bj-finsumval0  32159  bj-lsub  32166  bj-ldiv  32169  bj-bary1  32176  lshpinN  32207  lsatcveq0  32250  lsatcv0eq  32265  lsatcv1  32266  islshpcv  32271  lkr0f  32312  lkrshp4  32326  lshpkrlem1  32328  lshpset2N  32337  lfl1dim  32339  lfl1dim2N  32340  lub0N  32407  glb0N  32411  oplecon3b  32418  cmtcomN  32467  cmtbr3N  32472  cmtbr4N  32473  cvrnbtwn2  32493  cvrnbtwn3  32494  cvrcon3b  32495  cvrnbtwn4  32497  cvrcmp  32501  atcvreq0  32532  atnle  32535  atlatle  32538  cvlexchb1  32548  cvlcvr1  32557  hlrelat2  32620  exatleN  32621  cvrval3  32630  cvrval4N  32631  cvrexch  32637  atcvr0eq  32643  lnnat  32644  atcvrj0  32645  atcvrj2b  32649  atltcvr  32652  atbtwn  32663  ps-1  32694  3at  32707  islln2a  32734  llncmp  32739  islpln2a  32765  lplncmp  32779  islvol2aN  32809  4at  32830  lvolcmp  32834  pmaple  32978  lncmp  33000  paddss  33062  llnexchb2lem  33085  2polcon4bN  33135  ispsubcl2N  33164  lhpat3  33263  lautcvr  33309  ltrnid  33352  trlval2  33380  trlatn0  33389  ltrnideq  33392  trlnidatb  33394  cdlemeg49lebilem  33756  trlord  33786  cdlemg1a  33787  cdlemg1cex  33805  tendoid0  34042  dva1dim  34202  cdlemm10N  34336  diarnN  34347  cdlemn  34430  dihlspsnssN  34550  dihatexv  34556  dochkrshp  34604  dochkrshp4  34607  djhlsmcl  34632  lcfl6  34718  lcfl8  34720  lcfrvalsnN  34759  lcfrlem9  34768  mapdval2N  34848  mapdordlem2  34855  mapd1o  34866  mapd0  34883  mapdheq2biN  34948