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

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
StepHypRef Expression
1 impbid.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 impbid.2 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
31, 2impbid21d 183 . 2  |-  ( ph  ->  ( ph  ->  ( ps 
<->  ch ) ) )
43pm2.43i 45 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
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  1573  exbi  1591  equequ1  1696  equequ1OLD  1697  elequ1  1728  elequ2  1730  19.21t  1813  19.23t  1818  19.23tOLD  1838  19.21tOLD  1886  sbequ12  1944  cbv2h  1979  dral1  2053  dral1OLD  2054  ax11b  2078  sbft  2103  sbftOLD  2104  sbiedOLD  2124  sbequ  2138  sb56  2173  sbal1  2202  exsb  2206  dral1-o  2230  eupickb  2345  eupickbi  2346  2eu2  2361  ceqsalt  2970  ceqex  3058  mob2  3106  reu6  3115  sbciegft  3183  eqsbc3r  3210  csbiebt  3279  sseq1  3361  reupick  3617  reupick2  3619  uneqdifeq  3708  prnebg  3971  disjeq2  4178  disjeq1  4181  disjxiun  4201  disjss3  4203  copsexg  4434  euotd  4449  poeq2  4499  sotric  4521  sotrieq  4522  freq2  4545  seeq1  4546  seeq2  4547  tz7.7  4599  ordtri1  4606  ordtri3  4609  ordelinel  4671  reusv2lem2  4716  reusv2lem3  4717  alxfr  4727  ralxfrd  4728  oneqmin  4776  ordsuc  4785  ordelsuc  4791  ordsucelsuc  4793  ordunisuc2  4815  limsuc  4820  iss  5180  iotaval  5420  funeq  5464  funssres  5484  tz6.12c  5741  fnbrfvb  5758  ssimaex  5779  fvimacnv  5836  elpreima  5841  eldmrexrnb  5868  fsn  5897  fconst2g  5937  fconst5  5940  elunirnALT  5991  f1ocnvfvb  6008  foeqcnvco  6018  f1eqcocnv  6019  fliftfun  6025  soisores  6038  isofr  6053  isose  6054  isopo  6057  isoso  6059  f1oiso2  6063  oprabid  6096  f1opw2  6289  op1steq  6382  rntpos  6483  eusvobj2  6573  smoiso2  6622  seqomlem2  6699  oaord  6781  oawordex  6791  oaordex  6792  omord2  6801  om00  6809  oeord  6822  nnaord  6853  nnmord  6866  nnawordex  6871  nnaordex  6872  erexb  6921  swoord1  6925  swoord2  6926  iiner  6967  eceqoveq  7000  omxpenlem  7200  domtriord  7244  mapxpen  7264  mapunen  7267  ssenen  7272  nneneq  7281  onomeneq  7287  nndomo  7291  fodomfib  7377  f1opwfi  7401  elfiun  7426  suplub2  7455  ordiso2  7473  ordiso  7474  oieu  7497  brwdom2  7530  brwdom3  7539  cantnfreslem  7620  cantnflem1  7634  cardidm  7835  carddom2  7853  pm54.43  7876  pr2ne  7878  acnen  7923  acnen2  7925  alephord  7945  alephinit  7965  dfac5  7998  infdif2  8079  fictb  8114  coflim  8130  fincssdom  8192  fin23lem25  8193  isf32lem9  8230  isf34lem4  8246  fin1a2lem11  8279  axdc3lem2  8320  ficard  8429  fpwwe2lem12  8505  fpwwe2  8507  indpi  8773  nqereq  8801  1idpr  8895  ltapr  8911  leltne  9153  ltlen  9164  ltadd2  9166  ltord1  9542  mul0or  9651  ltmul1  9849  lt2msq  9883  nnsub  10027  nn0sub  10259  zrevaddcl  10310  zltp1le  10314  zdiv  10329  nneo  10342  zeo2  10345  zmax  10560  zbtwnre  10561  qrevaddcl  10585  xrlttri  10721  xrleltne  10727  xralrple  10780  xltneg  10792  xleadd1  10823  xlemul1  10858  supxrunb1  10887  supxrunb2  10888  ioo0  10930  iccid  10950  ico0  10951  ioc0  10952  icc0  10953  difreicc  11017  iccsplit  11018  0fz1  11063  uzsplit  11106  fzm1  11115  fzrevral  11119  elfznelfzob  11181  flge  11202  modid2  11259  seqf1olem1  11350  hashen  11619  hashdom  11641  hashle00  11657  hash2prb  11677  hashtpg  11679  shftlem  11871  shftuz  11872  abslt  12106  absle  12107  rexico  12145  cau3lem  12146  rlim2lt  12279  rlim3  12280  o1lo1  12319  rlimdm  12333  climshft  12358  o1dif  12411  isercolllem2  12447  isercoll  12449  zsum  12500  fsum  12502  fsum00  12565  incexclem  12604  dvdsval2  12843  moddvds  12847  negdvdsb  12854  dvdsnegb  12855  dvdscmulr  12866  dvdsmulcr  12867  dvdssub2  12875  fzo0dvdseq  12890  bitsf1ocnv  12944  sadcaddlem  12957  bitsuz  12974  dvdsgcdb  13032  gcdeq  13040  dvdssqlem  13047  isprm2lem  13074  dvdsprime  13080  dvdsprm  13087  coprm  13088  euclemma  13096  rpexp  13108  prmdiveq  13163  odzdvds  13169  pythagtrip  13196  pc2dvds  13240  pcprmpw2  13243  pcprmpw  13244  vdwapun  13330  ramtcl2  13367  firest  13648  mrieqv2d  13852  isacs2  13866  isssc  14008  setciso  14234  posasymb  14397  pleval2  14410  pltval3  14412  lubid  14427  joinle  14438  meetle  14445  lubun  14538  clatleglb  14541  latdisd  14604  letsr  14660  gsumval2a  14770  frmdss2  14796  isgrpid2  14829  isgrpinv  14843  oddvdsnn0  15170  oddvds  15173  odeq  15176  odeq1  15184  gexdvds  15206  pgpfi  15227  pgpssslw  15236  fislw  15247  sylow3lem2  15250  lsmelvalm  15273  lsmlub  15285  lsmss1b  15287  lsmss2b  15289  efgs1b  15356  cyggenod  15482  cyggexb  15496  dprdfeq0  15568  unitmulclb  15758  dvreq1  15786  drngmul0or  15844  isabvd  15896  issrngd  15937  lssats2  16064  lspsneq0  16076  lsmelval2  16145  lvecvs0or  16168  lspsneq  16182  lspsneu  16183  lidl1el  16277  lidldvgen  16314  isnzr2  16322  rrgeq0  16338  domneq0  16345  znunit  16832  ipeq0  16857  ocvsscon  16890  pjdm2  16926  obselocv  16943  unitg  17020  tgss3  17039  clsval2  17102  isopn3  17118  elcls3  17135  opncldf1  17136  neiint  17156  neips  17165  opnneissb  17166  opnssneib  17167  opnnei  17172  tpnei  17173  opnneiid  17178  restcld  17224  restopnb  17227  tgcn  17304  tgcnp  17305  subbascn  17306  iscnp4  17315  cnpnei  17316  cncls2  17325  cncls  17326  cnntr  17327  lmss  17350  hausnei2  17405  lpcls  17416  ordtt1  17431  cmpsub  17451  tgcmp  17452  1stcelcls  17512  kgencn2  17577  ptpjpre1  17591  upxp  17643  txcn  17646  txlm  17668  tgqtop  17732  kqfvima  17750  isr0  17757  regr1lem2  17760  hmeoopn  17786  hmeocld  17787  ptuncnv  17827  fbunfip  17889  fgss2  17894  ufilb  17926  ufprim  17929  trufil  17930  cfinufil  17948  ufildr  17951  elfm2  17968  elfm3  17970  rnelfm  17973  fmfnfmlem4  17977  fmco  17981  flimtopon  17990  flimopn  17995  fbflim2  17997  flimrest  18003  flffbas  18015  cnpflf  18021  fclstopon  18032  fclsnei  18039  fclsbas  18041  fclsfnflim  18047  fclscmp  18050  ufilcmp  18052  isfcf  18054  fcfnei  18055  cnpfcf  18061  alexsubb  18065  alexsubALT  18070  cldsubg  18128  tgphaus  18134  tgpt0  18136  tsmsgsum  18156  tsmsres  18161  xbln0  18432  blssexps  18444  blssex  18445  isxms2  18466  prdsbl  18509  neibl  18519  metss  18526  met2ndc  18541  metrest  18542  metcnp3  18558  nmoeq0  18758  xrsxmet  18828  reconn  18847  iccpnfcnv  18957  fgcfil  19212  iscau4  19220  cfilres  19237  iunmbl2  19439  ismbf3d  19534  mbfaddlem  19540  i1faddlem  19573  i1fmullem  19574  ellimc3  19754  tdeglem4  19971  deg1nn0clb  20001  deg1lt0  20002  dvdsq1p  20071  plypf1  20119  0dgrb  20153  plymul0or  20186  ulmshft  20294  ulmcaulem  20298  ulmcau  20299  cosord  20422  eff1olem  20438  lognegb  20472  eflogeq  20484  logdivlt  20504  efopn  20537  cxpeq0  20557  cxpeq  20629  angpieqvd  20660  dcubic  20674  asinsinb  20725  acoscosb  20726  atantanb  20752  rlimcnp  20792  isppw  20885  isppw2  20886  vmappw  20887  isnsqf  20906  ppieq0  20947  fsumdvdsdiag  20957  dvdsppwf1o  20959  fsumfldivdiag  20963  chpeq0  20980  chteq0  20981  dchrptlem1  21036  lgsdir2lem4  21098  lgsne0  21105  lgsqr  21118  lgsdchrval  21119  lgsquadlem1  21126  m1lgs  21134  ausisusgra  21368  nbgraf1olem5  21443  edgusgranbfin  21447  nb3graprlem1  21448  cusgrarn  21456  nbcusgra  21460  cusgrafilem2  21477  uvtxnbgra  21490  spthonepeq  21575  3v3e3cycl  21640  eupath2lem3  21689  grpoinvf  21816  rngosn3  22002  rngosn4  22003  rngoueqz  22006  rngoridfz  22011  nvmul0or  22121  nvz  22146  diporthcom  22203  ubthlem3  22362  hvmul0or  22515  his6  22589  hial0  22592  hial02  22593  orthcom  22598  normgt0  22617  ocin  22786  occon3  22787  shsel3  22805  shlub  22904  chssoc  22986  h1de2bi  23044  spansncol  23058  elspansn4  23063  spansnss2  23065  sumspansn  23139  lnopcnbd  23527  lnfncnbd  23548  riesz1  23556  elpjrn  23681  cvcon3  23775  dmdmd  23791  dmdbr3  23796  dmdbr4  23797  dmdbr5  23799  mdslmd1i  23820  atcveq0  23839  chcv1  23846  atssma  23869  atcv0eq  23870  atcv1  23871  bian1d  23938  xaddeq0  24107  eliccelico  24128  elicoelioo  24129  pstmfval  24279  unitdivcld  24287  xrge0iifcnv  24307  lmxrge0  24325  indf1ofs  24411  dstfrvunirn  24720  cvmliftmolem2  24957  cvmlift2lem12  24989  ghomf1olem  25093  climuzcnv  25096  relexpindlem  25127  mulge0b  25179  zprod  25252  fprod  25256  br8  25368  br6  25369  br4  25370  funbreq  25382  fprb  25384  axext4dist  25412  nodenselem8  25597  dfrdg4  25745  brbtwn  25786  brcgr  25787  brbtwn2  25792  axcontlem7  25857  cgrcom  25872  cgrcoml  25878  cgrdegen  25886  btwncom  25896  brsegle  25990  brsegle2  25991  colinbtwnle  26000  btwnoutside  26007  broutsideof3  26008  outsidele  26014  lineunray  26029  lineelsb2  26030  elhf2  26064  ontgval  26129  ordtop  26134  ordcmp  26145  nndivsub  26155  wl-bibi1  26171  cnambfre  26201  itg2addnc  26205  elicc3  26257  nn0prpwlem  26262  opnbnd  26265  cldbnd  26266  opnregcld  26270  cldregopn  26271  fnessref  26310  refssfne  26311  locfincmp  26321  neibastop2  26327  fnemeet2  26333  fnejoin2  26335  fgmin  26336  brabg2  26354  istotbnd3  26417  sstotbnd2  26420  sstotbnd  26421  sstotbnd3  26422  ssbnd  26434  ismtybnd  26453  reheibor  26485  grpoeqdivid  26493  grpokerinj  26497  1idl  26573  0rngo  26574  divrngidl  26575  igenval2  26613  ispridlc  26617  isdmn3  26621  prtlem10  26651  prter2  26667  ralxpmap  26679  elrfi  26685  diophrw  26754  eldioph2b  26758  diophin  26768  rexrabdioph  26791  rmxycomplete  26917  coprmdvdsb  26989  jm2.19  27001  jm2.26  27010  jm2.27  27016  limsuc2  27052  islinds4  27220  dgraa0p  27269  rngunsnply  27293  fiuneneq  27428  hashgcdlem  27431  dvconstbi  27466  expgrowth  27467  ax10ext  27521  pm14.24  27547  sbiota1  27549  sigarcol  27768  rexsb  27860  2reu2  27879  ralbinrald  27891  rlimdmafv  27955  ralxfrd2  28005  euhash1  28071  usgra2pth  28185  el2wlkonot  28210  el2spthonot  28211  el2wlkonotot0  28213  el2wlksotot  28223  usg2wlkonot  28224  usg2spthonot  28229  usg2spthonot0  28230  frgra3vlem2  28249  frgrancvvdeqlem3  28279  sbcim2g  28478  bnj145  28948  dral1NEW7  29347  cbv2hwAUX7  29367  sbiedNEW7  29392  sbftNEW7  29408  sbequNEW7  29431  sb56NEW7  29445  exsbNEW7  29448  sbal1NEW7  29464  ax11bNEW7  29471  cbv2hOLD7  29560  lubunNEW  29610  lshpinN  29626  lsatcveq0  29669  lsatcv0eq  29684  lsatcv1  29685  islshpcv  29690  lkr0f  29731  lkrshp4  29745  lshpkrlem1  29747  lshpset2N  29756  lfl1dim  29758  lfl1dim2N  29759  lub0N  29826  glb0N  29830  oplecon3b  29837  cmtcomN  29886  cmtbr3N  29891  cmtbr4N  29892  cvrnbtwn2  29912  cvrnbtwn3  29913  cvrcon3b  29914  cvrnbtwn4  29916  cvrcmp  29920  atcvreq0  29951  atnle  29954  atlatle  29957  cvlexchb1  29967  cvlcvr1  29976  hlrelat2  30039  exatleN  30040  cvrval3  30049  cvrval4N  30050  cvrexch  30056  atcvr0eq  30062  lnnat  30063  atcvrj0  30064  atcvrj2b  30068  atltcvr  30071  atbtwn  30082  ps-1  30113  3at  30126  islln2a  30153  llncmp  30158  islpln2a  30184  lplncmp  30198  islvol2aN  30228  4at  30249  lvolcmp  30253  pmaple  30397  lncmp  30419  paddss  30481  llnexchb2lem  30504  2polcon4bN  30554  ispsubcl2N  30583  lhpat3  30682  lautcvr  30728  ltrnid  30771  trlval2  30799  trlatn0  30808  ltrnideq  30811  trlnidatb  30813  cdlemeg49lebilem  31175  trlord  31205  cdlemg1a  31206  cdlemg1cex  31224  tendoid0  31461  dva1dim  31621  cdlemm10N  31755  diarnN  31766  cdlemn  31849  dihlspsnssN  31969  dihatexv  31975  dochkrshp  32023  dochkrshp4  32026  djhlsmcl  32051  lcfl6  32137  lcfl8  32139  lcfrvalsnN  32178  lcfrlem9  32187  mapdval2N  32267  mapdordlem2  32274  mapd1o  32285  mapd0  32302  mapdheq2biN  32367
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
  Copyright terms: Public domain W3C validator