Theorem impbid 184

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 183	. 2 |- ( ph -> ( ph -> ( ps <-> ch ) ) )
4	3	pm2.43i 45	1 |- ( ph -> ( ps <-> ch ) )

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

This theorem is referenced by:  bicom1  191  impbid1  195  impcon4bid  197  pm5.74  236  imbi1d  309  pm5.501  331  2falsed  341  impbida  806  dedlem0b  920  dedlema  921  dedlemb  922  albi  1570  exbi  1588  equequ1  1692  equequ1OLD  1693  elequ1  1724  elequ2  1726  19.21t  1809  19.23t  1814  19.23tOLD  1834  19.21tOLD  1882  sbequ12  1940  dral1  2022  dral1OLD  2023  cbv2h  2033  ax11b  2048  sbft  2074  sbied  2085  sbequ  2109  sb56  2147  sbal1  2176  exsb  2180  dral1-o  2204  eupickb  2319  eupickbi  2320  2eu2  2335  ceqsalt  2938  ceqex  3026  mob2  3074  reu6  3083  sbciegft  3151  eqsbc3r  3178  csbiebt  3247  sseq1  3329  reupick  3585  reupick2  3587  uneqdifeq  3676  prnebg  3939  disjeq2  4146  disjeq1  4149  disjxiun  4169  disjss3  4171  copsexg  4402  euotd  4417  poeq2  4467  sotric  4489  sotrieq  4490  freq2  4513  seeq1  4514  seeq2  4515  tz7.7  4567  ordtri1  4574  ordtri3  4577  ordelinel  4639  reusv2lem2  4684  reusv2lem3  4685  alxfr  4695  ralxfrd  4696  oneqmin  4744  ordsuc  4753  ordelsuc  4759  ordsucelsuc  4761  ordunisuc2  4783  limsuc  4788  iss  5148  iotaval  5388  funeq  5432  funssres  5452  tz6.12c  5709  fnbrfvb  5726  ssimaex  5747  fvimacnv  5804  elpreima  5809  eldmrexrnb  5836  fsn  5865  fconst2g  5905  fconst5  5908  elunirnALT  5959  f1ocnvfvb  5976  foeqcnvco  5986  f1eqcocnv  5987  fliftfun  5993  soisores  6006  isofr  6021  isose  6022  isopo  6025  isoso  6027  f1oiso2  6031  oprabid  6064  f1opw2  6257  op1steq  6350  rntpos  6451  eusvobj2  6541  smoiso2  6590  seqomlem2  6667  oaord  6749  oawordex  6759  oaordex  6760  omord2  6769  om00  6777  oeord  6790  nnaord  6821  nnmord  6834  nnawordex  6839  nnaordex  6840  erexb  6889  swoord1  6893  swoord2  6894  iiner  6935  eceqoveq  6968  omxpenlem  7168  domtriord  7212  mapxpen  7232  mapunen  7235  ssenen  7240  nneneq  7249  onomeneq  7255  nndomo  7259  fodomfib  7345  f1opwfi  7368  elfiun  7393  suplub2  7422  ordiso2  7440  ordiso  7441  oieu  7464  brwdom2  7497  brwdom3  7506  cantnfreslem  7587  cantnflem1  7601  cardidm  7802  carddom2  7820  pm54.43  7843  pr2ne  7845  acnen  7890  acnen2  7892  alephord  7912  alephinit  7932  dfac5  7965  infdif2  8046  fictb  8081  coflim  8097  fincssdom  8159  fin23lem25  8160  isf32lem9  8197  isf34lem4  8213  fin1a2lem11  8246  axdc3lem2  8287  ficard  8396  fpwwe2lem12  8472  fpwwe2  8474  indpi  8740  nqereq  8768  1idpr  8862  ltapr  8878  leltne  9120  ltlen  9131  ltadd2  9133  ltord1  9509  mul0or  9618  ltmul1  9816  lt2msq  9850  nnsub  9994  nn0sub  10226  zrevaddcl  10277  zltp1le  10281  zdiv  10296  nneo  10309  zeo2  10312  zmax  10527  zbtwnre  10528  qrevaddcl  10552  xrlttri  10688  xrleltne  10694  xralrple  10747  xltneg  10759  xleadd1  10790  xlemul1  10825  supxrunb1  10854  supxrunb2  10855  ioo0  10897  iccid  10917  ico0  10918  ioc0  10919  icc0  10920  difreicc  10984  iccsplit  10985  0fz1  11030  uzsplit  11073  fzm1  11082  fzrevral  11086  elfznelfzob  11148  flge  11169  modid2  11226  seqf1olem1  11317  hashen  11586  hashdom  11608  hashle00  11624  hash2prb  11644  hashtpg  11646  shftlem  11838  shftuz  11839  abslt  12073  absle  12074  rexico  12112  cau3lem  12113  rlim2lt  12246  rlim3  12247  o1lo1  12286  rlimdm  12300  climshft  12325  o1dif  12378  isercolllem2  12414  isercoll  12416  zsum  12467  fsum  12469  fsum00  12532  incexclem  12571  dvdsval2  12810  moddvds  12814  negdvdsb  12821  dvdsnegb  12822  dvdscmulr  12833  dvdsmulcr  12834  dvdssub2  12842  fzo0dvdseq  12857  bitsf1ocnv  12911  sadcaddlem  12924  bitsuz  12941  dvdsgcdb  12999  gcdeq  13007  dvdssqlem  13014  isprm2lem  13041  dvdsprime  13047  dvdsprm  13054  coprm  13055  euclemma  13063  rpexp  13075  prmdiveq  13130  odzdvds  13136  pythagtrip  13163  pc2dvds  13207  pcprmpw2  13210  pcprmpw  13211  vdwapun  13297  ramtcl2  13334  firest  13615  mrieqv2d  13819  isacs2  13833  isssc  13975  setciso  14201  posasymb  14364  pleval2  14377  pltval3  14379  lubid  14394  joinle  14405  meetle  14412  lubun  14505  clatleglb  14508  latdisd  14571  letsr  14627  gsumval2a  14737  frmdss2  14763  isgrpid2  14796  isgrpinv  14810  oddvdsnn0  15137  oddvds  15140  odeq  15143  odeq1  15151  gexdvds  15173  pgpfi  15194  pgpssslw  15203  fislw  15214  sylow3lem2  15217  lsmelvalm  15240  lsmlub  15252  lsmss1b  15254  lsmss2b  15256  efgs1b  15323  cyggenod  15449  cyggexb  15463  dprdfeq0  15535  unitmulclb  15725  dvreq1  15753  drngmul0or  15811  isabvd  15863  issrngd  15904  lssats2  16031  lspsneq0  16043  lsmelval2  16112  lvecvs0or  16135  lspsneq  16149  lspsneu  16150  lidl1el  16244  lidldvgen  16281  isnzr2  16289  rrgeq0  16305  domneq0  16312  znunit  16799  ipeq0  16824  ocvsscon  16857  pjdm2  16893  obselocv  16910  unitg  16987  tgss3  17006  clsval2  17069  isopn3  17085  elcls3  17102  opncldf1  17103  neiint  17123  neips  17132  opnneissb  17133  opnssneib  17134  opnnei  17139  tpnei  17140  opnneiid  17145  restcld  17190  restopnb  17193  tgcn  17270  tgcnp  17271  subbascn  17272  iscnp4  17281  cnpnei  17282  cncls2  17291  cncls  17292  cnntr  17293  lmss  17316  hausnei2  17371  lpcls  17382  ordtt1  17397  cmpsub  17417  tgcmp  17418  1stcelcls  17477  kgencn2  17542  ptpjpre1  17556  upxp  17608  txcn  17611  txlm  17633  tgqtop  17697  kqfvima  17715  isr0  17722  regr1lem2  17725  hmeoopn  17751  hmeocld  17752  ptuncnv  17792  fbunfip  17854  fgss2  17859  ufilb  17891  ufprim  17894  trufil  17895  cfinufil  17913  ufildr  17916  elfm2  17933  elfm3  17935  rnelfm  17938  fmfnfmlem4  17942  fmco  17946  flimtopon  17955  flimopn  17960  fbflim2  17962  flimrest  17968  flffbas  17980  cnpflf  17986  fclstopon  17997  fclsnei  18004  fclsbas  18006  fclsfnflim  18012  fclscmp  18015  ufilcmp  18017  isfcf  18019  fcfnei  18020  cnpfcf  18026  alexsubb  18030  alexsubALT  18035  cldsubg  18093  tgphaus  18099  tgpt0  18101  tsmsgsum  18121  tsmsres  18126  xbln0  18397  blssexps  18409  blssex  18410  isxms2  18431  prdsbl  18474  neibl  18484  metss  18491  met2ndc  18506  metrest  18507  metcnp3  18523  nmoeq0  18723  xrsxmet  18793  reconn  18812  iccpnfcnv  18922  fgcfil  19177  iscau4  19185  cfilres  19202  iunmbl2  19404  ismbf3d  19499  mbfaddlem  19505  i1faddlem  19538  i1fmullem  19539  ellimc3  19719  tdeglem4  19936  deg1nn0clb  19966  deg1lt0  19967  dvdsq1p  20036  plypf1  20084  0dgrb  20118  plymul0or  20151  ulmshft  20259  ulmcaulem  20263  ulmcau  20264  cosord  20387  eff1olem  20403  lognegb  20437  eflogeq  20449  logdivlt  20469  efopn  20502  cxpeq0  20522  cxpeq  20594  angpieqvd  20625  dcubic  20639  asinsinb  20690  acoscosb  20691  atantanb  20717  rlimcnp  20757  isppw  20850  isppw2  20851  vmappw  20852  isnsqf  20871  ppieq0  20912  fsumdvdsdiag  20922  dvdsppwf1o  20924  fsumfldivdiag  20928  chpeq0  20945  chteq0  20946  dchrptlem1  21001  lgsdir2lem4  21063  lgsne0  21070  lgsqr  21083  lgsdchrval  21084  lgsquadlem1  21091  m1lgs  21099  ausisusgra  21333  nbgraf1olem5  21408  edgusgranbfin  21412  nb3graprlem1  21413  cusgrarn  21421  nbcusgra  21425  cusgrafilem2  21442  uvtxnbgra  21455  spthonepeq  21540  3v3e3cycl  21605  eupath2lem3  21654  grpoinvf  21781  rngosn3  21967  rngosn4  21968  rngoueqz  21971  rngoridfz  21976  nvmul0or  22086  nvz  22111  diporthcom  22168  ubthlem3  22327  hvmul0or  22480  his6  22554  hial0  22557  hial02  22558  orthcom  22563  normgt0  22582  ocin  22751  occon3  22752  shsel3  22770  shlub  22869  chssoc  22951  h1de2bi  23009  spansncol  23023  elspansn4  23028  spansnss2  23030  sumspansn  23104  lnopcnbd  23492  lnfncnbd  23513  riesz1  23521  elpjrn  23646  cvcon3  23740  dmdmd  23756  dmdbr3  23761  dmdbr4  23762  dmdbr5  23764  mdslmd1i  23785  atcveq0  23804  chcv1  23811  atssma  23834  atcv0eq  23835  atcv1  23836  bian1d  23903  xaddeq0  24072  eliccelico  24093  elicoelioo  24094  pstmfval  24244  unitdivcld  24252  xrge0iifcnv  24272  lmxrge0  24290  indf1ofs  24376  dstfrvunirn  24685  cvmliftmolem2  24922  cvmlift2lem12  24954  ghomf1olem  25058  climuzcnv  25061  relexpindlem  25092  mulge0b  25144  zprod  25216  fprod  25220  br8  25327  br6  25328  br4  25329  funbreq  25341  fprb  25343  axext4dist  25371  nodenselem8  25556  dfrdg4  25703  brbtwn  25742  brcgr  25743  brbtwn2  25748  axcontlem7  25813  cgrcom  25828  cgrcoml  25834  cgrdegen  25842  btwncom  25852  brsegle  25946  brsegle2  25947  colinbtwnle  25956  btwnoutside  25963  broutsideof3  25964  outsidele  25970  lineunray  25985  lineelsb2  25986  elhf2  26020  ontgval  26085  ordtop  26090  ordcmp  26101  nndivsub  26111  wl-bibi1  26127  cnambfre  26154  itg2addnc  26158  elicc3  26210  nn0prpwlem  26215  opnbnd  26218  cldbnd  26219  opnregcld  26223  cldregopn  26224  fnessref  26263  refssfne  26264  locfincmp  26274  neibastop2  26280  fnemeet2  26286  fnejoin2  26288  fgmin  26289  brabg2  26307  istotbnd3  26370  sstotbnd2  26373  sstotbnd  26374  sstotbnd3  26375  ssbnd  26387  ismtybnd  26406  reheibor  26438  grpoeqdivid  26446  grpokerinj  26450  1idl  26526  0rngo  26527  divrngidl  26528  igenval2  26566  ispridlc  26570  isdmn3  26574  prtlem10  26604  prter2  26620  ralxpmap  26632  elrfi  26638  diophrw  26707  eldioph2b  26711  diophin  26721  rexrabdioph  26744  rmxycomplete  26870  coprmdvdsb  26942  jm2.19  26954  jm2.26  26963  jm2.27  26969  limsuc2  27005  islinds4  27173  dgraa0p  27222  rngunsnply  27246  fiuneneq  27381  hashgcdlem  27384  dvconstbi  27419  expgrowth  27420  ax10ext  27474  pm14.24  27500  sbiota1  27502  sigarcol  27721  rexsb  27813  2reu2  27832  ralbinrald  27844  rlimdmafv  27908  euhash1  27998  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  el2wlkonotot0  28069  el2wlksotot  28079  usg2wlkonot  28080  usg2spthonot  28085  usg2spthonot0  28086  frgra3vlem2  28105  frgrancvvdeqlem3  28135  sbcim2g  28334  bnj145  28800  dral1NEW7  29199  cbv2hwAUX7  29219  sbiedNEW7  29244  sbftNEW7  29260  sbequNEW7  29283  sb56NEW7  29297  exsbNEW7  29300  sbal1NEW7  29316  ax11bNEW7  29323  cbv2hOLD7  29405  lubunNEW  29456  lshpinN  29472  lsatcveq0  29515  lsatcv0eq  29530  lsatcv1  29531  islshpcv  29536  lkr0f  29577  lkrshp4  29591  lshpkrlem1  29593  lshpset2N  29602  lfl1dim  29604  lfl1dim2N  29605  lub0N  29672  glb0N  29676  oplecon3b  29683  cmtcomN  29732  cmtbr3N  29737  cmtbr4N  29738  cvrnbtwn2  29758  cvrnbtwn3  29759  cvrcon3b  29760  cvrnbtwn4  29762  cvrcmp  29766  atcvreq0  29797  atnle  29800  atlatle  29803  cvlexchb1  29813  cvlcvr1  29822  hlrelat2  29885  exatleN  29886  cvrval3  29895  cvrval4N  29896  cvrexch  29902  atcvr0eq  29908  lnnat  29909  atcvrj0  29910  atcvrj2b  29914  atltcvr  29917  atbtwn  29928  ps-1  29959  3at  29972  islln2a  29999  llncmp  30004  islpln2a  30030  lplncmp  30044  islvol2aN  30074  4at  30095  lvolcmp  30099  pmaple  30243  lncmp  30265  paddss  30327  llnexchb2lem  30350  2polcon4bN  30400  ispsubcl2N  30429  lhpat3  30528  lautcvr  30574  ltrnid  30617  trlval2  30645  trlatn0  30654  ltrnideq  30657  trlnidatb  30659  cdlemeg49lebilem  31021  trlord  31051  cdlemg1a  31052  cdlemg1cex  31070  tendoid0  31307  dva1dim  31467  cdlemm10N  31601  diarnN  31612  cdlemn  31695  dihlspsnssN  31815  dihatexv  31821  dochkrshp  31869  dochkrshp4  31872  djhlsmcl  31897  lcfl6  31983  lcfl8  31985  lcfrvalsnN  32024  lcfrlem9  32033  mapdval2N  32113  mapdordlem2  32120  mapd1o  32131  mapd0  32148  mapdheq2biN  32213

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178