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  1570  exbi  1588  equequ1  1691  equequ1OLD  1692  elequ1  1720  elequ2  1722  19.21t  1803  19.23t  1808  19.23tOLD  1828  19.21tOLD  1875  sbequ12  1933  dral1  2004  cbv2h  2015  ax11b  2029  sbft  2058  sbied  2069  sbequ  2093  sb56  2131  sbal1  2160  exsb  2164  dral1-o  2188  eupickb  2303  eupickbi  2304  2eu2  2319  ceqsalt  2921  ceqex  3009  mob2  3057  reu6  3066  sbciegft  3134  eqsbc3r  3161  csbiebt  3230  sseq1  3312  reupick  3568  reupick2  3570  uneqdifeq  3659  prnebg  3921  disjeq2  4127  disjeq1  4130  disjxiun  4150  disjss3  4152  copsexg  4383  euotd  4398  poeq2  4448  sotric  4470  sotrieq  4471  freq2  4494  seeq1  4495  seeq2  4496  tz7.7  4548  ordtri1  4555  ordtri3  4558  ordelinel  4620  reusv2lem2  4665  reusv2lem3  4666  alxfr  4676  ralxfrd  4677  oneqmin  4725  ordsuc  4734  ordelsuc  4740  ordsucelsuc  4742  ordunisuc2  4764  limsuc  4769  iss  5129  iotaval  5369  funeq  5413  funssres  5433  tz6.12c  5690  fnbrfvb  5706  ssimaex  5727  fvimacnv  5784  elpreima  5789  eldmrexrnb  5816  fsn  5845  fconst2g  5885  fconst5  5888  elunirnALT  5939  f1ocnvfvb  5956  foeqcnvco  5966  f1eqcocnv  5967  fliftfun  5973  soisores  5986  isofr  6001  isose  6002  isopo  6005  isoso  6007  f1oiso2  6011  oprabid  6044  f1opw2  6237  op1steq  6330  rntpos  6428  eusvobj2  6518  smoiso2  6567  seqomlem2  6644  oaord  6726  oawordex  6736  oaordex  6737  omord2  6746  om00  6754  oeord  6767  nnaord  6798  nnmord  6811  nnawordex  6816  nnaordex  6817  erexb  6866  swoord1  6870  swoord2  6871  iiner  6912  eceqoveq  6945  omxpenlem  7145  domtriord  7189  mapxpen  7209  mapunen  7212  ssenen  7217  nneneq  7226  onomeneq  7232  nndomo  7236  fodomfib  7322  f1opwfi  7345  elfiun  7370  suplub2  7399  ordiso2  7417  ordiso  7418  oieu  7441  brwdom2  7474  brwdom3  7483  cantnfreslem  7564  cantnflem1  7578  cardidm  7779  carddom2  7797  pm54.43  7820  pr2ne  7822  acnen  7867  acnen2  7869  alephord  7889  alephinit  7909  dfac5  7942  infdif2  8023  fictb  8058  coflim  8074  fincssdom  8136  fin23lem25  8137  isf32lem9  8174  isf34lem4  8190  fin1a2lem11  8223  axdc3lem2  8264  ficard  8373  fpwwe2lem12  8449  fpwwe2  8451  indpi  8717  nqereq  8745  1idpr  8839  ltapr  8855  leltne  9097  ltlen  9108  ltadd2  9110  ltord1  9485  mul0or  9594  ltmul1  9792  lt2msq  9826  nnsub  9970  nn0sub  10202  zrevaddcl  10253  zltp1le  10257  zdiv  10272  nneo  10285  zeo2  10288  zmax  10503  zbtwnre  10504  qrevaddcl  10528  xrlttri  10664  xrleltne  10670  xralrple  10723  xltneg  10735  xleadd1  10766  xlemul1  10801  supxrunb1  10830  supxrunb2  10831  ioo0  10873  iccid  10893  ico0  10894  ioc0  10895  icc0  10896  difreicc  10960  iccsplit  10961  0fz1  11006  uzsplit  11048  fzm1  11057  fzrevral  11061  elfznelfzob  11120  flge  11141  modid2  11198  seqf1olem1  11289  hashen  11558  hashdom  11580  hashle00  11596  hash2prb  11616  hashtpg  11618  shftlem  11810  shftuz  11811  abslt  12045  absle  12046  rexico  12084  cau3lem  12085  rlim2lt  12218  rlim3  12219  o1lo1  12258  rlimdm  12272  climshft  12297  o1dif  12350  isercolllem2  12386  isercoll  12388  zsum  12439  fsum  12441  fsum00  12504  incexclem  12543  dvdsval2  12782  moddvds  12786  negdvdsb  12793  dvdsnegb  12794  dvdscmulr  12805  dvdsmulcr  12806  dvdssub2  12814  fzo0dvdseq  12829  bitsf1ocnv  12883  sadcaddlem  12896  bitsuz  12913  dvdsgcdb  12971  gcdeq  12979  dvdssqlem  12986  isprm2lem  13013  dvdsprime  13019  dvdsprm  13026  coprm  13027  euclemma  13035  rpexp  13047  prmdiveq  13102  odzdvds  13108  pythagtrip  13135  pc2dvds  13179  pcprmpw2  13182  pcprmpw  13183  vdwapun  13269  ramtcl2  13306  firest  13587  mrieqv2d  13791  isacs2  13805  isssc  13947  setciso  14173  posasymb  14336  pleval2  14349  pltval3  14351  lubid  14366  joinle  14377  meetle  14384  lubun  14477  clatleglb  14480  latdisd  14543  letsr  14599  gsumval2a  14709  frmdss2  14735  isgrpid2  14768  isgrpinv  14782  oddvdsnn0  15109  oddvds  15112  odeq  15115  odeq1  15123  gexdvds  15145  pgpfi  15166  pgpssslw  15175  fislw  15186  sylow3lem2  15189  lsmelvalm  15212  lsmlub  15224  lsmss1b  15226  lsmss2b  15228  efgs1b  15295  cyggenod  15421  cyggexb  15435  dprdfeq0  15507  unitmulclb  15697  dvreq1  15725  drngmul0or  15783  isabvd  15835  issrngd  15876  lssats2  16003  lspsneq0  16015  lsmelval2  16084  lvecvs0or  16107  lspsneq  16121  lspsneu  16122  lidl1el  16216  lidldvgen  16253  isnzr2  16261  rrgeq0  16277  domneq0  16284  znunit  16767  ipeq0  16792  ocvsscon  16825  pjdm2  16861  obselocv  16878  unitg  16955  tgss3  16974  clsval2  17037  isopn3  17053  elcls3  17070  opncldf1  17071  neiint  17091  neips  17100  opnneissb  17101  opnssneib  17102  opnnei  17107  tpnei  17108  opnneiid  17113  restcld  17158  restopnb  17161  tgcn  17238  tgcnp  17239  subbascn  17240  iscnp4  17249  cnpnei  17250  cncls2  17259  cncls  17260  cnntr  17261  lmss  17284  hausnei2  17339  lpcls  17350  ordtt1  17365  cmpsub  17385  tgcmp  17386  1stcelcls  17445  kgencn2  17510  ptpjpre1  17524  upxp  17576  txcn  17579  txlm  17601  tgqtop  17665  kqfvima  17683  isr0  17690  regr1lem2  17693  hmeoopn  17719  hmeocld  17720  ptuncnv  17760  fbunfip  17822  fgss2  17827  ufilb  17859  ufprim  17862  trufil  17863  cfinufil  17881  ufildr  17884  elfm2  17901  elfm3  17903  rnelfm  17906  fmfnfmlem4  17910  fmco  17914  flimtopon  17923  flimopn  17928  fbflim2  17930  flimrest  17936  flffbas  17948  cnpflf  17954  fclstopon  17965  fclsnei  17972  fclsbas  17974  fclsfnflim  17980  fclscmp  17983  ufilcmp  17985  isfcf  17987  fcfnei  17988  cnpfcf  17994  alexsubb  17998  alexsubALT  18003  cldsubg  18061  tgphaus  18067  tgpt0  18069  tsmsgsum  18089  tsmsres  18094  xbln0  18339  blssex  18347  isxms2  18368  prdsbl  18411  neibl  18421  metss  18428  met2ndc  18443  metrest  18444  metcnp3  18460  nmoeq0  18641  xrsxmet  18711  reconn  18730  iccpnfcnv  18840  fgcfil  19095  iscau4  19103  cfilres  19120  iunmbl2  19318  ismbf3d  19413  mbfaddlem  19419  i1faddlem  19452  i1fmullem  19453  ellimc3  19633  tdeglem4  19850  deg1nn0clb  19880  deg1lt0  19881  dvdsq1p  19950  plypf1  19998  0dgrb  20032  plymul0or  20065  ulmshft  20173  ulmcaulem  20177  ulmcau  20178  cosord  20301  eff1olem  20317  lognegb  20351  eflogeq  20363  logdivlt  20383  efopn  20416  cxpeq0  20436  cxpeq  20508  angpieqvd  20539  dcubic  20553  asinsinb  20604  acoscosb  20605  atantanb  20631  rlimcnp  20671  isppw  20764  isppw2  20765  vmappw  20766  isnsqf  20785  ppieq0  20826  fsumdvdsdiag  20836  dvdsppwf1o  20838  fsumfldivdiag  20842  chpeq0  20859  chteq0  20860  dchrptlem1  20915  lgsdir2lem4  20977  lgsne0  20984  lgsqr  20997  lgsdchrval  20998  lgsquadlem1  21005  m1lgs  21013  ausisusgra  21247  nbusgra  21306  nbgraf1olem5  21321  edgusgranbfin  21325  nb3graprlem1  21326  cusgrarn  21334  nbcusgra  21338  cusgrafilem2  21355  uvtxnbgra  21368  3v3e3cycl  21500  eupath2lem3  21549  grpoinvf  21676  rngosn3  21862  rngosn4  21863  rngoueqz  21866  rngoridfz  21871  nvmul0or  21981  nvz  22006  diporthcom  22063  ubthlem3  22222  hvmul0or  22375  his6  22449  hial0  22452  hial02  22453  orthcom  22458  normgt0  22477  ocin  22646  occon3  22647  shsel3  22665  shlub  22764  chssoc  22846  h1de2bi  22904  spansncol  22918  elspansn4  22923  spansnss2  22925  sumspansn  22999  lnopcnbd  23387  lnfncnbd  23408  riesz1  23416  elpjrn  23541  cvcon3  23635  dmdmd  23651  dmdbr3  23656  dmdbr4  23657  dmdbr5  23659  mdslmd1i  23680  atcveq0  23699  chcv1  23706  atssma  23729  atcv0eq  23730  atcv1  23731  bian1d  23798  eliccelico  23976  elicoelioo  23977  xaddeq0  24030  unitdivcld  24103  xrge0iifcnv  24123  lmxrge0  24141  indf1ofs  24219  dstfrvunirn  24511  cvmliftmolem2  24748  cvmlift2lem12  24780  ghomf1olem  24884  climuzcnv  24887  relexpindlem  24918  mulge0b  24970  zprod  25042  fprod  25046  br8  25137  br6  25138  br4  25139  funbreq  25151  fprb  25153  axext4dist  25181  nodenselem8  25366  dfrdg4  25513  brbtwn  25552  brcgr  25553  brbtwn2  25558  axcontlem7  25623  cgrcom  25638  cgrcoml  25644  cgrdegen  25652  btwncom  25662  brsegle  25756  brsegle2  25757  colinbtwnle  25766  btwnoutside  25773  broutsideof3  25774  outsidele  25780  lineunray  25795  lineelsb2  25796  elhf2  25830  ontgval  25895  ordtop  25900  ordcmp  25911  nndivsub  25921  wl-bibi1  25937  itg2addnc  25959  elicc3  26011  nn0prpwlem  26016  opnbnd  26019  cldbnd  26020  opnregcld  26024  cldregopn  26025  fnessref  26064  refssfne  26065  locfincmp  26075  neibastop2  26081  fnemeet2  26087  fnejoin2  26089  fgmin  26090  brabg2  26108  istotbnd3  26171  sstotbnd2  26174  sstotbnd  26175  sstotbnd3  26176  ssbnd  26188  ismtybnd  26207  reheibor  26239  grpoeqdivid  26247  grpokerinj  26251  1idl  26327  0rngo  26328  divrngidl  26329  igenval2  26367  ispridlc  26371  isdmn3  26375  prtlem10  26405  prter2  26421  ralxpmap  26433  elrfi  26439  diophrw  26508  eldioph2b  26512  diophin  26522  rexrabdioph  26545  rmxycomplete  26671  coprmdvdsb  26743  jm2.19  26755  jm2.26  26764  jm2.27  26770  limsuc2  26806  islinds4  26974  dgraa0p  27023  rngunsnply  27047  fiuneneq  27182  hashgcdlem  27185  dvconstbi  27220  expgrowth  27221  ax10ext  27275  pm14.24  27301  sbiota1  27303  sigarcol  27522  rexsb  27614  2reu2  27633  ralbinrald  27645  rlimdmafv  27710  frgra3vlem2  27754  frgrancvvdeqlem3  27784  sbcim2g  27966  bnj145  28432  dral1NEW7  28831  cbv2hwAUX7  28851  sbiedNEW7  28876  sbftNEW7  28892  sbequNEW7  28915  sb56NEW7  28929  exsbNEW7  28932  sbal1NEW7  28948  ax11bNEW7  28955  cbv2hOLD7  29037  lubunNEW  29088  lshpinN  29104  lsatcveq0  29147  lsatcv0eq  29162  lsatcv1  29163  islshpcv  29168  lkr0f  29209  lkrshp4  29223  lshpkrlem1  29225  lshpset2N  29234  lfl1dim  29236  lfl1dim2N  29237  lub0N  29304  glb0N  29308  oplecon3b  29315  cmtcomN  29364  cmtbr3N  29369  cmtbr4N  29370  cvrnbtwn2  29390  cvrnbtwn3  29391  cvrcon3b  29392  cvrnbtwn4  29394  cvrcmp  29398  atcvreq0  29429  atnle  29432  atlatle  29435  cvlexchb1  29445  cvlcvr1  29454  hlrelat2  29517  exatleN  29518  cvrval3  29527  cvrval4N  29528  cvrexch  29534  atcvr0eq  29540  lnnat  29541  atcvrj0  29542  atcvrj2b  29546  atltcvr  29549  atbtwn  29560  ps-1  29591  3at  29604  islln2a  29631  llncmp  29636  islpln2a  29662  lplncmp  29676  islvol2aN  29706  4at  29727  lvolcmp  29731  pmaple  29875  lncmp  29897  paddss  29959  llnexchb2lem  29982  2polcon4bN  30032  ispsubcl2N  30061  lhpat3  30160  lautcvr  30206  ltrnid  30249  trlval2  30277  trlatn0  30286  ltrnideq  30289  trlnidatb  30291  cdlemeg49lebilem  30653  trlord  30683  cdlemg1a  30684  cdlemg1cex  30702  tendoid0  30939  dva1dim  31099  cdlemm10N  31233  diarnN  31244  cdlemn  31327  dihlspsnssN  31447  dihatexv  31453  dochkrshp  31501  dochkrshp4  31504  djhlsmcl  31529  lcfl6  31615  lcfl8  31617  lcfrvalsnN  31656  lcfrlem9  31665  mapdval2N  31745  mapdordlem2  31752  mapd1o  31763  mapd0  31780  mapdheq2biN  31845
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