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

Theorem notbid 294
Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)
Hypothesis
Ref Expression
notbid.1
Assertion
Ref Expression
notbid

Proof of Theorem notbid
StepHypRef Expression
1 notbid.1 . . 3
2 notnot 291 . . 3
3 notnot 291 . . 3
41, 2, 33bitr3g 287 . 2
54con4bid 293 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  notbi  295  con3th  958  nanbi1  1354  xorbi12d  1377  cbvexvw  1810  hba1w  1814  hbe1w  1815  cbvex  2022  cbvexd  2026  cbvex2  2028  drex1  2069  ax12inda  2278  eujustALT  2285  necon3abid  2703  neeq1OLD  2739  neeq2OLD  2741  neleq12d  2794  neleq1OLD  2796  neleq2OLD  2798  cbvrexf  3079  gencbval  3155  spcegf  3190  spc2gv  3197  spc3gv  3199  cdeqnot  3315  ru  3326  sbcng  3368  sbcrextOLD  3409  sbcrext  3410  cbvrexcsf  3467  difjust  3477  eldif  3485  dfpss3  3589  difeq2  3615  disjne  3872  pssdifcom1  3913  pssdifcom2  3914  eldifpr  4046  elpwunsn  4070  eldiftp  4072  prel12  4207  prel12g  4210  disjxun  4450  nalset  4589  pwnss  4617  dtru  4643  rexxfrd  4667  rexxfr2d  4669  rexxfr  4672  dtruALT  4684  dtruALT2  4696  opthneg  4731  otiunsndisj  4758  poeq1  4808  pocl  4812  swopo  4815  sotric  4831  sotrieq  4832  isso2i  4837  somo  4839  freq1  4854  frirr  4861  fr2nr  4862  frminex  4864  tz7.2  4868  wereu2  4881  nordeq  4902  ordtri1  4916  ordtri3  4919  poinxp  5068  frinxp  5070  posn  5073  frsn  5075  rexiunxp  5148  rexxpf  5155  intirr  5390  poirr2  5396  cnvpo  5550  fvmpti  5955  fndmdif  5991  rexrnmpt  6041  f1imapss  6174  cbvexfo  6193  soisoi  6224  isopolem  6241  weniso  6250  canth  6254  riotaclb  6295  rexrnmpt2  6418  ndmovg  6458  sorpssuni  6589  sorpssint  6590  fr3nr  6615  dfwe2  6617  ordsucsssuc  6658  nlimsucg  6677  orduninsuc  6678  dfom2  6702  ssnlim  6718  f1oweALT  6784  frxp  6910  poxp  6912  smoword  7056  tz7.48lem  7125  oacan  7216  oaword  7217  omlimcl  7246  omeulem1  7250  nnaword  7295  nnmword  7301  nneob  7320  brdifun  7357  swoer  7358  undifixp  7525  boxcutc  7532  2dom  7608  php  7721  nndomo  7731  nnsdomo  7732  unxpdomlem2  7745  frfi  7785  unfilem1  7804  supeq3  7929  supeq123d  7930  supmo  7932  eqsup  7936  supub  7939  supmaxlemOLD  7945  suppr  7950  supisolem  7952  supisoex  7953  oieq1  7958  ordtypecbv  7963  ordtypelem7  7970  wemapsolem  7996  canthwdom  8026  zfregcl  8041  elirrv  8044  elirr  8045  noinfep  8097  noinfepOLD  8098  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  rankr1clem  8259  carden2b  8369  domtri2  8391  alephord3  8480  alephdom2  8489  alephval3  8512  dfac9  8537  kmlem2  8552  kmlem4  8554  isfin4  8698  isfin7  8702  fin23lem11  8718  isf32lem5  8758  isf34lem4  8778  fin1a2lem6  8806  fin1a2lem7  8807  fin1a2lem12  8812  itunisuc  8820  ac6n  8886  zorn2g  8904  zornn0g  8906  ttukeylem7  8916  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axregnd  9002  axregndOLD  9003  elgch  9021  engch  9027  fpwwe2lem13  9041  fpwwe2  9042  pwfseqlem1  9057  pwfseqlem3  9059  hargch  9072  addnidpi  9300  pinq  9326  nqereu  9328  ltsonq  9368  prlem934  9432  ltexprlem7  9441  addcanpr  9445  prlem936  9446  reclem2pr  9447  reclem3pr  9448  supexpr  9453  ltsosr  9492  supsrlem  9509  axpre-lttri  9563  axpre-sup  9567  xrlenlt  9673  axlttri  9677  axsup  9681  ltne  9702  dedekind  9765  readdcan  9775  leadd1  10045  ltsub1  10073  ltsub2  10074  leord1  10105  lediv1  10432  lemuldiv  10449  lerec  10452  le2msq  10470  lbinfm  10521  infm3  10527  suprnub  10531  infmrgelb  10548  infmrlb  10549  avgle1  10803  avgle2  10804  znnnlt1  10916  indstr  11179  zsupss  11200  uzsupss  11203  rpneg  11278  xralrple  11433  xleneg  11446  xltadd1  11477  xposdif  11483  xmulneg1  11490  xltmul1  11513  xrsupexmnf  11525  xrinfmexpnf  11526  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrleub  11547  infmxrgelb  11555  difreicc  11681  nn0disj  11820  elfznelfzo  11915  injresinjlem  11925  ssnn0fi  12094  leexp2  12220  hashbnd  12411  hasheni  12421  hashbc  12502  wrdsymb0  12575  lsw0  12586  lswccatn0lsw  12607  swrdnd  12657  swrdvalodm2  12664  swrdvalodm  12665  repswswrd  12756  repswccat  12757  cshwidxmod  12774  cnpart  13073  sqrtlt  13095  limsuplt  13302  rlimrege0  13402  isercoll  13490  efle  13853  odd2np1  14046  divalglem7  14057  ndvdsadd  14066  bitsfval  14073  bitsval  14074  bits0  14078  bitsp1  14081  bitsmod  14086  bitscmp  14088  bitsinv1lem  14091  sadadd2lem2  14100  saddisjlem  14114  bitsshft  14125  gcdneg  14164  algcvgblem  14206  isprm3  14226  isprm5  14253  rpexp  14261  phiprmpw  14306  m1dvdsndvds  14325  pythagtrip  14358  pcgcd1  14400  prmpwdvds  14422  prmreclem2  14435  prmreclem3  14436  prmreclem5  14438  prmreclem6  14439  vdwlem6  14504  vdwnnlem2  14514  vdwnnlem3  14515  vdwnn  14516  prmlem0  14591  prmlem1a  14592  divsfval  14944  mrisval  15027  ismri  15028  ismri2dad  15034  cidpropd  15105  plttr  15600  joinval  15635  meetval  15649  acsfiindd  15807  isnsgrp  15915  mgm2nsgrplem2  16037  sgrp2nmndlem3  16043  symgfix2  16441  pmtrdifellem4  16504  psgnunilem1  16518  psgnunilem5  16519  psgnunilem2  16520  psgnunilem3  16521  pmtrsn  16544  sylow1lem3  16620  sylow2alem2  16638  efgsfo  16757  ablfac1eulem  17123  ablfac1eu  17124  pgpfac1lem1  17125  pgpfac1lem5  17130  islbs  17722  lbsind  17726  lbspss  17728  lbspropd  17745  lspsnne1  17763  islbs2  17800  lbsacsbs  17802  lbsextlem1  17804  lbsextlem3  17806  lbsextlem4  17807  lbsextg  17808  nzrunit  17915  opsrtoslem2  18149  cply1coe0  18341  cply1coe0bi  18342  frlmlbs  18831  islindf  18847  islinds2  18848  islindf2  18849  lindfind  18851  lindsind  18852  lindfrn  18856  lindfmm  18862  lsslindf  18865  islindf4  18873  mdetunilem7  19120  mdetunilem8  19121  mdetunilem9  19122  maducoeval2  19142  pmatcollpw3fi1lem1  19287  fvmptnn04ifa  19351  fvmptnn04ifc  19353  fvmptnn04ifd  19354  chfacffsupp  19357  chfacfscmul0  19359  chfacfpmmul0  19363  elcls  19574  maxlp  19648  perfi  19656  ordtbaslem  19689  ordtval  19690  ordtbas2  19692  ordtopn1  19695  ordtopn2  19696  ordtcnv  19702  ordtrest  19703  ordtrest2lem  19704  ordtrest2  19705  pnfnei  19721  mnfnei  19722  isreg2  19878  ordthauslem  19884  cmpfi  19908  cmpfii  19909  bwth  19910  bwthOLD  19911  nconsubb  19924  hausdiag  20146  txkgen  20153  kqdisj  20233  ordthmeolem  20302  fbfinnfr  20342  trfbas  20345  fbunfip  20370  fbasrn  20385  trfil3  20389  ufileu  20420  fin1aufil  20433  hausflim  20482  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem2  20553  ptcmplem3  20554  stdbdbl  21020  iccntr  21326  reconnlem2  21332  iccpnfcnv  21444  xrhmeo  21446  lebnumlem1  21461  lebnumlem2  21462  lebnumlem3  21463  bcthlem4  21766  minveclem3b  21843  ivthlem2  21864  ivthlem3  21865  mbfmax  22056  mbfposr  22059  i1fd  22088  mbfi1fseqlem4  22125  itg2splitlem  22155  itg2monolem1  22157  itg2cnlem1  22168  dvne0  22412  lhop1lem  22414  deg1nn0clb  22490  dgrle  22640  coemulhi  22651  aaliou3lem9  22746  cos11  22920  logleb  22988  argrege0  22996  logdivle  23007  ellogdm  23020  cxple  23076  cxplt2  23079  cxple3  23082  isosctrlem1  23152  atandm  23207  atans2  23262  atantayl2  23269  ftalem7  23352  isppw2  23389  musum  23467  dchrsum2  23543  bposlem1  23559  lgsmod  23596  lgsdir2lem2  23599  lgsdir2  23603  lgsne0  23608  lgsquadlem1  23629  rpvmasumlem  23672  padicabv  23815  ostth3  23823  ostth  23824  istrkg2d  23856  istrkgld  23857  tglowdim2l  24031  axlowdimlem16  24260  axlowdim2  24263  axlowdim  24264  usgra1v  24390  usgraidx2v  24393  nbgra0nb  24429  cusgrafilem3  24481  spthispth  24575  wlkdvspthlem  24609  clwlkisclwwlklem2a4  24784  clwlknclwlkdifs  24960  eupath2lem3  24979  eupath2  24980  konigsberg  24987  frgra2v  24999  frgrancvvdeqlem2  25031  2spotiundisj  25062  usg2spot2nb  25065  2spotmdisj  25068  frgrareggt1  25116  friendshipgt3  25121  lpni  25181  nmobndseqi  25694  minvecolem5  25797  chpsscon3  26421  chnle  26432  nonbooli  26569  pjnel  26644  specval  26817  nmcfnlbi  26971  stri  27176  hstri  27184  cvbr  27201  cvcon3  27203  chcv1  27274  cvexchlem  27287  chrelat2  27289  spc2d  27373  elpreq  27417  ifeqeqx  27419  ifbieq12d2  27420  isoun  27520  suppss3  27550  xrge0infss  27580  xrge0infssd  27581  eliccelico  27588  elicoelioo  27589  nndiffz1  27596  nn0min  27611  toslublem  27655  tosglblem  27657  isarchi2  27729  archiabl  27742  ordtcnvNEW  27902  ordtrestNEW  27903  ordtrest2NEWlem  27904  ordtrest2NEW  27905  ordtconlem1  27906  xrge0iifcnv  27915  elzdif0  27961  esumpcvgval  28084  ddemeas  28208  oms0  28266  oddpwdc  28293  eulerpartlems  28299  eulerpartlemf  28309  eulerpartlemt  28310  eulerpartlemr  28313  eulerpartlemgvv  28315  eulerpartlemn  28320  ballotlemfc0  28431  ballotlemfcc  28432  ballotlem4  28437  ballotlemimin  28444  ballotlem7  28474  plymulx  28505  signsply0  28508  eldmgm  28564  erdszelem10  28644  ismfs  28909  mvtinf  28915  untelirr  29080  untsucf  29082  untangtr  29086  inffz  29108  dfpo2  29184  dfon2lem3  29217  dfon2lem4  29218  dfon2lem7  29221  dfon2lem9  29223  distel  29236  predpoirr  29277  predfrirr  29278  soseq  29334  wfrlem10  29352  nodenselem4  29444  nodenselem5  29445  nocvxminlem  29450  nofulllem4  29465  funpartfv  29595  dfrdg4  29600  limsucncmpi  29910  limsucncmp  29911  ordcmp  29912  wl-ax11-lem8  30032  leceifl  30044  mblfinlem2  30052  mblfinlem3  30053  ismblfin  30055  cnambfre  30063  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  iblabsnclem  30078  ftc1anclem1  30090  areacirc  30112  nn0prpwlem  30140  nn0prpw  30141  heibor1lem  30305  heiborlem1  30307  heiborlem6  30312  heiborlem8  30314  heiborlem10  30316  smprngopr  30449  ellz1  30700  rencldnfilem  30754  jm2.22  30937  jm2.23  30938  wepwsolem  30987  fnwe2lem2  30997  aomclem8  31007  unxpwdom3  31041  radcnvrat  31195  lcmneg  31209  rusbcALT  31346  icccncfext  31690  stoweidlem14  31796  stoweidlem34  31816  stoweidlem59  31841  etransclem24  32041  eu2ndop1stv  32207  afvfv0bi  32237  afvco2  32261  ndmaovg  32269  otiunsndisjX  32301  rexxfrd2  32304  2f1fvneq  32307  ltnltne  32321  usgedgvadf1  32415  usgedgvadf1ALT  32418  lidldomnnring  32736  zrninitoringc  32879  ztprmneprm  32936  lindepsnlininds  33053  islindeps  33054  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  en3lpVD  33645  bnj23  33771  bnj1185  33852  bnj1476  33905  bnj1228  34067  bnj1388  34089  bnj1417  34097  bj-con3thALT  34162  bj-hbntbi  34258  bj-cbvexv  34297  bj-cbvexdv  34301  bj-cbvex2v  34303  bj-drex1v  34327  bj-nalset  34380  bj-dtru  34383  bj-ru0  34500  bj-nuliota  34586  riotaclbgBAD  34685  lcvfbr  34745  lcvbr  34746  lsatcv0  34756  l1cvpat  34779  opltcon3b  34929  cvrfval  34993  cvrval  34994  cvrnbtwn  34996  cvrval2  34999  cvrnbtwn2  35000  cvrnbtwn3  35001  cvrcon3b  35002  cvrnbtwn4  35004  atnlt  35038  iscvlat  35048  cvlexch1  35053  hlsuprexch  35105  hlrelat5N  35125  hlrelat2  35127  cvrval5  35139  3dimlem1  35182  3dim1lem5  35190  3dim2  35192  3dim3  35193  llnnlt  35247  islpln5  35259  lplni2  35261  lvolex3N  35262  lplnnle2at  35265  islpln2a  35272  lplnribN  35275  lplnexllnN  35288  lplnnlt  35289  lvoli3  35301  islvol5  35303  lvoli2  35305  lvolnle3at  35306  islvol2aN  35316  4atlem11  35333  lvolnltN  35342  dalawlem15  35609  4atexlemex2  35795  4atex  35800  4atex2-0aOLDN  35802  4atex2-0cOLDN  35804  lautcvr  35816  ltrnfset  35841  ltrnset  35842  ltrnu  35845  trlfset  35885  trlset  35886  trlval2  35888  cdlemd6  35928  cdleme0nex  36015  cdleme18d  36020  cdleme25b  36080  cdleme25cv  36084  cdleme29b  36101  cdleme31fv  36116  cdleme31fv2  36119  cdlemefrs29bpre0  36122  cdlemefr32sn2aw  36130  cdlemefr29bpre0N  36132  cdlemefr29clN  36133  cdlemefr32fvaN  36135  cdlemefr32fva1  36136  cdlemefs32sn1aw  36140  cdleme32fva  36163  cdleme32fvaw  36165  cdleme40v  36195  cdleme42b  36204  cdleme46f2g2  36219  cdleme46f2g1  36220  cdleme48gfv  36263  cdlemg1fvawlemN  36299  cdlemg1cex  36314  cdlemg6d  36347  cdlemm10N  36845  dicffval  36901  dicfval  36902  dicval  36903  dicfnN  36910  dicvalrelN  36912  dihffval  36957  dihfval  36958  dihlsscpre  36961  dvh4dimat  37165  dvh3dimatN  37166  dvh4dimlem  37170  dvh3dim  37173  dvh4dimN  37174  dvh3dim2  37175  dvh3dim3N  37176  mapdcv  37387  mapdh9aOLDN  37518  hdmapfval  37557  hdmapval  37558  hdmapval2  37562  hdmap11lem2  37572  bj-ifbi12  37702  bj-ifbi123  37705
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 185
  Copyright terms: Public domain W3C validator