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  1698  equequ1OLD  1699  elequ1  1730  elequ2  1732  19.21t  1815  19.23t  1820  19.23tOLD  1840  19.21tOLD  1888  sbequ12  1947  cbv2h  1982  dral1  2060  dral1OLD  2061  ax11b  2085  sbequ  2115  sbft  2119  sbftOLD  2120  sbiedOLD  2157  sb56  2180  sbal1  2209  exsb  2213  dral1-o  2237  eupickb  2352  eupickbi  2353  2eu2  2368  ceqsalt  2984  ceqex  3072  mob2  3120  reu6  3129  sbciegft  3197  eqsbc3r  3227  csbiebt  3286  sseq1  3355  reupick  3610  reupick2  3612  uneqdifeq  3740  prnebg  4003  disjeq2  4211  disjeq1  4214  disjxiun  4234  disjss3  4236  copsexg  4471  euotd  4486  poeq2  4536  sotric  4558  sotrieq  4559  freq2  4582  seeq1  4583  seeq2  4584  tz7.7  4636  ordtri1  4643  ordtri3  4646  ordelinel  4709  reusv2lem2  4754  reusv2lem3  4755  alxfr  4765  ralxfrd  4766  oneqmin  4814  ordsuc  4823  ordelsuc  4829  ordsucelsuc  4831  ordunisuc2  4853  limsuc  4858  iss  5218  iotaval  5458  funeq  5502  funssres  5522  tz6.12c  5779  fnbrfvb  5796  ssimaex  5817  fvimacnv  5874  elpreima  5879  eldmrexrnb  5906  fsn  5935  fconst2g  5975  fconst5  5978  elunirnALT  6029  f1ocnvfvb  6046  foeqcnvco  6056  f1eqcocnv  6057  fliftfun  6063  soisores  6076  isofr  6091  isose  6092  isopo  6095  isoso  6097  f1oiso2  6101  oprabid  6134  f1opw2  6327  op1steq  6420  rntpos  6521  eusvobj2  6611  smoiso2  6660  seqomlem2  6737  oaord  6819  oawordex  6829  oaordex  6830  omord2  6839  om00  6847  oeord  6860  nnaord  6891  nnmord  6904  nnawordex  6909  nnaordex  6910  erexb  6959  swoord1  6963  swoord2  6964  iiner  7005  eceqoveq  7038  omxpenlem  7238  domtriord  7282  mapxpen  7302  mapunen  7305  ssenen  7310  nneneq  7319  onomeneq  7325  nndomo  7329  fodomfib  7415  f1opwfi  7439  elfiun  7464  suplub2  7495  ordiso2  7513  ordiso  7514  oieu  7537  brwdom2  7570  brwdom3  7579  cantnfreslem  7660  cantnflem1  7674  cardidm  7877  carddom2  7895  pm54.43  7918  pr2ne  7920  acnen  7965  acnen2  7967  alephord  7987  alephinit  8007  dfac5  8040  infdif2  8121  fictb  8156  coflim  8172  fincssdom  8234  fin23lem25  8235  isf32lem9  8272  isf34lem4  8288  fin1a2lem11  8321  axdc3lem2  8362  ficard  8471  fpwwe2lem12  8547  fpwwe2  8549  indpi  8815  nqereq  8843  1idpr  8937  ltapr  8953  leltne  9195  ltlen  9206  ltadd2  9208  ltord1  9584  mul0or  9693  ltmul1  9891  lt2msq  9925  nnsub  10069  nn0sub  10301  zrevaddcl  10352  zltp1le  10356  zdiv  10371  nneo  10384  zeo2  10387  zmax  10602  zbtwnre  10603  qrevaddcl  10627  xrlttri  10763  xrleltne  10769  xralrple  10822  xltneg  10834  xleadd1  10865  xlemul1  10900  supxrunb1  10929  supxrunb2  10930  ioo0  10972  iccid  10992  ico0  10993  ioc0  10994  icc0  10995  difreicc  11059  iccsplit  11060  0fz1  11105  uzsplit  11149  fzm1  11158  fzrevral  11162  elfznelfzob  11224  flge  11245  modid2  11302  seqf1olem1  11393  hashen  11662  hashdom  11684  hashle00  11700  hash2prb  11720  hashtpg  11722  shftlem  11914  shftuz  11915  abslt  12149  absle  12150  rexico  12188  cau3lem  12189  rlim2lt  12322  rlim3  12323  o1lo1  12362  rlimdm  12376  climshft  12401  o1dif  12454  isercolllem2  12490  isercoll  12492  zsum  12543  fsum  12545  fsum00  12608  incexclem  12647  dvdsval2  12886  moddvds  12890  negdvdsb  12897  dvdsnegb  12898  dvdscmulr  12909  dvdsmulcr  12910  dvdssub2  12918  fzo0dvdseq  12933  bitsf1ocnv  12987  sadcaddlem  13000  bitsuz  13017  dvdsgcdb  13075  gcdeq  13083  dvdssqlem  13090  isprm2lem  13117  dvdsprime  13123  dvdsprm  13130  coprm  13131  euclemma  13139  rpexp  13151  prmdiveq  13206  odzdvds  13212  pythagtrip  13239  pc2dvds  13283  pcprmpw2  13286  pcprmpw  13287  vdwapun  13373  ramtcl2  13410  firest  13691  mrieqv2d  13895  isacs2  13909  isssc  14051  setciso  14277  posasymb  14440  pleval2  14453  pltval3  14455  lubid  14470  joinle  14481  meetle  14488  lubun  14581  clatleglb  14584  latdisd  14647  letsr  14703  gsumval2a  14813  frmdss2  14839  isgrpid2  14872  isgrpinv  14886  oddvdsnn0  15213  oddvds  15216  odeq  15219  odeq1  15227  gexdvds  15249  pgpfi  15270  pgpssslw  15279  fislw  15290  sylow3lem2  15293  lsmelvalm  15316  lsmlub  15328  lsmss1b  15330  lsmss2b  15332  efgs1b  15399  cyggenod  15525  cyggexb  15539  dprdfeq0  15611  unitmulclb  15801  dvreq1  15829  drngmul0or  15887  isabvd  15939  issrngd  15980  lssats2  16107  lspsneq0  16119  lsmelval2  16188  lvecvs0or  16211  lspsneq  16225  lspsneu  16226  lidl1el  16320  lidldvgen  16357  isnzr2  16365  rrgeq0  16381  domneq0  16388  znunit  16875  ipeq0  16900  ocvsscon  16933  pjdm2  16969  obselocv  16986  unitg  17063  tgss3  17082  clsval2  17145  isopn3  17161  elcls3  17178  opncldf1  17179  neiint  17199  neips  17208  opnneissb  17209  opnssneib  17210  opnnei  17215  tpnei  17216  opnneiid  17221  restcld  17267  restopnb  17270  tgcn  17347  tgcnp  17348  subbascn  17349  iscnp4  17358  cnpnei  17359  cncls2  17368  cncls  17369  cnntr  17370  lmss  17393  hausnei2  17448  lpcls  17459  ordtt1  17474  cmpsub  17494  tgcmp  17495  1stcelcls  17555  kgencn2  17620  ptpjpre1  17634  upxp  17686  txcn  17689  txlm  17711  tgqtop  17775  kqfvima  17793  isr0  17800  regr1lem2  17803  hmeoopn  17829  hmeocld  17830  ptuncnv  17870  fbunfip  17932  fgss2  17937  ufilb  17969  ufprim  17972  trufil  17973  cfinufil  17991  ufildr  17994  elfm2  18011  elfm3  18013  rnelfm  18016  fmfnfmlem4  18020  fmco  18024  flimtopon  18033  flimopn  18038  fbflim2  18040  flimrest  18046  flffbas  18058  cnpflf  18064  fclstopon  18075  fclsnei  18082  fclsbas  18084  fclsfnflim  18090  fclscmp  18093  ufilcmp  18095  isfcf  18097  fcfnei  18098  cnpfcf  18104  alexsubb  18108  alexsubALT  18113  cldsubg  18171  tgphaus  18177  tgpt0  18179  tsmsgsum  18199  tsmsres  18204  xbln0  18475  blssexps  18487  blssex  18488  isxms2  18509  prdsbl  18552  neibl  18562  metss  18569  met2ndc  18584  metrest  18585  metcnp3  18601  nmoeq0  18801  xrsxmet  18871  reconn  18890  iccpnfcnv  19000  fgcfil  19255  iscau4  19263  cfilres  19280  iunmbl2  19482  ismbf3d  19575  mbfaddlem  19581  i1faddlem  19614  i1fmullem  19615  ellimc3  19797  tdeglem4  20014  deg1nn0clb  20044  deg1lt0  20045  dvdsq1p  20114  plypf1  20162  0dgrb  20196  plymul0or  20229  ulmshft  20337  ulmcaulem  20341  ulmcau  20342  cosord  20465  eff1olem  20481  lognegb  20515  eflogeq  20527  logdivlt  20547  efopn  20580  cxpeq0  20600  cxpeq  20672  angpieqvd  20703  dcubic  20717  asinsinb  20768  acoscosb  20769  atantanb  20795  rlimcnp  20835  isppw  20928  isppw2  20929  vmappw  20930  isnsqf  20949  ppieq0  20990  fsumdvdsdiag  21000  dvdsppwf1o  21002  fsumfldivdiag  21006  chpeq0  21023  chteq0  21024  dchrptlem1  21079  lgsdir2lem4  21141  lgsne0  21148  lgsqr  21161  lgsdchrval  21162  lgsquadlem1  21169  m1lgs  21177  ausisusgra  21411  nbgraf1olem5  21486  edgusgranbfin  21490  nb3graprlem1  21491  cusgrarn  21499  nbcusgra  21503  cusgrafilem2  21520  uvtxnbgra  21533  spthonepeq  21618  3v3e3cycl  21683  eupath2lem3  21732  grpoinvf  21859  rngosn3  22045  rngosn4  22046  rngoueqz  22049  rngoridfz  22054  nvmul0or  22164  nvz  22189  diporthcom  22246  ubthlem3  22405  hvmul0or  22558  his6  22632  hial0  22635  hial02  22636  orthcom  22641  normgt0  22660  ocin  22829  occon3  22830  shsel3  22848  shlub  22947  chssoc  23029  h1de2bi  23087  spansncol  23101  elspansn4  23106  spansnss2  23108  sumspansn  23182  lnopcnbd  23570  lnfncnbd  23591  riesz1  23599  elpjrn  23724  cvcon3  23818  dmdmd  23834  dmdbr3  23839  dmdbr4  23840  dmdbr5  23842  mdslmd1i  23863  atcveq0  23882  chcv1  23889  atssma  23912  atcv0eq  23913  atcv1  23914  bian1d  23981  xaddeq0  24150  eliccelico  24171  elicoelioo  24172  pstmfval  24322  unitdivcld  24330  xrge0iifcnv  24350  lmxrge0  24368  indf1ofs  24454  dstfrvunirn  24763  cvmliftmolem2  25000  cvmlift2lem12  25032  ghomf1olem  25136  climuzcnv  25139  relexpindlem  25170  mulge0b  25222  zprod  25294  fprod  25298  br8  25410  br6  25411  br4  25412  funbreq  25426  fprb  25428  axext4dist  25459  nodenselem8  25674  dfrdg4  25826  brbtwn  25869  brcgr  25870  brbtwn2  25875  axcontlem7  25940  cgrcom  25955  cgrcoml  25961  cgrdegen  25969  btwncom  25979  brsegle  26073  brsegle2  26074  colinbtwnle  26083  btwnoutside  26090  broutsideof3  26091  outsidele  26097  lineunray  26112  lineelsb2  26113  elhf2  26147  ontgval  26212  ordtop  26217  ordcmp  26228  nndivsub  26238  wl-bibi1  26254  cnambfre  26291  itg2addnc  26297  elicc3  26358  nn0prpwlem  26363  opnbnd  26366  cldbnd  26367  opnregcld  26371  cldregopn  26372  fnessref  26411  refssfne  26412  locfincmp  26422  neibastop2  26428  fnemeet2  26434  fnejoin2  26436  fgmin  26437  brabg2  26455  istotbnd3  26518  sstotbnd2  26521  sstotbnd  26522  sstotbnd3  26523  ssbnd  26535  ismtybnd  26554  reheibor  26586  grpoeqdivid  26594  grpokerinj  26598  1idl  26674  0rngo  26675  divrngidl  26676  igenval2  26714  ispridlc  26718  isdmn3  26722  prtlem10  26752  prter2  26768  ralxpmap  26780  elrfi  26786  diophrw  26855  eldioph2b  26859  diophin  26869  rexrabdioph  26892  rmxycomplete  27018  coprmdvdsb  27090  jm2.19  27102  jm2.26  27111  jm2.27  27117  limsuc2  27153  islinds4  27320  dgraa0p  27369  rngunsnply  27393  fiuneneq  27528  hashgcdlem  27531  dvconstbi  27566  expgrowth  27567  ax10ext  27621  pm14.24  27647  sbiota1  27649  sigarcol  27868  rexsb  27960  2reu2  27979  ralbinrald  27991  rlimdmafv  28055  ralxfrd2  28111  2ffzoeq  28187  euhash1  28214  uvtxnb  28355  usgra2pth  28373  wlkiswwlk  28404  wlklniswwlkn  28407  el2wlkonot  28425  el2spthonot  28426  el2wlkonotot0  28428  el2wlksotot  28438  usg2wlkonot  28439  usg2spthonot  28444  usg2spthonot0  28445  nbhashuvtx  28456  uvtxhashnb  28457  0eusgraiff0rgra  28474  cusgraiffrusgra  28475  frgra3vlem2  28489  frgrancvvdeqlem3  28519  sbcim2g  28721  sineq0ALT  29147  bnj145  29192  dral1NEW7  29591  cbv2hwAUX7  29611  sbiedNEW7  29638  sbftNEW7  29654  sbequNEW7  29678  sb8dwAUX7  29688  sb56NEW7  29694  exsbNEW7  29697  sbal1NEW7  29713  ax11bNEW7  29720  cbv2hOLD7  29819  lubunNEW  29869  lshpinN  29885  lsatcveq0  29928  lsatcv0eq  29943  lsatcv1  29944  islshpcv  29949  lkr0f  29990  lkrshp4  30004  lshpkrlem1  30006  lshpset2N  30015  lfl1dim  30017  lfl1dim2N  30018  lub0N  30085  glb0N  30089  oplecon3b  30096  cmtcomN  30145  cmtbr3N  30150  cmtbr4N  30151  cvrnbtwn2  30171  cvrnbtwn3  30172  cvrcon3b  30173  cvrnbtwn4  30175  cvrcmp  30179  atcvreq0  30210  atnle  30213  atlatle  30216  cvlexchb1  30226  cvlcvr1  30235  hlrelat2  30298  exatleN  30299  cvrval3  30308  cvrval4N  30309  cvrexch  30315  atcvr0eq  30321  lnnat  30322  atcvrj0  30323  atcvrj2b  30327  atltcvr  30330  atbtwn  30341  ps-1  30372  3at  30385  islln2a  30412  llncmp  30417  islpln2a  30443  lplncmp  30457  islvol2aN  30487  4at  30508  lvolcmp  30512  pmaple  30656  lncmp  30678  paddss  30740  llnexchb2lem  30763  2polcon4bN  30813  ispsubcl2N  30842  lhpat3  30941  lautcvr  30987  ltrnid  31030  trlval2  31058  trlatn0  31067  ltrnideq  31070  trlnidatb  31072  cdlemeg49lebilem  31434  trlord  31464  cdlemg1a  31465  cdlemg1cex  31483  tendoid0  31720  dva1dim  31880  cdlemm10N  32014  diarnN  32025  cdlemn  32108  dihlspsnssN  32228  dihatexv  32234  dochkrshp  32282  dochkrshp4  32285  djhlsmcl  32310  lcfl6  32396  lcfl8  32398  lcfrvalsnN  32437  lcfrlem9  32446  mapdval2N  32526  mapdordlem2  32533  mapd1o  32544  mapd0  32561  mapdheq2biN  32626
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