MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notbid Structured version   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  1304  xorbi12d  1324  cbvexvw  1717  hba1w  1722  hbe1w  1723  cbvex  1983  cbvexd  1988  equsexOLD  2003  ax10lem2OLD  2026  ax9OLD  2033  drex1  2059  ax11inda  2277  eujustALT  2284  2mo  2359  neeq1  2609  neeq2  2610  necon3abid  2634  neleq1  2699  neleq2  2700  cbvrexf  2927  gencbval  3000  spcegf  3032  spc2gv  3039  spc3gv  3041  cdeqnot  3149  ru  3160  sbcng  3201  sbcrext  3234  sbcnel12g  3268  cbvrexcsf  3312  difjust  3322  eldif  3330  dfpss3  3433  difeq2  3459  disjne  3673  pssdifcom1  3713  pssdifcom2  3714  prel12  3975  disjxun  4210  nalset  4340  pwnss  4365  dtru  4390  dtruALT  4396  dtruALT2  4408  poeq1  4506  pocl  4510  swopo  4513  sotric  4529  sotrieq  4530  isso2i  4535  somo  4537  freq1  4552  frirr  4559  fr2nr  4560  frminex  4562  tz7.2  4566  wereu2  4579  nordeq  4600  ordtri1  4614  ordtri3  4617  rexxfrd  4738  rexxfr2d  4740  rexxfr  4743  elpwunsn  4757  fr3nr  4760  dfwe2  4762  ordsucsssuc  4803  nlimsucg  4822  orduninsuc  4823  dfom2  4847  ssnlim  4863  poinxp  4941  frinxp  4943  posn  4946  frsn  4948  rexiunxp  5015  rexxpf  5020  intirr  5252  poirr2  5258  cnvpo  5410  fvmpti  5805  fndmdif  5834  rexrnmpt  5879  f1imapss  6012  cbvexfo  6023  soisoi  6048  isopolem  6065  f1oweALT  6074  weniso  6075  rexrnmpt2  6185  ndmovg  6230  frxp  6456  poxp  6458  sorpssuni  6531  sorpssint  6532  canth  6539  riotaclbg  6589  smoword  6628  tz7.48lem  6698  abianfp  6716  oacan  6791  oaword  6792  omlimcl  6821  omeulem1  6825  nnaword  6870  nnmword  6876  nneob  6895  brdifun  6932  swoer  6933  undifixp  7098  boxcutc  7105  2dom  7179  php  7291  nndomo  7300  nnsdomo  7301  unxpdomlem2  7314  frfi  7352  unfilem1  7371  supeq3  7454  supeq123d  7455  supmo  7457  eqsup  7461  supub  7464  supmaxlem  7469  suppr  7473  supisolem  7475  supisoex  7476  oieq1  7481  ordtypecbv  7486  ordtypelem7  7493  wemapso2lem  7519  canthwdom  7547  zfregcl  7562  elirrv  7565  elirr  7566  noinfep  7614  noinfepOLD  7615  cantnfp1lem3  7636  rankr1clem  7746  carden2b  7854  domtri2  7876  alephord3  7959  alephdom2  7968  alephval3  7991  dfac9  8016  kmlem2  8031  kmlem4  8033  isfin4  8177  isfin7  8181  fin23lem11  8197  isf32lem5  8237  isf34lem4  8257  fin1a2lem6  8285  fin1a2lem7  8286  fin1a2lem12  8291  itunisuc  8299  ac6n  8365  zorn2g  8383  zornn0g  8385  ttukeylem7  8395  axpowndlem2  8473  axpowndlem3  8474  axpowndlem4  8475  axregnd  8479  elgch  8497  engch  8503  fpwwe2lem13  8517  fpwwe2  8518  pwfseqlem1  8533  pwfseqlem3  8535  hargch  8552  addnidpi  8778  pinq  8804  nqereu  8806  ltsonq  8846  prlem934  8910  ltexprlem7  8919  addcanpr  8923  prlem936  8924  reclem2pr  8925  reclem3pr  8926  supexpr  8931  ltsosr  8969  supsrlem  8986  axpre-lttri  9040  axpre-sup  9044  xrlenlt  9143  axlttri  9147  axsup  9151  ltne  9170  readdcan  9240  leadd1  9496  ltsub1  9524  ltsub2  9525  leord1  9554  lediv1  9875  lemuldiv  9889  lerec  9892  le2msq  9910  lbinfm  9961  infm3  9967  suprnub  9971  infmrgelb  9988  infmrlb  9989  avgle1  10207  avgle2  10208  znnnlt1  10308  indstr  10545  zsupss  10565  uzsupss  10568  rpneg  10641  xralrple  10791  xleneg  10804  xltadd1  10835  xposdif  10841  xmulneg1  10848  xltmul1  10871  xrsupexmnf  10883  xrinfmexpnf  10884  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  supxrleub  10905  infmxrgelb  10913  difreicc  11028  elfznelfzo  11192  injresinjlem  11199  leexp2  11434  hashbnd  11624  hasheni  11632  hashbc  11702  cnpart  12045  sqrlt  12067  limsuplt  12273  rlimrege0  12373  isercoll  12461  efle  12719  odd2np1  12908  divalglem7  12919  ndvdsadd  12928  bitsfval  12935  bitsval  12936  bits0  12940  bitsp1  12943  bitsmod  12948  bitscmp  12950  bitsinv1lem  12953  sadadd2lem2  12962  saddisjlem  12976  bitsshft  12987  gcdneg  13026  algcvgblem  13068  isprm3  13088  isprm5  13112  rpexp  13120  phiprmpw  13165  pythagtrip  13208  pcgcd1  13250  prmpwdvds  13272  prmreclem2  13285  prmreclem3  13286  prmreclem5  13288  prmreclem6  13289  vdwlem6  13354  vdwnnlem2  13364  vdwnnlem3  13365  vdwnn  13366  prmlem0  13428  prmlem1a  13429  divsfval  13772  mrisval  13855  ismri  13856  ismri2dad  13862  cidpropd  13936  plttr  14427  acsfiindd  14603  sylow1lem3  15234  sylow2alem2  15252  efgsfo  15371  ablfac1eulem  15630  ablfac1eu  15631  pgpfac1lem1  15632  pgpfac1lem5  15637  islbs  16148  lbsind  16152  lbspss  16154  lbspropd  16171  lspsnne1  16189  islbs2  16226  lbsacsbs  16228  lbsextlem1  16230  lbsextlem3  16232  lbsextlem4  16233  lbsextg  16234  nzrunit  16337  opsrtoslem2  16545  elcls  17137  maxlp  17211  perfi  17219  ordtbaslem  17252  ordtval  17253  ordtbas2  17255  ordtopn1  17258  ordtopn2  17259  ordtcnv  17265  ordtrest  17266  ordtrest2lem  17267  ordtrest2  17268  pnfnei  17284  mnfnei  17285  isreg2  17441  ordthauslem  17447  cmpfi  17471  cmpfii  17472  bwth  17473  nconsubb  17486  hausdiag  17677  txkgen  17684  kqdisj  17764  ordthmeolem  17833  fbfinnfr  17873  trfbas  17876  fbunfip  17901  fbasrn  17916  trfil3  17920  ufileu  17951  fin1aufil  17964  hausflim  18013  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALTlem4  18081  ptcmplem2  18084  ptcmplem3  18085  stdbdbl  18547  iccntr  18852  reconnlem2  18858  iccpnfcnv  18969  xrhmeo  18971  lebnumlem1  18986  lebnumlem2  18987  lebnumlem3  18988  bcthlem4  19280  minveclem3b  19329  ivthlem2  19349  ivthlem3  19350  mbfmax  19541  mbfposr  19544  i1fd  19573  mbfi1fseqlem4  19610  itg2splitlem  19640  itg2monolem1  19642  itg2cnlem1  19653  dvne0  19895  lhop1lem  19897  deg1nn0clb  20013  dgrle  20162  coemulhi  20172  aaliou3lem9  20267  cos11  20435  logleb  20498  argrege0  20506  logdivle  20517  ellogdm  20530  cxple  20586  cxplt2  20589  cxple3  20592  isosctrlem1  20662  atandm  20716  atans2  20771  atantayl2  20778  ftalem7  20861  isppw2  20898  musum  20976  dchrsum2  21052  bposlem1  21068  lgsmod  21105  lgsdir2lem2  21108  lgsdir2  21112  lgsne0  21117  lgsquadlem1  21138  rpvmasumlem  21181  padicabv  21324  ostth3  21332  ostth  21333  usgra1v  21409  usgraidx2v  21412  nbgra0nb  21441  cusgrafilem3  21490  spthispth  21573  wlkdvspthlem  21607  eupath2lem3  21701  eupath2  21702  konigsberg  21709  lpni  21767  nmobndseqi  22280  minvecolem5  22383  chpsscon3  23005  chnle  23016  nonbooli  23153  pjnel  23228  specval  23401  nmcfnlbi  23555  stri  23760  hstri  23768  cvbr  23785  cvcon3  23787  chcv1  23858  cvexchlem  23871  chrelat2  23873  elpreq  23999  ifeqeqx  24001  ifbieq12d2  24002  isoun  24089  eliccelico  24140  elicoelioo  24141  toslub  24191  tosglb  24192  isarchi2  24255  xrge0iifcnv  24319  elzdif0  24364  eldifpr  24392  eldiftp  24393  esumpcvgval  24468  ballotlemfc0  24750  ballotlemfcc  24751  ballotlem4  24756  ballotlemimin  24763  ballotlem7  24793  eldmgm  24806  erdszelem10  24886  untelirr  25157  untsucf  25159  untangtr  25163  dedekind  25187  inffz  25200  dfpo2  25378  dfon2lem3  25412  dfon2lem4  25413  dfon2lem7  25416  dfon2lem9  25418  distel  25431  predpoirr  25472  predfrirr  25473  soseq  25529  wfrlem10  25547  nodenselem4  25639  nodenselem5  25640  nocvxminlem  25645  nofulllem4  25660  funpartfv  25790  dfrdg4  25795  axlowdimlem16  25896  axlowdim2  25899  axlowdim  25900  limsucncmpi  26195  limsucncmp  26196  ordcmp  26197  leceifl  26240  mblfinlem2  26244  mblfinlem3  26245  ismblfin  26247  cnambfre  26255  itg2addnclem  26256  itg2addnclem2  26257  iblabsnclem  26268  ftc1anclem1  26280  areacirc  26297  nn0prpwlem  26325  nn0prpw  26326  heibor1lem  26518  heiborlem1  26520  heiborlem6  26525  heiborlem8  26527  heiborlem10  26529  smprngopr  26662  ellz1  26825  rencldnfilem  26881  jm2.22  27066  jm2.23  27067  wepwsolem  27116  fnwe2lem2  27126  aomclem8  27136  frlmlbs  27226  unxpwdom3  27233  islindf  27259  islinds2  27260  islindf2  27261  lindfind  27263  lindsind  27264  lindfrn  27268  lindfmm  27274  lsslindf  27277  islindf4  27285  psgnunilem1  27393  psgnunilem5  27394  psgnunilem2  27395  psgnunilem3  27396  rusbcALT  27616  xrltneNEW  27633  stoweidlem14  27739  stoweidlem34  27759  stoweidlem59  27784  eu2ndop1stv  27956  afvfv0bi  27992  afvco2  28016  ndmaovg  28024  otiunsndisj  28066  otiunsndisjX  28067  rexxfrd2  28073  2f1fvneq  28077  ltnltne  28094  wrdsymb0  28170  swrdnd  28182  swrdvalodm2  28188  swrdvalodm  28189  2cshwmod  28257  lswrd0  28261  2cshwcom  28267  frgra2v  28389  frgrancvvdeqlem2  28420  2spotiundisj  28451  usg2spot2nb  28454  2spotmdisj  28457  en3lpVD  28957  bnj23  29083  bnj1185  29165  bnj1476  29218  bnj1228  29380  bnj1388  29402  bnj1417  29410  ax9NEW7  29468  equsexNEW7  29490  drex1NEW7  29494  cbvexwAUX7  29520  cbvexOLD7  29726  cbvexdOLD7  29735  lcvfbr  29818  lcvbr  29819  lsatcv0  29829  l1cvpat  29852  opltcon3b  30002  cvrfval  30066  cvrval  30067  cvrnbtwn  30069  cvrval2  30072  cvrnbtwn2  30073  cvrnbtwn3  30074  cvrcon3b  30075  cvrnbtwn4  30077  atnlt  30111  iscvlat  30121  cvlexch1  30126  hlsuprexch  30178  hlrelat5N  30198  hlrelat2  30200  cvrval5  30212  3dimlem1  30255  3dim1lem5  30263  3dim2  30265  3dim3  30266  llnnlt  30320  islpln5  30332  lplni2  30334  lvolex3N  30335  lplnnle2at  30338  islpln2a  30345  lplnribN  30348  lplnexllnN  30361  lplnnlt  30362  lvoli3  30374  islvol5  30376  lvoli2  30378  lvolnle3at  30379  islvol2aN  30389  4atlem11  30406  lvolnltN  30415  dalawlem15  30682  4atexlemex2  30868  4atex  30873  4atex2-0aOLDN  30875  4atex2-0cOLDN  30877  lautcvr  30889  ltrnfset  30914  ltrnset  30915  ltrnu  30918  trlfset  30957  trlset  30958  trlval2  30960  cdlemd6  31000  cdleme0nex  31087  cdleme18d  31092  cdleme25b  31151  cdleme25cv  31155  cdleme29b  31172  cdleme31fv  31187  cdleme31fv2  31190  cdlemefrs29bpre0  31193  cdlemefr32sn2aw  31201  cdlemefr29bpre0N  31203  cdlemefr29clN  31204  cdlemefr32fvaN  31206  cdlemefr32fva1  31207  cdlemefs32sn1aw  31211  cdleme32fva  31234  cdleme32fvaw  31236  cdleme40v  31266  cdleme42b  31275  cdleme46f2g2  31290  cdleme46f2g1  31291  cdleme48gfv  31334  cdlemg1fvawlemN  31370  cdlemg1cex  31385  cdlemg6d  31418  cdlemm10N  31916  dicffval  31972  dicfval  31973  dicval  31974  dicfnN  31981  dicvalrelN  31983  dihffval  32028  dihfval  32029  dihlsscpre  32032  dvh4dimat  32236  dvh3dimatN  32237  dvh4dimlem  32241  dvh3dim  32244  dvh4dimN  32245  dvh3dim2  32246  dvh3dim3N  32247  mapdcv  32458  mapdh9aOLDN  32589  hdmapfval  32628  hdmapval  32629  hdmapval2  32633  hdmap11lem2  32643
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