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

Theorem notbid 285
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 282 . . 3  |-  ( ps  <->  -. 
-.  ps )
3 notnot 282 . . 3  |-  ( ch  <->  -. 
-.  ch )
41, 2, 33bitr3g 278 . 2  |-  ( ph  ->  ( -.  -.  ps  <->  -. 
-.  ch ) )
54con4bid 284 1  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  notbi  286  con3th  924  xorbi12d  1306  cbvexvw  1677  hba1w  1681  hbe1w  1682  ax10lem2  1877  ax9  1889  equsex  1902  drex1  1907  cbvex  1925  cbvexd  1949  ax11inda  2139  eujustALT  2146  2mo  2221  neeq1  2454  neeq2  2455  necon3abid  2479  neleq1  2537  neleq2  2538  cbvrexf  2759  gencbval  2832  spcegf  2864  spc2gv  2871  spc3gv  2873  cdeqnot  2979  ru  2990  sbcng  3031  sbcrext  3064  sbcnel12g  3098  cbvrexcsf  3144  difjust  3154  eldif  3162  dfpss3  3262  difeq2  3288  disjne  3500  pssdifcom1  3539  pssdifcom2  3540  prel12  3789  disjxun  4021  nalset  4151  pwnss  4176  dtru  4201  dtruALT  4207  dtruALT2  4219  poeq1  4317  pocl  4321  swopo  4324  sotric  4340  sotrieq  4341  isso2i  4346  somo  4348  freq1  4363  frirr  4370  fr2nr  4371  frminex  4373  tz7.2  4377  wereu2  4390  nordeq  4411  ordtri1  4425  ordtri3  4428  rexxfrd  4549  rexxfr2d  4551  rexxfr  4554  elpwunsn  4568  fr3nr  4571  dfwe2  4573  ordsucsssuc  4614  nlimsucg  4633  orduninsuc  4634  dfom2  4658  ssnlim  4674  poinxp  4753  frinxp  4755  posn  4758  frsn  4760  rexiunxp  4826  rexxpf  4831  intirr  5061  poirr2  5067  cnvpo  5213  fvmpti  5601  fndmdif  5629  rexrnmpt  5670  f1imapss  5790  cbvexfo  5800  soisoi  5825  isopolem  5842  f1oweALT  5851  weniso  5852  rexrnmpt2  5959  ndmovg  6003  frxp  6225  poxp  6227  sorpssuni  6286  sorpssint  6287  canth  6294  riotaclbg  6344  smoword  6383  tz7.48lem  6453  abianfp  6471  oacan  6546  oaword  6547  omlimcl  6576  omeulem1  6580  nnaword  6625  nnmword  6631  nneob  6650  brdifun  6687  swoer  6688  undifixp  6852  boxcutc  6859  2dom  6933  php  7045  nndomo  7054  nnsdomo  7055  unxpdomlem2  7068  frfi  7102  unfilem1  7121  supmo  7203  eqsup  7207  supub  7210  supmaxlem  7215  suppr  7219  supisolem  7221  supisoex  7222  oieq1  7227  ordtypecbv  7232  ordtypelem7  7239  wemapso2lem  7265  canthwdom  7293  zfregcl  7308  elirrv  7311  elirr  7312  noinfep  7360  noinfepOLD  7361  cantnfp1lem3  7382  rankr1clem  7492  carden2b  7600  domtri2  7622  alephord3  7705  alephdom2  7714  alephval3  7737  dfac9  7762  kmlem2  7777  kmlem4  7779  isfin4  7923  isfin7  7927  fin23lem11  7943  isf32lem5  7983  isf34lem4  8003  fin1a2lem6  8031  fin1a2lem7  8032  fin1a2lem12  8037  itunisuc  8045  ac6n  8112  zorn2g  8130  zornn0g  8132  ttukeylem7  8142  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axregnd  8226  elgch  8244  engch  8250  fpwwe2lem13  8264  fpwwe2  8265  pwfseqlem1  8280  pwfseqlem3  8282  hargch  8299  addnidpi  8525  pinq  8551  nqereu  8553  ltsonq  8593  prlem934  8657  ltexprlem7  8666  addcanpr  8670  prlem936  8671  reclem2pr  8672  reclem3pr  8673  supexpr  8678  ltsosr  8716  supsrlem  8733  axpre-lttri  8787  axpre-sup  8791  xrlenlt  8890  axlttri  8894  axsup  8898  ltne  8917  readdcan  8986  leadd1  9242  ltsub1  9270  ltsub2  9271  leord1  9300  lediv1  9621  lemuldiv  9635  lerec  9638  le2msq  9656  lbinfm  9707  infm3  9713  suprnub  9717  infmrgelb  9734  infmrlb  9735  avgle1  9951  avgle2  9952  znnnlt1  10050  indstr  10287  zsupss  10307  uzsupss  10310  rpneg  10383  xralrple  10532  xleneg  10545  xltadd1  10576  xposdif  10582  xmulneg1  10589  xltmul1  10612  xrsupexmnf  10623  xrinfmexpnf  10624  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrleub  10645  infmxrgelb  10653  difreicc  10767  leexp2  11156  hashbnd  11343  hasheni  11347  hashbc  11391  cnpart  11725  sqrlt  11747  limsuplt  11953  rlimrege0  12053  isercoll  12141  efle  12398  odd2np1  12587  divalglem7  12598  ndvdsadd  12607  bitsfval  12614  bitsval  12615  bits0  12619  bitsp1  12622  bitsmod  12627  bitscmp  12629  bitsinv1lem  12632  sadadd2lem2  12641  saddisjlem  12655  bitsshft  12666  gcdneg  12705  algcvgblem  12747  isprm3  12767  isprm5  12791  rpexp  12799  phiprmpw  12844  pythagtrip  12887  pcgcd1  12929  prmpwdvds  12951  prmreclem2  12964  prmreclem3  12965  prmreclem5  12967  prmreclem6  12968  vdwlem6  13033  vdwnnlem2  13043  vdwnnlem3  13044  vdwnn  13045  prmlem0  13107  prmlem1a  13108  divsfval  13449  mrisval  13532  ismri  13533  ismri2dad  13539  cidpropd  13613  plttr  14104  acsfiindd  14280  sylow1lem3  14911  sylow2alem2  14929  efgsfo  15048  ablfac1eulem  15307  ablfac1eu  15308  pgpfac1lem1  15309  pgpfac1lem5  15314  islbs  15829  lbsind  15833  lbspss  15835  lbspropd  15852  lspsnne1  15870  islbs2  15907  lbsacsbs  15909  lbsextlem1  15911  lbsextlem3  15913  lbsextlem4  15914  lbsextg  15915  nzrunit  16018  opsrtoslem2  16226  elcls  16810  maxlp  16878  perfi  16886  ordtbaslem  16918  ordtval  16919  ordtbas2  16921  ordtopn1  16924  ordtopn2  16925  ordtcnv  16931  ordtrest  16932  ordtrest2lem  16933  ordtrest2  16934  pnfnei  16950  mnfnei  16951  isreg2  17105  ordthauslem  17111  cmpfi  17135  cmpfii  17136  nconsubb  17149  hausdiag  17339  txkgen  17346  kqdisj  17423  ordthmeolem  17492  fbfinnfr  17536  trfbas  17539  fbunfip  17564  fbasrn  17579  trfil3  17583  ufileu  17614  fin1aufil  17627  hausflim  17676  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem2  17747  ptcmplem3  17748  stdbdbl  18063  iccntr  18326  reconnlem2  18332  iccpnfcnv  18442  xrhmeo  18444  lebnumlem1  18459  lebnumlem2  18460  lebnumlem3  18461  bcthlem4  18749  minveclem3b  18792  ivthlem2  18812  ivthlem3  18813  mbfmax  19004  mbfposr  19007  i1fd  19036  mbfi1fseqlem4  19073  itg2splitlem  19103  itg2monolem1  19105  itg2cnlem1  19116  dvne0  19358  lhop1lem  19360  deg1nn0clb  19476  dgrle  19625  coemulhi  19635  aaliou3lem9  19730  cos11  19895  logleb  19957  argrege0  19965  logdivle  19973  ellogdm  19986  cxple  20042  cxplt2  20045  cxple3  20048  isosctrlem1  20118  atandm  20172  atans2  20227  atantayl2  20234  ftalem7  20316  isppw2  20353  musum  20431  dchrsum2  20507  bposlem1  20523  lgsmod  20560  lgsdir2lem2  20563  lgsdir2  20567  lgsne0  20572  lgsquadlem1  20593  rpvmasumlem  20636  padicabv  20779  ostth3  20787  ostth  20788  lpni  20846  nmobndseqi  21357  minvecolem5  21460  chpsscon3  22082  chnle  22093  nonbooli  22230  pjnel  22305  specval  22478  nmcfnlbi  22632  stri  22837  hstri  22845  cvbr  22862  cvcon3  22864  chcv1  22935  cvexchlem  22948  chrelat2  22950  ifeqeqx  23034  ballotlemfc0  23051  ballotlemfcc  23052  ballotlem4  23057  ballotlemi1  23061  ballotlemii  23062  ballotlemimin  23064  ballotlem7  23094  ifbieq12d2  23149  elpreq  23188  isoun  23242  eliccelico  23270  elicoelioo  23271  xrge0iifcnv  23315  eldifpr  23394  eldiftp  23395  esumpcvgval  23446  eldmgm  23694  erdszelem10  23731  eupath2lem3  23903  eupath2  23904  konigsberg  23911  untelirr  24054  untsucf  24056  untangtr  24060  dedekind  24082  inffz  24095  dfpo2  24112  dfon2lem3  24141  dfon2lem4  24142  dfon2lem7  24145  dfon2lem9  24147  distel  24160  predpoirr  24197  predfrirr  24198  soseq  24254  nodenselem4  24338  nodenselem5  24339  nocvxminlem  24344  nofulllem4  24359  funpartfv  24483  dfrdg4  24488  axlowdimlem16  24585  axlowdim2  24588  axlowdim  24589  nabi1  24828  nabi2  24829  limsucncmpi  24884  limsucncmp  24885  ordcmp  24886  areacirc  24931  vxveqv  25054  inttpemp  25139  dstr  25171  nelioo5  25511  bwt2  25592  iintlem1  25610  tethpnc2  26071  pdiveql  26168  nn0prpwlem  26238  nn0prpw  26239  heibor1lem  26533  heiborlem1  26535  heiborlem6  26540  heiborlem8  26542  heiborlem10  26544  smprngopr  26677  ellz1  26846  rencldnfilem  26903  jm2.22  27088  jm2.23  27089  wepwsolem  27138  fnwe2lem2  27148  supeq123d  27158  aomclem8  27159  frlmlbs  27249  unxpwdom3  27256  islindf  27282  islinds2  27283  islindf2  27284  lindfind  27286  lindsind  27287  lindfrn  27291  lindfmm  27297  lsslindf  27300  islindf4  27308  psgnunilem1  27416  psgnunilem5  27417  psgnunilem2  27418  psgnunilem3  27419  rusbcALT  27639  xrltneNEW  27657  stoweidlem14  27763  stoweidlem34  27783  stoweidlem59  27808  afvfv0bi  28015  afvco2  28037  ndmaovg  28044  usgra1v  28126  nbusgra  28143  nbgra0nb  28144  frgra2v  28177  en3lpVD  28621  bnj23  28744  bnj1185  28826  bnj1476  28879  bnj1228  29041  bnj1388  29063  bnj1417  29071  ax12-4  29106  equsexv-x12  29113  a12study10  29136  a12study10n  29137  lcvfbr  29210  lcvbr  29211  lsatcv0  29221  l1cvpat  29244  opltcon3b  29394  cvrfval  29458  cvrval  29459  cvrnbtwn  29461  cvrval2  29464  cvrnbtwn2  29465  cvrnbtwn3  29466  cvrcon3b  29467  cvrnbtwn4  29469  atnlt  29503  iscvlat  29513  cvlexch1  29518  hlsuprexch  29570  hlrelat5N  29590  hlrelat2  29592  cvrval5  29604  3dimlem1  29647  3dim1lem5  29655  3dim2  29657  3dim3  29658  llnnlt  29712  islpln5  29724  lplni2  29726  lvolex3N  29727  lplnnle2at  29730  islpln2a  29737  lplnribN  29740  lplnexllnN  29753  lplnnlt  29754  lvoli3  29766  islvol5  29768  lvoli2  29770  lvolnle3at  29771  islvol2aN  29781  4atlem11  29798  lvolnltN  29807  dalawlem15  30074  4atexlemex2  30260  4atex  30265  4atex2-0aOLDN  30267  4atex2-0cOLDN  30269  lautcvr  30281  ltrnfset  30306  ltrnset  30307  ltrnu  30310  trlfset  30349  trlset  30350  trlval2  30352  cdlemd6  30392  cdleme0nex  30479  cdleme18d  30484  cdleme25b  30543  cdleme25cv  30547  cdleme29b  30564  cdleme31fv  30579  cdleme31fv2  30582  cdlemefrs29bpre0  30585  cdlemefr32sn2aw  30593  cdlemefr29bpre0N  30595  cdlemefr29clN  30596  cdlemefr32fvaN  30598  cdlemefr32fva1  30599  cdlemefs32sn1aw  30603  cdleme32fva  30626  cdleme32fvaw  30628  cdleme40v  30658  cdleme42b  30667  cdleme46f2g2  30682  cdleme46f2g1  30683  cdleme48gfv  30726  cdlemg1fvawlemN  30762  cdlemg1cex  30777  cdlemg6d  30810  cdlemm10N  31308  dicffval  31364  dicfval  31365  dicval  31366  dicfnN  31373  dicvalrelN  31375  dihffval  31420  dihfval  31421  dihlsscpre  31424  dvh4dimat  31628  dvh3dimatN  31629  dvh4dimlem  31633  dvh3dim  31636  dvh4dimN  31637  dvh3dim2  31638  dvh3dim3N  31639  mapdcv  31850  mapdh9aOLDN  31981  hdmapfval  32020  hdmapval  32021  hdmapval2  32025  hdmap11lem2  32035
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 177
  Copyright terms: Public domain W3C validator