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

Theorem impbid 183
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 182 . 2  |-  ( ph  ->  ( ph  ->  ( ps 
<->  ch ) ) )
43pm2.43i 43 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bicom1  190  impbid1  194  impcon4bid  196  pm5.74  235  imbi1d  308  pm5.501  330  2falsed  340  impbida  805  dedlem0b  919  dedlema  920  dedlemb  921  albi  1553  exbi  1570  equequ1  1650  elequ1  1689  elequ2  1691  19.21t  1792  19.23t  1798  sbequ12  1862  dral1  1907  cbv2h  1922  ax11b  1937  sbft  1967  sbied  1978  sbequ  2002  sb56  2039  sbal1  2067  exsb  2071  dral1-o  2095  eupickb  2210  eupickbi  2211  2eu2  2226  ceqsalt  2812  ceqex  2900  mob2  2947  reu6  2956  sbciegft  3023  eqsbc3r  3050  csbiebt  3119  sseq1  3201  reupick  3454  reupick2  3456  uneqdifeq  3544  disjeq2  3999  disjeq1  4002  disjxiun  4022  disjss3  4024  copsexg  4254  euotd  4269  poeq2  4320  sotric  4342  sotrieq  4343  freq2  4366  seeq1  4367  seeq2  4368  tz7.7  4420  ordtri1  4427  ordtri3  4430  ordelinel  4493  reusv2lem2  4538  reusv2lem3  4539  alxfr  4549  ralxfrd  4550  oneqmin  4598  ordsuc  4607  ordelsuc  4613  ordsucelsuc  4615  ordunisuc2  4637  limsuc  4642  iss  5000  iotaval  5232  funeq  5276  funssres  5296  tz6.12c  5549  fnbrfvb  5565  ssimaex  5586  fvimacnv  5642  elpreima  5647  fsn  5698  fconst2g  5730  fconst5  5733  elunirnALT  5781  f1ocnvfvb  5797  foeqcnvco  5806  f1eqcocnv  5807  fliftfun  5813  soisores  5826  isofr  5841  isose  5842  isopo  5845  isoso  5847  f1oiso2  5851  oprabid  5884  f1opw2  6073  op1steq  6166  rntpos  6249  eusvobj2  6339  smoiso2  6388  seqomlem2  6465  oaord  6547  oawordex  6557  oaordex  6558  omord2  6567  om00  6575  oeord  6588  nnaord  6619  nnmord  6632  nnawordex  6637  nnaordex  6638  erexb  6687  swoord1  6691  swoord2  6692  iiner  6733  eceqoveq  6765  omxpenlem  6965  domtriord  7009  mapxpen  7029  mapunen  7032  ssenen  7037  nneneq  7046  onomeneq  7052  nndomo  7056  fodomfib  7138  f1opwfi  7161  elfiun  7185  suplub2  7214  ordiso2  7232  ordiso  7233  oieu  7256  brwdom2  7289  brwdom3  7298  cantnfreslem  7379  cantnflem1  7393  cardidm  7594  carddom2  7612  pm54.43  7635  pr2ne  7637  acnen  7682  acnen2  7684  alephord  7704  alephinit  7724  dfac5  7757  infdif2  7838  fictb  7873  coflim  7889  fincssdom  7951  fin23lem25  7952  isf32lem9  7989  isf34lem4  8005  fin1a2lem11  8038  axdc3lem2  8079  ficard  8189  fpwwe2lem12  8265  fpwwe2  8267  indpi  8533  nqereq  8561  1idpr  8655  ltapr  8671  leltne  8913  ltlen  8924  ltadd2  8926  ltord1  9301  mul0or  9410  ltmul1  9608  lt2msq  9642  nnsub  9786  nn0sub  10016  zrevaddcl  10065  zltp1le  10069  zdiv  10084  nneo  10097  zeo2  10100  zmax  10315  zbtwnre  10316  qrevaddcl  10340  xrlttri  10475  xrleltne  10481  xralrple  10534  xltneg  10546  xleadd1  10577  xlemul1  10612  supxrunb1  10640  supxrunb2  10641  ioo0  10683  iccid  10703  ico0  10704  ioc0  10705  icc0  10706  difreicc  10769  iccsplit  10770  0fz1  10815  uzsplit  10857  fzm1  10864  fzrevral  10868  flge  10939  modid2  10996  seqf1olem1  11087  hashen  11348  hashdom  11363  shftlem  11565  shftuz  11566  abslt  11800  absle  11801  rexico  11839  cau3lem  11840  rlim2lt  11973  rlim3  11974  o1lo1  12013  rlimdm  12027  climshft  12052  o1dif  12105  isercolllem2  12141  isercoll  12143  zsum  12193  fsum  12195  fsum00  12258  incexclem  12297  dvdsval2  12536  moddvds  12540  negdvdsb  12547  dvdsnegb  12548  dvdscmulr  12559  dvdsmulcr  12560  dvdssub2  12568  fzo0dvdseq  12583  bitsf1ocnv  12637  sadcaddlem  12650  bitsuz  12667  dvdsgcdb  12725  gcdeq  12733  dvdssqlem  12740  isprm2lem  12767  dvdsprime  12773  dvdsprm  12780  coprm  12781  euclemma  12789  rpexp  12801  prmdiveq  12856  odzdvds  12862  pythagtrip  12889  pc2dvds  12933  pcprmpw2  12936  pcprmpw  12937  vdwapun  13023  ramtcl2  13060  firest  13339  mrieqv2d  13543  isacs2  13557  isssc  13699  setciso  13925  posasymb  14088  pleval2  14101  pltval3  14103  lubid  14118  joinle  14129  meetle  14136  lubun  14229  clatleglb  14232  latdisd  14295  letsr  14351  gsumval2a  14461  frmdss2  14487  isgrpid2  14520  isgrpinv  14534  oddvdsnn0  14861  oddvds  14864  odeq  14867  odeq1  14875  gexdvds  14897  pgpfi  14918  pgpssslw  14927  fislw  14938  sylow3lem2  14941  lsmelvalm  14964  lsmlub  14976  lsmss1b  14978  lsmss2b  14980  efgs1b  15047  cyggenod  15173  cyggexb  15187  dprdfeq0  15259  unitmulclb  15449  dvreq1  15477  drngmul0or  15535  isabvd  15587  issrngd  15628  lssats2  15759  lspsneq0  15771  lsmelval2  15840  lvecvs0or  15863  lspsneq  15877  lspsneu  15878  lidl1el  15972  lidldvgen  16009  isnzr2  16017  rrgeq0  16033  domneq0  16040  znunit  16519  ipeq0  16544  ocvsscon  16577  pjdm2  16613  obselocv  16630  unitg  16707  tgss3  16726  clsval2  16789  isopn3  16805  elcls3  16822  opncldf1  16823  neiint  16843  neips  16852  opnneissb  16853  opnssneib  16854  opnnei  16859  tpnei  16860  opnneiid  16865  restcld  16905  restopnb  16908  tgcn  16984  tgcnp  16985  subbascn  16986  cnpnei  16995  cncls2  17004  cncls  17005  cnntr  17006  lmss  17028  hausnei2  17083  lpcls  17094  ordtt1  17109  cmpsub  17129  tgcmp  17130  1stcelcls  17189  kgencn2  17254  ptpjpre1  17268  upxp  17319  txcn  17322  txlm  17344  tgqtop  17405  kqfvima  17423  isr0  17430  regr1lem2  17433  hmeoopn  17459  hmeocld  17460  ptuncnv  17500  fbunfip  17566  fgss2  17571  ufilb  17603  ufprim  17606  trufil  17607  cfinufil  17625  ufildr  17628  elfm2  17645  elfm3  17647  rnelfm  17650  fmfnfmlem4  17654  fmco  17658  flimtopon  17667  flimopn  17672  fbflim2  17674  flimrest  17680  flffbas  17692  cnpflf  17698  fclstopon  17709  fclsnei  17716  fclsbas  17718  fclsfnflim  17724  fclscmp  17727  ufilcmp  17729  isfcf  17731  fcfnei  17732  cnpfcf  17738  alexsubb  17742  alexsubALT  17747  cldsubg  17795  tgphaus  17801  tgpt0  17803  tsmsgsum  17823  tsmsres  17828  xbln0  17967  blssex  17975  isxms2  17996  prdsbl  18039  neibl  18049  metss  18056  met2ndc  18071  metrest  18072  metcnp3  18088  nmoeq0  18247  xrsxmet  18317  reconn  18335  iccpnfcnv  18444  fgcfil  18699  iscau4  18707  cfilres  18724  iunmbl2  18916  ismbf3d  19011  mbfaddlem  19017  i1faddlem  19050  i1fmullem  19051  ellimc3  19231  tdeglem4  19448  deg1nn0clb  19478  deg1lt0  19479  dvdsq1p  19548  plypf1  19596  0dgrb  19630  plymul0or  19663  ulmshft  19771  ulmcaulem  19773  ulmcau  19774  cosord  19896  eff1olem  19912  lognegb  19945  eflogeq  19957  logdivlt  19974  efopn  20007  cxpeq0  20027  cxpeq  20099  angpieqvd  20130  dcubic  20144  asinsinb  20195  acoscosb  20196  atantanb  20222  rlimcnp  20262  isppw  20354  isppw2  20355  vmappw  20356  isnsqf  20375  ppieq0  20416  fsumdvdsdiag  20426  dvdsppwf1o  20428  fsumfldivdiag  20432  chpeq0  20449  chteq0  20450  dchrptlem1  20505  lgsdir2lem4  20567  lgsne0  20574  lgsqr  20587  lgsdchrval  20588  lgsquadlem1  20595  m1lgs  20603  grpoinvf  20909  rngosn3  21095  rngosn4  21096  rngoueqz  21099  nvmul0or  21212  nvz  21237  diporthcom  21294  ubthlem3  21453  hvmul0or  21606  his6  21680  hial0  21683  hial02  21684  orthcom  21689  normgt0  21708  ocin  21877  occon3  21878  shsel3  21896  shlub  21995  chssoc  22077  h1de2bi  22135  spansncol  22149  elspansn4  22154  spansnss2  22156  sumspansn  22230  lnopcnbd  22618  lnfncnbd  22639  riesz1  22647  elpjrn  22772  cvcon3  22866  dmdmd  22882  dmdbr3  22887  dmdbr4  22888  dmdbr5  22890  mdslmd1i  22911  atcveq0  22930  chcv1  22937  atssma  22960  atcv0eq  22961  atcv1  22962  funimass4f  23044  ballotlemsf1o  23074  eliccioo  23117  bisimpd  23122  bian1d  23124  eliccelico  23272  elicoelioo  23273  unitdivcld  23287  xaddeq0  23306  xrsinvgval  23308  xrge0iifcnv  23317  disjabrex  23361  disjabrexf  23362  lmxrge0  23377  imambfm  23569  indf1ofs  23611  orvcgteel  23670  orvclteel  23675  dstfrvunirn  23677  cvmliftmolem2  23815  cvmlift2lem12  23847  eupath2lem3  23905  ghomf1olem  24003  climuzcnv  24006  relexpindlem  24038  mulge0b  24088  br8  24115  br6  24116  br4  24117  funbreq  24129  fprb  24131  axext4dist  24159  nodenselem8  24344  dfrdg4  24490  brbtwn  24529  brcgr  24530  brbtwn2  24535  axcontlem7  24600  cgrcom  24615  cgrcoml  24621  cgrdegen  24629  btwncom  24639  brsegle  24733  brsegle2  24734  colinbtwnle  24743  btwnoutside  24750  broutsideof3  24751  outsidele  24757  lineunray  24772  lineelsb2  24773  elhf2  24807  ontgval  24872  ordtop  24877  ordcmp  24888  nndivsub  24898  wl-bibi1  24915  itg2addnc  24935  copsexgb  24977  boxbid  25022  nxtbid  25023  diabid  25024  untbi12d  25033  domrngref  25071  domintreflemb  25073  f1ofi  25081  twsymr  25089  injrec2  25130  surjsec2  25131  repcpwti  25172  cbicp  25177  dupre1  25254  inposet  25289  dffprod  25330  grpodivfo  25385  trran2  25404  ltrran2  25414  rltrran  25425  rngoridfz  25448  svli2  25495  svs2  25498  cldifemp  25535  iscnp4  25574  limptlimpr  25587  flfnei2  25588  iint  25623  trran  25625  dmrngcmp  25762  ismonc  25825  isepic  25835  sgplpte21e  26148  xsyysx  26156  pdiveql  26179  abhp  26184  elicc3  26239  nn0prpwlem  26249  opnbnd  26254  cldbnd  26255  opnregcld  26259  cldregopn  26260  fnessref  26304  refssfne  26305  locfincmp  26315  neibastop2  26321  fnemeet2  26327  fnejoin2  26329  fgmin  26330  brabg2  26377  istotbnd3  26506  sstotbnd2  26509  sstotbnd  26510  sstotbnd3  26511  ssbnd  26523  ismtybnd  26542  reheibor  26574  grpoeqdivid  26582  grpokerinj  26586  1idl  26662  0rngo  26663  divrngidl  26664  igenval2  26702  ispridlc  26706  isdmn3  26710  prtlem10  26744  prter2  26760  ralxpmap  26772  elrfi  26780  diophrw  26849  eldioph2b  26853  diophin  26863  rexrabdioph  26886  rmxycomplete  27013  coprmdvdsb  27085  jm2.19  27097  jm2.26  27106  jm2.27  27112  limsuc2  27148  islinds4  27316  dgraa0p  27365  rngunsnply  27389  fiuneneq  27524  hashgcdlem  27527  dvconstbi  27562  expgrowth  27563  ax10ext  27617  pm14.24  27643  sbiota1  27645  sigarcol  27865  rexsb  27957  2reu2  27976  ralbinrald  27988  nbusgra  28154  nbcusgra  28170  uvtxnbgra  28176  frgra3vlem2  28190  sbcim2g  28358  bnj145  28828  ax9lem2  29214  lubunNEW  29236  lshpinN  29252  lsatcveq0  29295  lsatcv0eq  29310  lsatcv1  29311  islshpcv  29316  lkr0f  29357  lkrshp4  29371  lshpkrlem1  29373  lshpset2N  29382  lfl1dim  29384  lfl1dim2N  29385  lub0N  29452  glb0N  29456  oplecon3b  29463  cmtcomN  29512  cmtbr3N  29517  cmtbr4N  29518  cvrnbtwn2  29538  cvrnbtwn3  29539  cvrcon3b  29540  cvrnbtwn4  29542  cvrcmp  29546  atcvreq0  29577  atnle  29580  atlatle  29583  cvlexchb1  29593  cvlcvr1  29602  hlrelat2  29665  exatleN  29666  cvrval3  29675  cvrval4N  29676  cvrexch  29682  atcvr0eq  29688  lnnat  29689  atcvrj0  29690  atcvrj2b  29694  atltcvr  29697  atbtwn  29708  ps-1  29739  3at  29752  islln2a  29779  llncmp  29784  islpln2a  29810  lplncmp  29824  islvol2aN  29854  4at  29875  lvolcmp  29879  pmaple  30023  lncmp  30045  paddss  30107  llnexchb2lem  30130  2polcon4bN  30180  ispsubcl2N  30209  lhpat3  30308  lautcvr  30354  ltrnid  30397  trlval2  30425  trlatn0  30434  ltrnideq  30437  trlnidatb  30439  cdlemeg49lebilem  30801  trlord  30831  cdlemg1a  30832  cdlemg1cex  30850  tendoid0  31087  dva1dim  31247  cdlemm10N  31381  diarnN  31392  cdlemn  31475  dihlspsnssN  31595  dihatexv  31601  dochkrshp  31649  dochkrshp4  31652  djhlsmcl  31677  lcfl6  31763  lcfl8  31765  lcfrvalsnN  31804  lcfrlem9  31813  mapdval2N  31893  mapdordlem2  31900  mapd1o  31911  mapd0  31928  mapdheq2biN  31993
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 177
  Copyright terms: Public domain W3C validator