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

Theorem notbid 286
Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)
Hypothesis
Ref Expression
notbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
notbid  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)

Proof of Theorem notbid
StepHypRef Expression
1 notbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 notnot 283 . . 3  |-  ( ps  <->  -. 
-.  ps )
3 notnot 283 . . 3  |-  ( ch  <->  -. 
-.  ch )
41, 2, 33bitr3g 279 . 2  |-  ( ph  ->  ( -.  -.  ps  <->  -. 
-.  ch ) )
54con4bid 285 1  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  notbi  287  con3th  925  nanbi1  1301  xorbi12d  1321  cbvexvw  1713  hba1w  1718  hbe1w  1719  equsexOLD  1970  ax10lem2OLD  1992  ax9OLD  1999  drex1  2024  cbvex  2038  cbvexd  2059  ax11inda  2250  eujustALT  2257  2mo  2332  neeq1  2575  neeq2  2576  necon3abid  2600  neleq1  2660  neleq2  2661  cbvrexf  2887  gencbval  2960  spcegf  2992  spc2gv  2999  spc3gv  3001  cdeqnot  3109  ru  3120  sbcng  3161  sbcrext  3194  sbcnel12g  3228  cbvrexcsf  3272  difjust  3282  eldif  3290  dfpss3  3393  difeq2  3419  disjne  3633  pssdifcom1  3673  pssdifcom2  3674  prel12  3935  disjxun  4170  nalset  4300  pwnss  4325  dtru  4350  dtruALT  4356  dtruALT2  4368  poeq1  4466  pocl  4470  swopo  4473  sotric  4489  sotrieq  4490  isso2i  4495  somo  4497  freq1  4512  frirr  4519  fr2nr  4520  frminex  4522  tz7.2  4526  wereu2  4539  nordeq  4560  ordtri1  4574  ordtri3  4577  rexxfrd  4697  rexxfr2d  4699  rexxfr  4702  elpwunsn  4716  fr3nr  4719  dfwe2  4721  ordsucsssuc  4762  nlimsucg  4781  orduninsuc  4782  dfom2  4806  ssnlim  4822  poinxp  4900  frinxp  4902  posn  4905  frsn  4907  rexiunxp  4974  rexxpf  4979  intirr  5211  poirr2  5217  cnvpo  5369  fvmpti  5764  fndmdif  5793  rexrnmpt  5838  f1imapss  5971  cbvexfo  5982  soisoi  6007  isopolem  6024  f1oweALT  6033  weniso  6034  rexrnmpt2  6144  ndmovg  6189  frxp  6415  poxp  6417  sorpssuni  6490  sorpssint  6491  canth  6498  riotaclbg  6548  smoword  6587  tz7.48lem  6657  abianfp  6675  oacan  6750  oaword  6751  omlimcl  6780  omeulem1  6784  nnaword  6829  nnmword  6835  nneob  6854  brdifun  6891  swoer  6892  undifixp  7057  boxcutc  7064  2dom  7138  php  7250  nndomo  7259  nnsdomo  7260  unxpdomlem2  7273  frfi  7311  unfilem1  7330  supmo  7413  eqsup  7417  supub  7420  supmaxlem  7425  suppr  7429  supisolem  7431  supisoex  7432  oieq1  7437  ordtypecbv  7442  ordtypelem7  7449  wemapso2lem  7475  canthwdom  7503  zfregcl  7518  elirrv  7521  elirr  7522  noinfep  7570  noinfepOLD  7571  cantnfp1lem3  7592  rankr1clem  7702  carden2b  7810  domtri2  7832  alephord3  7915  alephdom2  7924  alephval3  7947  dfac9  7972  kmlem2  7987  kmlem4  7989  isfin4  8133  isfin7  8137  fin23lem11  8153  isf32lem5  8193  isf34lem4  8213  fin1a2lem6  8241  fin1a2lem7  8242  fin1a2lem12  8247  itunisuc  8255  ac6n  8321  zorn2g  8339  zornn0g  8341  ttukeylem7  8351  axpowndlem2  8429  axpowndlem3  8430  axpowndlem4  8431  axregnd  8435  elgch  8453  engch  8459  fpwwe2lem13  8473  fpwwe2  8474  pwfseqlem1  8489  pwfseqlem3  8491  hargch  8508  addnidpi  8734  pinq  8760  nqereu  8762  ltsonq  8802  prlem934  8866  ltexprlem7  8875  addcanpr  8879  prlem936  8880  reclem2pr  8881  reclem3pr  8882  supexpr  8887  ltsosr  8925  supsrlem  8942  axpre-lttri  8996  axpre-sup  9000  xrlenlt  9099  axlttri  9103  axsup  9107  ltne  9126  readdcan  9196  leadd1  9452  ltsub1  9480  ltsub2  9481  leord1  9510  lediv1  9831  lemuldiv  9845  lerec  9848  le2msq  9866  lbinfm  9917  infm3  9923  suprnub  9927  infmrgelb  9944  infmrlb  9945  avgle1  10163  avgle2  10164  znnnlt1  10264  indstr  10501  zsupss  10521  uzsupss  10524  rpneg  10597  xralrple  10747  xleneg  10760  xltadd1  10791  xposdif  10797  xmulneg1  10804  xltmul1  10827  xrsupexmnf  10839  xrinfmexpnf  10840  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxrleub  10861  infmxrgelb  10869  difreicc  10984  elfznelfzo  11147  injresinjlem  11154  leexp2  11389  hashbnd  11579  hasheni  11587  hashbc  11657  cnpart  12000  sqrlt  12022  limsuplt  12228  rlimrege0  12328  isercoll  12416  efle  12674  odd2np1  12863  divalglem7  12874  ndvdsadd  12883  bitsfval  12890  bitsval  12891  bits0  12895  bitsp1  12898  bitsmod  12903  bitscmp  12905  bitsinv1lem  12908  sadadd2lem2  12917  saddisjlem  12931  bitsshft  12942  gcdneg  12981  algcvgblem  13023  isprm3  13043  isprm5  13067  rpexp  13075  phiprmpw  13120  pythagtrip  13163  pcgcd1  13205  prmpwdvds  13227  prmreclem2  13240  prmreclem3  13241  prmreclem5  13243  prmreclem6  13244  vdwlem6  13309  vdwnnlem2  13319  vdwnnlem3  13320  vdwnn  13321  prmlem0  13383  prmlem1a  13384  divsfval  13727  mrisval  13810  ismri  13811  ismri2dad  13817  cidpropd  13891  plttr  14382  acsfiindd  14558  sylow1lem3  15189  sylow2alem2  15207  efgsfo  15326  ablfac1eulem  15585  ablfac1eu  15586  pgpfac1lem1  15587  pgpfac1lem5  15592  islbs  16103  lbsind  16107  lbspss  16109  lbspropd  16126  lspsnne1  16144  islbs2  16181  lbsacsbs  16183  lbsextlem1  16185  lbsextlem3  16187  lbsextlem4  16188  lbsextg  16189  nzrunit  16292  opsrtoslem2  16500  elcls  17092  maxlp  17165  perfi  17173  ordtbaslem  17206  ordtval  17207  ordtbas2  17209  ordtopn1  17212  ordtopn2  17213  ordtcnv  17219  ordtrest  17220  ordtrest2lem  17221  ordtrest2  17222  pnfnei  17238  mnfnei  17239  isreg2  17395  ordthauslem  17401  cmpfi  17425  cmpfii  17426  nconsubb  17439  hausdiag  17630  txkgen  17637  kqdisj  17717  ordthmeolem  17786  fbfinnfr  17826  trfbas  17829  fbunfip  17854  fbasrn  17869  trfil3  17873  ufileu  17904  fin1aufil  17917  hausflim  17966  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem2  18037  ptcmplem3  18038  stdbdbl  18500  iccntr  18805  reconnlem2  18811  iccpnfcnv  18922  xrhmeo  18924  lebnumlem1  18939  lebnumlem2  18940  lebnumlem3  18941  bcthlem4  19233  minveclem3b  19282  ivthlem2  19302  ivthlem3  19303  mbfmax  19494  mbfposr  19497  i1fd  19526  mbfi1fseqlem4  19563  itg2splitlem  19593  itg2monolem1  19595  itg2cnlem1  19606  dvne0  19848  lhop1lem  19850  deg1nn0clb  19966  dgrle  20115  coemulhi  20125  aaliou3lem9  20220  cos11  20388  logleb  20451  argrege0  20459  logdivle  20470  ellogdm  20483  cxple  20539  cxplt2  20542  cxple3  20545  isosctrlem1  20615  atandm  20669  atans2  20724  atantayl2  20731  ftalem7  20814  isppw2  20851  musum  20929  dchrsum2  21005  bposlem1  21021  lgsmod  21058  lgsdir2lem2  21061  lgsdir2  21065  lgsne0  21070  lgsquadlem1  21091  rpvmasumlem  21134  padicabv  21277  ostth3  21285  ostth  21286  usgra1v  21362  usgraidx2v  21365  nbgra0nb  21394  cusgrafilem3  21443  spthispth  21526  wlkdvspthlem  21560  eupath2lem3  21654  eupath2  21655  konigsberg  21662  lpni  21720  nmobndseqi  22233  minvecolem5  22336  chpsscon3  22958  chnle  22969  nonbooli  23106  pjnel  23181  specval  23354  nmcfnlbi  23508  stri  23713  hstri  23721  cvbr  23738  cvcon3  23740  chcv1  23811  cvexchlem  23824  chrelat2  23826  elpreq  23952  ifeqeqx  23954  ifbieq12d2  23955  isoun  24042  eliccelico  24093  elicoelioo  24094  toslub  24144  tosglb  24145  isarchi2  24208  xrge0iifcnv  24272  elzdif0  24317  eldifpr  24345  eldiftp  24346  esumpcvgval  24421  ballotlemfc0  24703  ballotlemfcc  24704  ballotlem4  24709  ballotlemimin  24716  ballotlem7  24746  eldmgm  24759  erdszelem10  24839  untelirr  25110  untsucf  25112  untangtr  25116  dedekind  25140  inffz  25153  dfpo2  25326  dfon2lem3  25355  dfon2lem4  25356  dfon2lem7  25359  dfon2lem9  25361  distel  25374  predpoirr  25411  predfrirr  25412  soseq  25468  nodenselem4  25552  nodenselem5  25553  nocvxminlem  25558  nofulllem4  25573  funpartfv  25698  dfrdg4  25703  axlowdimlem16  25800  axlowdim2  25803  axlowdim  25804  limsucncmpi  26099  limsucncmp  26100  ordcmp  26101  leceifl  26141  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  cnambfre  26154  itg2addnclem  26155  itg2addnclem2  26156  iblabsnclem  26167  areacirc  26187  nn0prpwlem  26215  nn0prpw  26216  heibor1lem  26408  heiborlem1  26410  heiborlem6  26415  heiborlem8  26417  heiborlem10  26419  smprngopr  26552  ellz1  26715  rencldnfilem  26771  jm2.22  26956  jm2.23  26957  wepwsolem  27006  fnwe2lem2  27016  supeq123d  27026  aomclem8  27027  frlmlbs  27117  unxpwdom3  27124  islindf  27150  islinds2  27151  islindf2  27152  lindfind  27154  lindsind  27155  lindfrn  27159  lindfmm  27165  lsslindf  27168  islindf4  27176  psgnunilem1  27284  psgnunilem5  27285  psgnunilem2  27286  psgnunilem3  27287  rusbcALT  27507  xrltneNEW  27524  stoweidlem14  27630  stoweidlem34  27650  stoweidlem59  27675  eu2ndop1stv  27847  afvfv0bi  27883  afvco2  27907  ndmaovg  27915  otiunsndisj  27954  otiunsndisjX  27955  2f1fvneq  27958  swrdnd  28001  swrdccat3  28029  swrdccat3b  28031  frgra2v  28103  frgrancvvdeqlem2  28134  2spotiundisj  28165  usg2spot2nb  28168  2spotmdisj  28171  en3lpVD  28666  bnj23  28789  bnj1185  28871  bnj1476  28924  bnj1228  29086  bnj1388  29108  bnj1417  29116  ax9NEW7  29174  equsexNEW7  29196  drex1NEW7  29200  cbvexwAUX7  29224  cbvexOLD7  29410  cbvexdOLD7  29419  lcvfbr  29503  lcvbr  29504  lsatcv0  29514  l1cvpat  29537  opltcon3b  29687  cvrfval  29751  cvrval  29752  cvrnbtwn  29754  cvrval2  29757  cvrnbtwn2  29758  cvrnbtwn3  29759  cvrcon3b  29760  cvrnbtwn4  29762  atnlt  29796  iscvlat  29806  cvlexch1  29811  hlsuprexch  29863  hlrelat5N  29883  hlrelat2  29885  cvrval5  29897  3dimlem1  29940  3dim1lem5  29948  3dim2  29950  3dim3  29951  llnnlt  30005  islpln5  30017  lplni2  30019  lvolex3N  30020  lplnnle2at  30023  islpln2a  30030  lplnribN  30033  lplnexllnN  30046  lplnnlt  30047  lvoli3  30059  islvol5  30061  lvoli2  30063  lvolnle3at  30064  islvol2aN  30074  4atlem11  30091  lvolnltN  30100  dalawlem15  30367  4atexlemex2  30553  4atex  30558  4atex2-0aOLDN  30560  4atex2-0cOLDN  30562  lautcvr  30574  ltrnfset  30599  ltrnset  30600  ltrnu  30603  trlfset  30642  trlset  30643  trlval2  30645  cdlemd6  30685  cdleme0nex  30772  cdleme18d  30777  cdleme25b  30836  cdleme25cv  30840  cdleme29b  30857  cdleme31fv  30872  cdleme31fv2  30875  cdlemefrs29bpre0  30878  cdlemefr32sn2aw  30886  cdlemefr29bpre0N  30888  cdlemefr29clN  30889  cdlemefr32fvaN  30891  cdlemefr32fva1  30892  cdlemefs32sn1aw  30896  cdleme32fva  30919  cdleme32fvaw  30921  cdleme40v  30951  cdleme42b  30960  cdleme46f2g2  30975  cdleme46f2g1  30976  cdleme48gfv  31019  cdlemg1fvawlemN  31055  cdlemg1cex  31070  cdlemg6d  31103  cdlemm10N  31601  dicffval  31657  dicfval  31658  dicval  31659  dicfnN  31666  dicvalrelN  31668  dihffval  31713  dihfval  31714  dihlsscpre  31717  dvh4dimat  31921  dvh3dimatN  31922  dvh4dimlem  31926  dvh3dim  31929  dvh4dimN  31930  dvh3dim2  31931  dvh3dim3N  31932  mapdcv  32143  mapdh9aOLDN  32274  hdmapfval  32313  hdmapval  32314  hdmapval2  32318  hdmap11lem2  32328
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