MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impbid Structured version   Unicode version

Theorem impbid 185
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
StepHypRef Expression
1 impbid.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 impbid.2 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
31, 2impbid21d 184 . 2  |-  ( ph  ->  ( ph  ->  ( ps 
<->  ch ) ) )
43pm2.43i 46 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  bicom1  192  impbid1  196  impcon4bid  198  pm5.74  237  imbi1d  310  pm5.501  332  2falsed  342  impbida  807  dedlem0b  921  dedlema  922  dedlemb  923  albi  1574  exbi  1592  equequ1  1697  equequ1OLD  1698  elequ1  1729  elequ2  1731  19.21t  1814  19.23t  1819  19.23tOLD  1839  19.21tOLD  1887  sbequ12  1945  cbv2h  1980  dral1  2058  dral1OLD  2059  ax11b  2083  sbequ  2113  sbft  2117  sbftOLD  2118  sbied  2151  sb56  2176  sbal1  2205  exsb  2209  dral1-o  2233  eupickb  2348  eupickbi  2349  2eu2  2364  ceqsalt  2980  ceqex  3068  mob2  3116  reu6  3125  sbciegft  3193  eqsbc3r  3220  csbiebt  3289  sseq1  3371  reupick  3627  reupick2  3629  uneqdifeq  3718  prnebg  3981  disjeq2  4189  disjeq1  4192  disjxiun  4212  disjss3  4214  copsexg  4445  euotd  4460  poeq2  4510  sotric  4532  sotrieq  4533  freq2  4556  seeq1  4557  seeq2  4558  tz7.7  4610  ordtri1  4617  ordtri3  4620  ordelinel  4683  reusv2lem2  4728  reusv2lem3  4729  alxfr  4739  ralxfrd  4740  oneqmin  4788  ordsuc  4797  ordelsuc  4803  ordsucelsuc  4805  ordunisuc2  4827  limsuc  4832  iss  5192  iotaval  5432  funeq  5476  funssres  5496  tz6.12c  5753  fnbrfvb  5770  ssimaex  5791  fvimacnv  5848  elpreima  5853  eldmrexrnb  5880  fsn  5909  fconst2g  5949  fconst5  5952  elunirnALT  6003  f1ocnvfvb  6020  foeqcnvco  6030  f1eqcocnv  6031  fliftfun  6037  soisores  6050  isofr  6065  isose  6066  isopo  6069  isoso  6071  f1oiso2  6075  oprabid  6108  f1opw2  6301  op1steq  6394  rntpos  6495  eusvobj2  6585  smoiso2  6634  seqomlem2  6711  oaord  6793  oawordex  6803  oaordex  6804  omord2  6813  om00  6821  oeord  6834  nnaord  6865  nnmord  6878  nnawordex  6883  nnaordex  6884  erexb  6933  swoord1  6937  swoord2  6938  iiner  6979  eceqoveq  7012  omxpenlem  7212  domtriord  7256  mapxpen  7276  mapunen  7279  ssenen  7284  nneneq  7293  onomeneq  7299  nndomo  7303  fodomfib  7389  f1opwfi  7413  elfiun  7438  suplub2  7469  ordiso2  7487  ordiso  7488  oieu  7511  brwdom2  7544  brwdom3  7553  cantnfreslem  7634  cantnflem1  7648  cardidm  7851  carddom2  7869  pm54.43  7892  pr2ne  7894  acnen  7939  acnen2  7941  alephord  7961  alephinit  7981  dfac5  8014  infdif2  8095  fictb  8130  coflim  8146  fincssdom  8208  fin23lem25  8209  isf32lem9  8246  isf34lem4  8262  fin1a2lem11  8295  axdc3lem2  8336  ficard  8445  fpwwe2lem12  8521  fpwwe2  8523  indpi  8789  nqereq  8817  1idpr  8911  ltapr  8927  leltne  9169  ltlen  9180  ltadd2  9182  ltord1  9558  mul0or  9667  ltmul1  9865  lt2msq  9899  nnsub  10043  nn0sub  10275  zrevaddcl  10326  zltp1le  10330  zdiv  10345  nneo  10358  zeo2  10361  zmax  10576  zbtwnre  10577  qrevaddcl  10601  xrlttri  10737  xrleltne  10743  xralrple  10796  xltneg  10808  xleadd1  10839  xlemul1  10874  supxrunb1  10903  supxrunb2  10904  ioo0  10946  iccid  10966  ico0  10967  ioc0  10968  icc0  10969  difreicc  11033  iccsplit  11034  0fz1  11079  uzsplit  11123  fzm1  11132  fzrevral  11136  elfznelfzob  11198  flge  11219  modid2  11276  seqf1olem1  11367  hashen  11636  hashdom  11658  hashle00  11674  hash2prb  11694  hashtpg  11696  shftlem  11888  shftuz  11889  abslt  12123  absle  12124  rexico  12162  cau3lem  12163  rlim2lt  12296  rlim3  12297  o1lo1  12336  rlimdm  12350  climshft  12375  o1dif  12428  isercolllem2  12464  isercoll  12466  zsum  12517  fsum  12519  fsum00  12582  incexclem  12621  dvdsval2  12860  moddvds  12864  negdvdsb  12871  dvdsnegb  12872  dvdscmulr  12883  dvdsmulcr  12884  dvdssub2  12892  fzo0dvdseq  12907  bitsf1ocnv  12961  sadcaddlem  12974  bitsuz  12991  dvdsgcdb  13049  gcdeq  13057  dvdssqlem  13064  isprm2lem  13091  dvdsprime  13097  dvdsprm  13104  coprm  13105  euclemma  13113  rpexp  13125  prmdiveq  13180  odzdvds  13186  pythagtrip  13213  pc2dvds  13257  pcprmpw2  13260  pcprmpw  13261  vdwapun  13347  ramtcl2  13384  firest  13665  mrieqv2d  13869  isacs2  13883  isssc  14025  setciso  14251  posasymb  14414  pleval2  14427  pltval3  14429  lubid  14444  joinle  14455  meetle  14462  lubun  14555  clatleglb  14558  latdisd  14621  letsr  14677  gsumval2a  14787  frmdss2  14813  isgrpid2  14846  isgrpinv  14860  oddvdsnn0  15187  oddvds  15190  odeq  15193  odeq1  15201  gexdvds  15223  pgpfi  15244  pgpssslw  15253  fislw  15264  sylow3lem2  15267  lsmelvalm  15290  lsmlub  15302  lsmss1b  15304  lsmss2b  15306  efgs1b  15373  cyggenod  15499  cyggexb  15513  dprdfeq0  15585  unitmulclb  15775  dvreq1  15803  drngmul0or  15861  isabvd  15913  issrngd  15954  lssats2  16081  lspsneq0  16093  lsmelval2  16162  lvecvs0or  16185  lspsneq  16199  lspsneu  16200  lidl1el  16294  lidldvgen  16331  isnzr2  16339  rrgeq0  16355  domneq0  16362  znunit  16849  ipeq0  16874  ocvsscon  16907  pjdm2  16943  obselocv  16960  unitg  17037  tgss3  17056  clsval2  17119  isopn3  17135  elcls3  17152  opncldf1  17153  neiint  17173  neips  17182  opnneissb  17183  opnssneib  17184  opnnei  17189  tpnei  17190  opnneiid  17195  restcld  17241  restopnb  17244  tgcn  17321  tgcnp  17322  subbascn  17323  iscnp4  17332  cnpnei  17333  cncls2  17342  cncls  17343  cnntr  17344  lmss  17367  hausnei2  17422  lpcls  17433  ordtt1  17448  cmpsub  17468  tgcmp  17469  1stcelcls  17529  kgencn2  17594  ptpjpre1  17608  upxp  17660  txcn  17663  txlm  17685  tgqtop  17749  kqfvima  17767  isr0  17774  regr1lem2  17777  hmeoopn  17803  hmeocld  17804  ptuncnv  17844  fbunfip  17906  fgss2  17911  ufilb  17943  ufprim  17946  trufil  17947  cfinufil  17965  ufildr  17968  elfm2  17985  elfm3  17987  rnelfm  17990  fmfnfmlem4  17994  fmco  17998  flimtopon  18007  flimopn  18012  fbflim2  18014  flimrest  18020  flffbas  18032  cnpflf  18038  fclstopon  18049  fclsnei  18056  fclsbas  18058  fclsfnflim  18064  fclscmp  18067  ufilcmp  18069  isfcf  18071  fcfnei  18072  cnpfcf  18078  alexsubb  18082  alexsubALT  18087  cldsubg  18145  tgphaus  18151  tgpt0  18153  tsmsgsum  18173  tsmsres  18178  xbln0  18449  blssexps  18461  blssex  18462  isxms2  18483  prdsbl  18526  neibl  18536  metss  18543  met2ndc  18558  metrest  18559  metcnp3  18575  nmoeq0  18775  xrsxmet  18845  reconn  18864  iccpnfcnv  18974  fgcfil  19229  iscau4  19237  cfilres  19254  iunmbl2  19456  ismbf3d  19549  mbfaddlem  19555  i1faddlem  19588  i1fmullem  19589  ellimc3  19771  tdeglem4  19988  deg1nn0clb  20018  deg1lt0  20019  dvdsq1p  20088  plypf1  20136  0dgrb  20170  plymul0or  20203  ulmshft  20311  ulmcaulem  20315  ulmcau  20316  cosord  20439  eff1olem  20455  lognegb  20489  eflogeq  20501  logdivlt  20521  efopn  20554  cxpeq0  20574  cxpeq  20646  angpieqvd  20677  dcubic  20691  asinsinb  20742  acoscosb  20743  atantanb  20769  rlimcnp  20809  isppw  20902  isppw2  20903  vmappw  20904  isnsqf  20923  ppieq0  20964  fsumdvdsdiag  20974  dvdsppwf1o  20976  fsumfldivdiag  20980  chpeq0  20997  chteq0  20998  dchrptlem1  21053  lgsdir2lem4  21115  lgsne0  21122  lgsqr  21135  lgsdchrval  21136  lgsquadlem1  21143  m1lgs  21151  ausisusgra  21385  nbgraf1olem5  21460  edgusgranbfin  21464  nb3graprlem1  21465  cusgrarn  21473  nbcusgra  21477  cusgrafilem2  21494  uvtxnbgra  21507  spthonepeq  21592  3v3e3cycl  21657  eupath2lem3  21706  grpoinvf  21833  rngosn3  22019  rngosn4  22020  rngoueqz  22023  rngoridfz  22028  nvmul0or  22138  nvz  22163  diporthcom  22220  ubthlem3  22379  hvmul0or  22532  his6  22606  hial0  22609  hial02  22610  orthcom  22615  normgt0  22634  ocin  22803  occon3  22804  shsel3  22822  shlub  22921  chssoc  23003  h1de2bi  23061  spansncol  23075  elspansn4  23080  spansnss2  23082  sumspansn  23156  lnopcnbd  23544  lnfncnbd  23565  riesz1  23573  elpjrn  23698  cvcon3  23792  dmdmd  23808  dmdbr3  23813  dmdbr4  23814  dmdbr5  23816  mdslmd1i  23837  atcveq0  23856  chcv1  23863  atssma  23886  atcv0eq  23887  atcv1  23888  bian1d  23955  xaddeq0  24124  eliccelico  24145  elicoelioo  24146  pstmfval  24296  unitdivcld  24304  xrge0iifcnv  24324  lmxrge0  24342  indf1ofs  24428  dstfrvunirn  24737  cvmliftmolem2  24974  cvmlift2lem12  25006  ghomf1olem  25110  climuzcnv  25113  relexpindlem  25144  mulge0b  25196  zprod  25268  fprod  25272  br8  25384  br6  25385  br4  25386  funbreq  25400  fprb  25402  axext4dist  25433  nodenselem8  25648  dfrdg4  25800  brbtwn  25843  brcgr  25844  brbtwn2  25849  axcontlem7  25914  cgrcom  25929  cgrcoml  25935  cgrdegen  25943  btwncom  25953  brsegle  26047  brsegle2  26048  colinbtwnle  26057  btwnoutside  26064  broutsideof3  26065  outsidele  26071  lineunray  26086  lineelsb2  26087  elhf2  26121  ontgval  26186  ordtop  26191  ordcmp  26202  nndivsub  26212  wl-bibi1  26228  cnambfre  26267  itg2addnc  26273  elicc3  26334  nn0prpwlem  26339  opnbnd  26342  cldbnd  26343  opnregcld  26347  cldregopn  26348  fnessref  26387  refssfne  26388  locfincmp  26398  neibastop2  26404  fnemeet2  26410  fnejoin2  26412  fgmin  26413  brabg2  26431  istotbnd3  26494  sstotbnd2  26497  sstotbnd  26498  sstotbnd3  26499  ssbnd  26511  ismtybnd  26530  reheibor  26562  grpoeqdivid  26570  grpokerinj  26574  1idl  26650  0rngo  26651  divrngidl  26652  igenval2  26690  ispridlc  26694  isdmn3  26698  prtlem10  26728  prter2  26744  ralxpmap  26756  elrfi  26762  diophrw  26831  eldioph2b  26835  diophin  26845  rexrabdioph  26868  rmxycomplete  26994  coprmdvdsb  27066  jm2.19  27078  jm2.26  27087  jm2.27  27093  limsuc2  27129  islinds4  27296  dgraa0p  27345  rngunsnply  27369  fiuneneq  27504  hashgcdlem  27507  dvconstbi  27542  expgrowth  27543  ax10ext  27597  pm14.24  27623  sbiota1  27625  sigarcol  27844  rexsb  27936  2reu2  27955  ralbinrald  27967  rlimdmafv  28031  ralxfrd2  28087  2ffzoeq  28163  euhash1  28190  uvtxnb  28331  usgra2pth  28349  wlkiswwlk  28380  wlklniswwlkn  28383  el2wlkonot  28401  el2spthonot  28402  el2wlkonotot0  28404  el2wlksotot  28414  usg2wlkonot  28415  usg2spthonot  28420  usg2spthonot0  28421  nbhashuvtx  28432  uvtxhashnb  28433  0eusgraiff0rgra  28450  cusgraiffrusgra  28451  frgra3vlem2  28465  frgrancvvdeqlem3  28495  sbcim2g  28697  sineq0ALT  29123  bnj145  29168  dral1NEW7  29567  cbv2hwAUX7  29587  sbiedNEW7  29614  sbftNEW7  29630  sbequNEW7  29654  sb8dwAUX7  29664  sb56NEW7  29670  exsbNEW7  29673  sbal1NEW7  29689  ax11bNEW7  29696  cbv2hOLD7  29795  lubunNEW  29845  lshpinN  29861  lsatcveq0  29904  lsatcv0eq  29919  lsatcv1  29920  islshpcv  29925  lkr0f  29966  lkrshp4  29980  lshpkrlem1  29982  lshpset2N  29991  lfl1dim  29993  lfl1dim2N  29994  lub0N  30061  glb0N  30065  oplecon3b  30072  cmtcomN  30121  cmtbr3N  30126  cmtbr4N  30127  cvrnbtwn2  30147  cvrnbtwn3  30148  cvrcon3b  30149  cvrnbtwn4  30151  cvrcmp  30155  atcvreq0  30186  atnle  30189  atlatle  30192  cvlexchb1  30202  cvlcvr1  30211  hlrelat2  30274  exatleN  30275  cvrval3  30284  cvrval4N  30285  cvrexch  30291  atcvr0eq  30297  lnnat  30298  atcvrj0  30299  atcvrj2b  30303  atltcvr  30306  atbtwn  30317  ps-1  30348  3at  30361  islln2a  30388  llncmp  30393  islpln2a  30419  lplncmp  30433  islvol2aN  30463  4at  30484  lvolcmp  30488  pmaple  30632  lncmp  30654  paddss  30716  llnexchb2lem  30739  2polcon4bN  30789  ispsubcl2N  30818  lhpat3  30917  lautcvr  30963  ltrnid  31006  trlval2  31034  trlatn0  31043  ltrnideq  31046  trlnidatb  31048  cdlemeg49lebilem  31410  trlord  31440  cdlemg1a  31441  cdlemg1cex  31459  tendoid0  31696  dva1dim  31856  cdlemm10N  31990  diarnN  32001  cdlemn  32084  dihlspsnssN  32204  dihatexv  32210  dochkrshp  32258  dochkrshp4  32261  djhlsmcl  32286  lcfl6  32372  lcfl8  32374  lcfrvalsnN  32413  lcfrlem9  32422  mapdval2N  32502  mapdordlem2  32509  mapd1o  32520  mapd0  32537  mapdheq2biN  32602
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 179
  Copyright terms: Public domain W3C validator