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  1710  hba1w  1714  hbe1w  1715  equsexOLD  1958  ax10lem2OLD  1983  ax9OLD  1989  drex1  2006  cbvex  2020  cbvexd  2043  ax11inda  2234  eujustALT  2241  2mo  2316  neeq1  2558  neeq2  2559  necon3abid  2583  neleq1  2643  neleq2  2644  cbvrexf  2870  gencbval  2943  spcegf  2975  spc2gv  2982  spc3gv  2984  cdeqnot  3092  ru  3103  sbcng  3144  sbcrext  3177  sbcnel12g  3211  cbvrexcsf  3255  difjust  3265  eldif  3273  dfpss3  3376  difeq2  3402  disjne  3616  pssdifcom1  3656  pssdifcom2  3657  prel12  3917  disjxun  4151  nalset  4281  pwnss  4306  dtru  4331  dtruALT  4337  dtruALT2  4349  poeq1  4447  pocl  4451  swopo  4454  sotric  4470  sotrieq  4471  isso2i  4476  somo  4478  freq1  4493  frirr  4500  fr2nr  4501  frminex  4503  tz7.2  4507  wereu2  4520  nordeq  4541  ordtri1  4555  ordtri3  4558  rexxfrd  4678  rexxfr2d  4680  rexxfr  4683  elpwunsn  4697  fr3nr  4700  dfwe2  4702  ordsucsssuc  4743  nlimsucg  4762  orduninsuc  4763  dfom2  4787  ssnlim  4803  poinxp  4881  frinxp  4883  posn  4886  frsn  4888  rexiunxp  4955  rexxpf  4960  intirr  5192  poirr2  5198  cnvpo  5350  fvmpti  5744  fndmdif  5773  rexrnmpt  5818  f1imapss  5951  cbvexfo  5962  soisoi  5987  isopolem  6004  f1oweALT  6013  weniso  6014  rexrnmpt2  6124  ndmovg  6169  frxp  6392  poxp  6394  sorpssuni  6467  sorpssint  6468  canth  6475  riotaclbg  6525  smoword  6564  tz7.48lem  6634  abianfp  6652  oacan  6727  oaword  6728  omlimcl  6757  omeulem1  6761  nnaword  6806  nnmword  6812  nneob  6831  brdifun  6868  swoer  6869  undifixp  7034  boxcutc  7041  2dom  7115  php  7227  nndomo  7236  nnsdomo  7237  unxpdomlem2  7250  frfi  7288  unfilem1  7307  supmo  7390  eqsup  7394  supub  7397  supmaxlem  7402  suppr  7406  supisolem  7408  supisoex  7409  oieq1  7414  ordtypecbv  7419  ordtypelem7  7426  wemapso2lem  7452  canthwdom  7480  zfregcl  7495  elirrv  7498  elirr  7499  noinfep  7547  noinfepOLD  7548  cantnfp1lem3  7569  rankr1clem  7679  carden2b  7787  domtri2  7809  alephord3  7892  alephdom2  7901  alephval3  7924  dfac9  7949  kmlem2  7964  kmlem4  7966  isfin4  8110  isfin7  8114  fin23lem11  8130  isf32lem5  8170  isf34lem4  8190  fin1a2lem6  8218  fin1a2lem7  8219  fin1a2lem12  8224  itunisuc  8232  ac6n  8298  zorn2g  8316  zornn0g  8318  ttukeylem7  8328  axpowndlem2  8406  axpowndlem3  8407  axpowndlem4  8408  axregnd  8412  elgch  8430  engch  8436  fpwwe2lem13  8450  fpwwe2  8451  pwfseqlem1  8466  pwfseqlem3  8468  hargch  8485  addnidpi  8711  pinq  8737  nqereu  8739  ltsonq  8779  prlem934  8843  ltexprlem7  8852  addcanpr  8856  prlem936  8857  reclem2pr  8858  reclem3pr  8859  supexpr  8864  ltsosr  8902  supsrlem  8919  axpre-lttri  8973  axpre-sup  8977  xrlenlt  9076  axlttri  9080  axsup  9084  ltne  9103  readdcan  9172  leadd1  9428  ltsub1  9456  ltsub2  9457  leord1  9486  lediv1  9807  lemuldiv  9821  lerec  9824  le2msq  9842  lbinfm  9893  infm3  9899  suprnub  9903  infmrgelb  9920  infmrlb  9921  avgle1  10139  avgle2  10140  znnnlt1  10240  indstr  10477  zsupss  10497  uzsupss  10500  rpneg  10573  xralrple  10723  xleneg  10736  xltadd1  10767  xposdif  10773  xmulneg1  10780  xltmul1  10803  xrsupexmnf  10815  xrinfmexpnf  10816  xrsupsslem  10817  xrinfmsslem  10818  xrub  10822  supxrleub  10837  infmxrgelb  10845  difreicc  10960  elfznelfzo  11119  injresinjlem  11126  leexp2  11361  hashbnd  11551  hasheni  11559  hashbc  11629  cnpart  11972  sqrlt  11994  limsuplt  12200  rlimrege0  12300  isercoll  12388  efle  12646  odd2np1  12835  divalglem7  12846  ndvdsadd  12855  bitsfval  12862  bitsval  12863  bits0  12867  bitsp1  12870  bitsmod  12875  bitscmp  12877  bitsinv1lem  12880  sadadd2lem2  12889  saddisjlem  12903  bitsshft  12914  gcdneg  12953  algcvgblem  12995  isprm3  13015  isprm5  13039  rpexp  13047  phiprmpw  13092  pythagtrip  13135  pcgcd1  13177  prmpwdvds  13199  prmreclem2  13212  prmreclem3  13213  prmreclem5  13215  prmreclem6  13216  vdwlem6  13281  vdwnnlem2  13291  vdwnnlem3  13292  vdwnn  13293  prmlem0  13355  prmlem1a  13356  divsfval  13699  mrisval  13782  ismri  13783  ismri2dad  13789  cidpropd  13863  plttr  14354  acsfiindd  14530  sylow1lem3  15161  sylow2alem2  15179  efgsfo  15298  ablfac1eulem  15557  ablfac1eu  15558  pgpfac1lem1  15559  pgpfac1lem5  15564  islbs  16075  lbsind  16079  lbspss  16081  lbspropd  16098  lspsnne1  16116  islbs2  16153  lbsacsbs  16155  lbsextlem1  16157  lbsextlem3  16159  lbsextlem4  16160  lbsextg  16161  nzrunit  16264  opsrtoslem2  16472  elcls  17060  maxlp  17133  perfi  17141  ordtbaslem  17174  ordtval  17175  ordtbas2  17177  ordtopn1  17180  ordtopn2  17181  ordtcnv  17187  ordtrest  17188  ordtrest2lem  17189  ordtrest2  17190  pnfnei  17206  mnfnei  17207  isreg2  17363  ordthauslem  17369  cmpfi  17393  cmpfii  17394  nconsubb  17407  hausdiag  17598  txkgen  17605  kqdisj  17685  ordthmeolem  17754  fbfinnfr  17794  trfbas  17797  fbunfip  17822  fbasrn  17837  trfil3  17841  ufileu  17872  fin1aufil  17885  hausflim  17934  alexsubALTlem2  18000  alexsubALTlem3  18001  alexsubALTlem4  18002  ptcmplem2  18005  ptcmplem3  18006  stdbdbl  18437  iccntr  18723  reconnlem2  18729  iccpnfcnv  18840  xrhmeo  18842  lebnumlem1  18857  lebnumlem2  18858  lebnumlem3  18859  bcthlem4  19149  minveclem3b  19196  ivthlem2  19216  ivthlem3  19217  mbfmax  19408  mbfposr  19411  i1fd  19440  mbfi1fseqlem4  19477  itg2splitlem  19507  itg2monolem1  19509  itg2cnlem1  19520  dvne0  19762  lhop1lem  19764  deg1nn0clb  19880  dgrle  20029  coemulhi  20039  aaliou3lem9  20134  cos11  20302  logleb  20365  argrege0  20373  logdivle  20384  ellogdm  20397  cxple  20453  cxplt2  20456  cxple3  20459  isosctrlem1  20529  atandm  20583  atans2  20638  atantayl2  20645  ftalem7  20728  isppw2  20765  musum  20843  dchrsum2  20919  bposlem1  20935  lgsmod  20972  lgsdir2lem2  20975  lgsdir2  20979  lgsne0  20984  lgsquadlem1  21005  rpvmasumlem  21048  padicabv  21191  ostth3  21199  ostth  21200  usgra1v  21275  usgraidx2v  21278  nbusgra  21306  nbgra0nb  21307  cusgrafilem3  21356  spthispth  21427  wlkdvspthlem  21455  eupath2lem3  21549  eupath2  21550  konigsberg  21557  lpni  21615  nmobndseqi  22128  minvecolem5  22231  chpsscon3  22853  chnle  22864  nonbooli  23001  pjnel  23076  specval  23249  nmcfnlbi  23403  stri  23608  hstri  23616  cvbr  23633  cvcon3  23635  chcv1  23706  cvexchlem  23719  chrelat2  23721  elpreq  23843  ifeqeqx  23845  ifbieq12d2  23846  isoun  23930  eliccelico  23976  elicoelioo  23977  xrge0iifcnv  24123  elzdif0  24163  eldifpr  24188  eldiftp  24189  esumpcvgval  24264  ballotlemfc0  24529  ballotlemfcc  24530  ballotlem4  24535  ballotlemimin  24542  ballotlem7  24572  eldmgm  24585  erdszelem10  24665  untelirr  24936  untsucf  24938  untangtr  24942  dedekind  24966  inffz  24979  dfpo2  25136  dfon2lem3  25165  dfon2lem4  25166  dfon2lem7  25169  dfon2lem9  25171  distel  25184  predpoirr  25221  predfrirr  25222  soseq  25278  nodenselem4  25362  nodenselem5  25363  nocvxminlem  25368  nofulllem4  25383  funpartfv  25508  dfrdg4  25513  axlowdimlem16  25610  axlowdim2  25613  axlowdim  25614  limsucncmpi  25909  limsucncmp  25910  ordcmp  25911  leceifl  25951  itg2addnclem  25957  itg2addnclem2  25958  itgaddnclem2  25964  iblabsnclem  25968  areacirc  25988  nn0prpwlem  26016  nn0prpw  26017  heibor1lem  26209  heiborlem1  26211  heiborlem6  26216  heiborlem8  26218  heiborlem10  26220  smprngopr  26353  ellz1  26516  rencldnfilem  26572  jm2.22  26757  jm2.23  26758  wepwsolem  26807  fnwe2lem2  26817  supeq123d  26827  aomclem8  26828  frlmlbs  26918  unxpwdom3  26925  islindf  26951  islinds2  26952  islindf2  26953  lindfind  26955  lindsind  26956  lindfrn  26960  lindfmm  26966  lsslindf  26969  islindf4  26977  psgnunilem1  27085  psgnunilem5  27086  psgnunilem2  27087  psgnunilem3  27088  rusbcALT  27308  xrltneNEW  27325  stoweidlem14  27431  stoweidlem34  27451  stoweidlem59  27476  eu2ndop1stv  27648  afvfv0bi  27685  afvco2  27709  ndmaovg  27717  frgra2v  27752  frgrancvvdeqlem2  27783  en3lpVD  28298  bnj23  28421  bnj1185  28503  bnj1476  28556  bnj1228  28718  bnj1388  28740  bnj1417  28748  ax9NEW7  28806  equsexNEW7  28828  drex1NEW7  28832  cbvexwAUX7  28856  cbvexOLD7  29042  cbvexdOLD7  29051  lcvfbr  29135  lcvbr  29136  lsatcv0  29146  l1cvpat  29169  opltcon3b  29319  cvrfval  29383  cvrval  29384  cvrnbtwn  29386  cvrval2  29389  cvrnbtwn2  29390  cvrnbtwn3  29391  cvrcon3b  29392  cvrnbtwn4  29394  atnlt  29428  iscvlat  29438  cvlexch1  29443  hlsuprexch  29495  hlrelat5N  29515  hlrelat2  29517  cvrval5  29529  3dimlem1  29572  3dim1lem5  29580  3dim2  29582  3dim3  29583  llnnlt  29637  islpln5  29649  lplni2  29651  lvolex3N  29652  lplnnle2at  29655  islpln2a  29662  lplnribN  29665  lplnexllnN  29678  lplnnlt  29679  lvoli3  29691  islvol5  29693  lvoli2  29695  lvolnle3at  29696  islvol2aN  29706  4atlem11  29723  lvolnltN  29732  dalawlem15  29999  4atexlemex2  30185  4atex  30190  4atex2-0aOLDN  30192  4atex2-0cOLDN  30194  lautcvr  30206  ltrnfset  30231  ltrnset  30232  ltrnu  30235  trlfset  30274  trlset  30275  trlval2  30277  cdlemd6  30317  cdleme0nex  30404  cdleme18d  30409  cdleme25b  30468  cdleme25cv  30472  cdleme29b  30489  cdleme31fv  30504  cdleme31fv2  30507  cdlemefrs29bpre0  30510  cdlemefr32sn2aw  30518  cdlemefr29bpre0N  30520  cdlemefr29clN  30521  cdlemefr32fvaN  30523  cdlemefr32fva1  30524  cdlemefs32sn1aw  30528  cdleme32fva  30551  cdleme32fvaw  30553  cdleme40v  30583  cdleme42b  30592  cdleme46f2g2  30607  cdleme46f2g1  30608  cdleme48gfv  30651  cdlemg1fvawlemN  30687  cdlemg1cex  30702  cdlemg6d  30735  cdlemm10N  31233  dicffval  31289  dicfval  31290  dicval  31291  dicfnN  31298  dicvalrelN  31300  dihffval  31345  dihfval  31346  dihlsscpre  31349  dvh4dimat  31553  dvh3dimatN  31554  dvh4dimlem  31558  dvh3dim  31561  dvh4dimN  31562  dvh3dim2  31563  dvh3dim3N  31564  mapdcv  31775  mapdh9aOLDN  31906  hdmapfval  31945  hdmapval  31946  hdmapval2  31950  hdmap11lem2  31960
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