MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impbid Structured version   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  2126  sbequ  2140  sb56  2174  sbal1  2203  exsb  2207  dral1-o  2231  eupickb  2346  eupickbi  2347  2eu2  2362  ceqsalt  2971  ceqex  3059  mob2  3107  reu6  3116  sbciegft  3184  eqsbc3r  3211  csbiebt  3280  sseq1  3362  reupick  3618  reupick2  3620  uneqdifeq  3709  prnebg  3972  disjeq2  4179  disjeq1  4182  disjxiun  4202  disjss3  4204  copsexg  4435  euotd  4450  poeq2  4500  sotric  4522  sotrieq  4523  freq2  4546  seeq1  4547  seeq2  4548  tz7.7  4600  ordtri1  4607  ordtri3  4610  ordelinel  4673  reusv2lem2  4718  reusv2lem3  4719  alxfr  4729  ralxfrd  4730  oneqmin  4778  ordsuc  4787  ordelsuc  4793  ordsucelsuc  4795  ordunisuc2  4817  limsuc  4822  iss  5182  iotaval  5422  funeq  5466  funssres  5486  tz6.12c  5743  fnbrfvb  5760  ssimaex  5781  fvimacnv  5838  elpreima  5843  eldmrexrnb  5870  fsn  5899  fconst2g  5939  fconst5  5942  elunirnALT  5993  f1ocnvfvb  6010  foeqcnvco  6020  f1eqcocnv  6021  fliftfun  6027  soisores  6040  isofr  6055  isose  6056  isopo  6059  isoso  6061  f1oiso2  6065  oprabid  6098  f1opw2  6291  op1steq  6384  rntpos  6485  eusvobj2  6575  smoiso2  6624  seqomlem2  6701  oaord  6783  oawordex  6793  oaordex  6794  omord2  6803  om00  6811  oeord  6824  nnaord  6855  nnmord  6868  nnawordex  6873  nnaordex  6874  erexb  6923  swoord1  6927  swoord2  6928  iiner  6969  eceqoveq  7002  omxpenlem  7202  domtriord  7246  mapxpen  7266  mapunen  7269  ssenen  7274  nneneq  7283  onomeneq  7289  nndomo  7293  fodomfib  7379  f1opwfi  7403  elfiun  7428  suplub2  7459  ordiso2  7477  ordiso  7478  oieu  7501  brwdom2  7534  brwdom3  7543  cantnfreslem  7624  cantnflem1  7638  cardidm  7839  carddom2  7857  pm54.43  7880  pr2ne  7882  acnen  7927  acnen2  7929  alephord  7949  alephinit  7969  dfac5  8002  infdif2  8083  fictb  8118  coflim  8134  fincssdom  8196  fin23lem25  8197  isf32lem9  8234  isf34lem4  8250  fin1a2lem11  8283  axdc3lem2  8324  ficard  8433  fpwwe2lem12  8509  fpwwe2  8511  indpi  8777  nqereq  8805  1idpr  8899  ltapr  8915  leltne  9157  ltlen  9168  ltadd2  9170  ltord1  9546  mul0or  9655  ltmul1  9853  lt2msq  9887  nnsub  10031  nn0sub  10263  zrevaddcl  10314  zltp1le  10318  zdiv  10333  nneo  10346  zeo2  10349  zmax  10564  zbtwnre  10565  qrevaddcl  10589  xrlttri  10725  xrleltne  10731  xralrple  10784  xltneg  10796  xleadd1  10827  xlemul1  10862  supxrunb1  10891  supxrunb2  10892  ioo0  10934  iccid  10954  ico0  10955  ioc0  10956  icc0  10957  difreicc  11021  iccsplit  11022  0fz1  11067  uzsplit  11111  fzm1  11120  fzrevral  11124  elfznelfzob  11186  flge  11207  modid2  11264  seqf1olem1  11355  hashen  11624  hashdom  11646  hashle00  11662  hash2prb  11682  hashtpg  11684  shftlem  11876  shftuz  11877  abslt  12111  absle  12112  rexico  12150  cau3lem  12151  rlim2lt  12284  rlim3  12285  o1lo1  12324  rlimdm  12338  climshft  12363  o1dif  12416  isercolllem2  12452  isercoll  12454  zsum  12505  fsum  12507  fsum00  12570  incexclem  12609  dvdsval2  12848  moddvds  12852  negdvdsb  12859  dvdsnegb  12860  dvdscmulr  12871  dvdsmulcr  12872  dvdssub2  12880  fzo0dvdseq  12895  bitsf1ocnv  12949  sadcaddlem  12962  bitsuz  12979  dvdsgcdb  13037  gcdeq  13045  dvdssqlem  13052  isprm2lem  13079  dvdsprime  13085  dvdsprm  13092  coprm  13093  euclemma  13101  rpexp  13113  prmdiveq  13168  odzdvds  13174  pythagtrip  13201  pc2dvds  13245  pcprmpw2  13248  pcprmpw  13249  vdwapun  13335  ramtcl2  13372  firest  13653  mrieqv2d  13857  isacs2  13871  isssc  14013  setciso  14239  posasymb  14402  pleval2  14415  pltval3  14417  lubid  14432  joinle  14443  meetle  14450  lubun  14543  clatleglb  14546  latdisd  14609  letsr  14665  gsumval2a  14775  frmdss2  14801  isgrpid2  14834  isgrpinv  14848  oddvdsnn0  15175  oddvds  15178  odeq  15181  odeq1  15189  gexdvds  15211  pgpfi  15232  pgpssslw  15241  fislw  15252  sylow3lem2  15255  lsmelvalm  15278  lsmlub  15290  lsmss1b  15292  lsmss2b  15294  efgs1b  15361  cyggenod  15487  cyggexb  15501  dprdfeq0  15573  unitmulclb  15763  dvreq1  15791  drngmul0or  15849  isabvd  15901  issrngd  15942  lssats2  16069  lspsneq0  16081  lsmelval2  16150  lvecvs0or  16173  lspsneq  16187  lspsneu  16188  lidl1el  16282  lidldvgen  16319  isnzr2  16327  rrgeq0  16343  domneq0  16350  znunit  16837  ipeq0  16862  ocvsscon  16895  pjdm2  16931  obselocv  16948  unitg  17025  tgss3  17044  clsval2  17107  isopn3  17123  elcls3  17140  opncldf1  17141  neiint  17161  neips  17170  opnneissb  17171  opnssneib  17172  opnnei  17177  tpnei  17178  opnneiid  17183  restcld  17229  restopnb  17232  tgcn  17309  tgcnp  17310  subbascn  17311  iscnp4  17320  cnpnei  17321  cncls2  17330  cncls  17331  cnntr  17332  lmss  17355  hausnei2  17410  lpcls  17421  ordtt1  17436  cmpsub  17456  tgcmp  17457  1stcelcls  17517  kgencn2  17582  ptpjpre1  17596  upxp  17648  txcn  17651  txlm  17673  tgqtop  17737  kqfvima  17755  isr0  17762  regr1lem2  17765  hmeoopn  17791  hmeocld  17792  ptuncnv  17832  fbunfip  17894  fgss2  17899  ufilb  17931  ufprim  17934  trufil  17935  cfinufil  17953  ufildr  17956  elfm2  17973  elfm3  17975  rnelfm  17978  fmfnfmlem4  17982  fmco  17986  flimtopon  17995  flimopn  18000  fbflim2  18002  flimrest  18008  flffbas  18020  cnpflf  18026  fclstopon  18037  fclsnei  18044  fclsbas  18046  fclsfnflim  18052  fclscmp  18055  ufilcmp  18057  isfcf  18059  fcfnei  18060  cnpfcf  18066  alexsubb  18070  alexsubALT  18075  cldsubg  18133  tgphaus  18139  tgpt0  18141  tsmsgsum  18161  tsmsres  18166  xbln0  18437  blssexps  18449  blssex  18450  isxms2  18471  prdsbl  18514  neibl  18524  metss  18531  met2ndc  18546  metrest  18547  metcnp3  18563  nmoeq0  18763  xrsxmet  18833  reconn  18852  iccpnfcnv  18962  fgcfil  19217  iscau4  19225  cfilres  19242  iunmbl2  19444  ismbf3d  19539  mbfaddlem  19545  i1faddlem  19578  i1fmullem  19579  ellimc3  19759  tdeglem4  19976  deg1nn0clb  20006  deg1lt0  20007  dvdsq1p  20076  plypf1  20124  0dgrb  20158  plymul0or  20191  ulmshft  20299  ulmcaulem  20303  ulmcau  20304  cosord  20427  eff1olem  20443  lognegb  20477  eflogeq  20489  logdivlt  20509  efopn  20542  cxpeq0  20562  cxpeq  20634  angpieqvd  20665  dcubic  20679  asinsinb  20730  acoscosb  20731  atantanb  20757  rlimcnp  20797  isppw  20890  isppw2  20891  vmappw  20892  isnsqf  20911  ppieq0  20952  fsumdvdsdiag  20962  dvdsppwf1o  20964  fsumfldivdiag  20968  chpeq0  20985  chteq0  20986  dchrptlem1  21041  lgsdir2lem4  21103  lgsne0  21110  lgsqr  21123  lgsdchrval  21124  lgsquadlem1  21131  m1lgs  21139  ausisusgra  21373  nbgraf1olem5  21448  edgusgranbfin  21452  nb3graprlem1  21453  cusgrarn  21461  nbcusgra  21465  cusgrafilem2  21482  uvtxnbgra  21495  spthonepeq  21580  3v3e3cycl  21645  eupath2lem3  21694  grpoinvf  21821  rngosn3  22007  rngosn4  22008  rngoueqz  22011  rngoridfz  22016  nvmul0or  22126  nvz  22151  diporthcom  22208  ubthlem3  22367  hvmul0or  22520  his6  22594  hial0  22597  hial02  22598  orthcom  22603  normgt0  22622  ocin  22791  occon3  22792  shsel3  22810  shlub  22909  chssoc  22991  h1de2bi  23049  spansncol  23063  elspansn4  23068  spansnss2  23070  sumspansn  23144  lnopcnbd  23532  lnfncnbd  23553  riesz1  23561  elpjrn  23686  cvcon3  23780  dmdmd  23796  dmdbr3  23801  dmdbr4  23802  dmdbr5  23804  mdslmd1i  23825  atcveq0  23844  chcv1  23851  atssma  23874  atcv0eq  23875  atcv1  23876  bian1d  23943  xaddeq0  24112  eliccelico  24133  elicoelioo  24134  pstmfval  24284  unitdivcld  24292  xrge0iifcnv  24312  lmxrge0  24330  indf1ofs  24416  dstfrvunirn  24725  cvmliftmolem2  24962  cvmlift2lem12  24994  ghomf1olem  25098  climuzcnv  25101  relexpindlem  25132  mulge0b  25184  zprod  25256  fprod  25260  br8  25372  br6  25373  br4  25374  funbreq  25388  fprb  25390  axext4dist  25421  nodenselem8  25636  dfrdg4  25788  brbtwn  25831  brcgr  25832  brbtwn2  25837  axcontlem7  25902  cgrcom  25917  cgrcoml  25923  cgrdegen  25931  btwncom  25941  brsegle  26035  brsegle2  26036  colinbtwnle  26045  btwnoutside  26052  broutsideof3  26053  outsidele  26059  lineunray  26074  lineelsb2  26075  elhf2  26109  ontgval  26174  ordtop  26179  ordcmp  26190  nndivsub  26200  wl-bibi1  26216  cnambfre  26246  itg2addnc  26250  elicc3  26312  nn0prpwlem  26317  opnbnd  26320  cldbnd  26321  opnregcld  26325  cldregopn  26326  fnessref  26365  refssfne  26366  locfincmp  26376  neibastop2  26382  fnemeet2  26388  fnejoin2  26390  fgmin  26391  brabg2  26409  istotbnd3  26472  sstotbnd2  26475  sstotbnd  26476  sstotbnd3  26477  ssbnd  26489  ismtybnd  26508  reheibor  26540  grpoeqdivid  26548  grpokerinj  26552  1idl  26628  0rngo  26629  divrngidl  26630  igenval2  26668  ispridlc  26672  isdmn3  26676  prtlem10  26706  prter2  26722  ralxpmap  26734  elrfi  26740  diophrw  26809  eldioph2b  26813  diophin  26823  rexrabdioph  26846  rmxycomplete  26972  coprmdvdsb  27044  jm2.19  27056  jm2.26  27065  jm2.27  27071  limsuc2  27107  islinds4  27274  dgraa0p  27323  rngunsnply  27347  fiuneneq  27482  hashgcdlem  27485  dvconstbi  27520  expgrowth  27521  ax10ext  27575  pm14.24  27601  sbiota1  27603  sigarcol  27822  rexsb  27914  2reu2  27933  ralbinrald  27945  rlimdmafv  28009  ralxfrd2  28060  euhash1  28146  usgra2pth  28265  el2wlkonot  28290  el2spthonot  28291  el2wlkonotot0  28293  el2wlksotot  28303  usg2wlkonot  28304  usg2spthonot  28309  usg2spthonot0  28310  frgra3vlem2  28329  frgrancvvdeqlem3  28359  sbcim2g  28561  sineq0ALT  28987  bnj145  29032  dral1NEW7  29431  cbv2hwAUX7  29451  sbiedNEW7  29478  sbftNEW7  29494  sbequNEW7  29518  sb8dwAUX7  29528  sb56NEW7  29534  exsbNEW7  29537  sbal1NEW7  29553  ax11bNEW7  29560  cbv2hOLD7  29659  lubunNEW  29709  lshpinN  29725  lsatcveq0  29768  lsatcv0eq  29783  lsatcv1  29784  islshpcv  29789  lkr0f  29830  lkrshp4  29844  lshpkrlem1  29846  lshpset2N  29855  lfl1dim  29857  lfl1dim2N  29858  lub0N  29925  glb0N  29929  oplecon3b  29936  cmtcomN  29985  cmtbr3N  29990  cmtbr4N  29991  cvrnbtwn2  30011  cvrnbtwn3  30012  cvrcon3b  30013  cvrnbtwn4  30015  cvrcmp  30019  atcvreq0  30050  atnle  30053  atlatle  30056  cvlexchb1  30066  cvlcvr1  30075  hlrelat2  30138  exatleN  30139  cvrval3  30148  cvrval4N  30149  cvrexch  30155  atcvr0eq  30161  lnnat  30162  atcvrj0  30163  atcvrj2b  30167  atltcvr  30170  atbtwn  30181  ps-1  30212  3at  30225  islln2a  30252  llncmp  30257  islpln2a  30283  lplncmp  30297  islvol2aN  30327  4at  30348  lvolcmp  30352  pmaple  30496  lncmp  30518  paddss  30580  llnexchb2lem  30603  2polcon4bN  30653  ispsubcl2N  30682  lhpat3  30781  lautcvr  30827  ltrnid  30870  trlval2  30898  trlatn0  30907  ltrnideq  30910  trlnidatb  30912  cdlemeg49lebilem  31274  trlord  31304  cdlemg1a  31305  cdlemg1cex  31323  tendoid0  31560  dva1dim  31720  cdlemm10N  31854  diarnN  31865  cdlemn  31948  dihlspsnssN  32068  dihatexv  32074  dochkrshp  32122  dochkrshp4  32125  djhlsmcl  32150  lcfl6  32236  lcfl8  32238  lcfrvalsnN  32277  lcfrlem9  32286  mapdval2N  32366  mapdordlem2  32373  mapd1o  32384  mapd0  32401  mapdheq2biN  32466
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