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

Theorem notbid 287
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 284 . . 3  |-  ( ps  <->  -. 
-.  ps )
3 notnot 284 . . 3  |-  ( ch  <->  -. 
-.  ch )
41, 2, 33bitr3g 280 . 2  |-  ( ph  ->  ( -.  -.  ps  <->  -. 
-.  ch ) )
54con4bid 286 1  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178
This theorem is referenced by:  notbi  288  con3th  929  xorbi12d  1311  ax10lem21  1670  ax9  1683  equsex  1853  drex1  1860  cbvex  1878  cbvexd  2053  ax11inda  2116  eujustALT  2120  2mo  2194  neeq1  2427  neeq2  2428  necon3abid  2452  neleq1  2510  neleq2  2511  cbvrexf  2729  gencbval  2800  cla4egf  2832  cla42gv  2839  cla43gv  2841  cdeqnot  2940  ru  2951  sbcng  2992  sbcrext  3025  sbcnel12g  3059  cbvrexcsf  3105  difjust  3115  eldif  3123  dfpss3  3223  difeq2  3249  disjne  3461  pssdifcom1  3500  pssdifcom2  3501  prel12  3749  disjxun  3981  nalset  4111  dtru  4159  dtruALT  4165  dtruALT2  4177  poeq1  4275  pocl  4279  swopo  4282  sotric  4298  sotrieq  4299  isso2i  4304  somo  4306  freq1  4321  frirr  4328  fr2nr  4329  frminex  4331  tz7.2  4335  wereu2  4348  nordeq  4369  ordtri1  4383  ordtri3  4386  rexxfrd  4507  rexxfr2d  4509  rexxfr  4512  elpwunsn  4526  fr3nr  4529  dfwe2  4531  ordsucsssuc  4572  nlimsucg  4591  orduninsuc  4592  dfom2  4616  ssnlim  4632  poinxp  4727  frinxp  4729  posn  4732  frsn  4734  rexiunxp  4800  rexxpf  4805  intirr  5035  poirr2  5041  cnvpo  5186  fvmpti  5521  fndmdif  5549  rexrnmpt  5590  f1imapss  5710  cbvexfo  5720  soisoi  5745  isopolem  5762  f1oweALT  5771  weniso  5772  rexrnmpt2  5879  ndmovg  5923  frxp  6145  poxp  6147  sorpssuni  6206  sorpssint  6207  canth  6246  pwnss  6251  riotaclbg  6298  smoword  6337  tz7.48lem  6407  abianfp  6425  oacan  6500  oaword  6501  omlimcl  6530  omeulem1  6534  nnaword  6579  nnmword  6585  nneob  6604  brdifun  6641  swoer  6642  undifixp  6806  boxcutc  6813  2dom  6887  php  6999  nndomo  7008  nnsdomo  7009  unxpdomlem2  7022  frfi  7056  unfilem1  7075  supmo  7157  eqsup  7161  supub  7164  supmaxlem  7169  suppr  7173  supisolem  7175  supisoex  7176  oieq1  7181  ordtypecbv  7186  ordtypelem7  7193  wemapso2lem  7219  canthwdom  7247  zfregcl  7262  elirrv  7265  elirr  7266  noinfep  7314  noinfepOLD  7315  cantnfp1lem3  7336  rankr1clem  7446  carden2b  7554  domtri2  7576  alephord3  7659  alephdom2  7668  alephval3  7691  dfac9  7716  kmlem2  7731  kmlem4  7733  isfin4  7877  isfin7  7881  fin23lem11  7897  isf32lem5  7937  isf34lem4  7957  fin1a2lem6  7985  fin1a2lem7  7986  fin1a2lem12  7991  itunisuc  7999  ac6n  8066  zorn2g  8084  zornn0g  8086  ttukeylem7  8096  axpowndlem2  8174  axpowndlem3  8175  axpowndlem4  8176  axregnd  8180  elgch  8198  engch  8204  fpwwe2lem13  8218  fpwwe2  8219  pwfseqlem1  8234  pwfseqlem3  8236  hargch  8253  addnidpi  8479  pinq  8505  nqereu  8507  ltsonq  8547  prlem934  8611  ltexprlem7  8620  addcanpr  8624  prlem936  8625  reclem2pr  8626  reclem3pr  8627  supexpr  8632  ltsosr  8670  supsrlem  8687  axpre-lttri  8741  axpre-sup  8745  xrlenlt  8844  axlttri  8848  axsup  8852  ltne  8871  readdcan  8940  leadd1  9196  ltsub1  9224  ltsub2  9225  leord1  9254  lediv1  9575  lemuldiv  9589  lerec  9592  le2msq  9610  lbinfm  9661  infm3  9667  suprnub  9671  infmrgelb  9688  infmrlb  9689  avgle1  9904  avgle2  9905  znnnlt1  10003  indstr  10240  zsupss  10260  uzsupss  10263  rpneg  10336  xralrple  10484  xleneg  10497  xltadd1  10528  xposdif  10534  xmulneg1  10541  xltmul1  10564  xrsupexmnf  10575  xrinfmexpnf  10576  xrsupsslem  10577  xrinfmsslem  10578  xrub  10582  supxrleub  10597  infmxrgelb  10605  difreicc  10719  leexp2  11108  hashbnd  11295  hasheni  11299  hashbc  11342  cnpart  11676  sqrlt  11698  limsuplt  11904  rlimrege0  12004  isercoll  12092  efle  12346  odd2np1  12535  divalglem7  12546  ndvdsadd  12555  bitsfval  12562  bitsval  12563  bits0  12567  bitsp1  12570  bitsmod  12575  bitscmp  12577  bitsinv1lem  12580  sadadd2lem2  12589  saddisjlem  12603  bitsshft  12614  gcdneg  12653  algcvgblem  12695  isprm3  12715  isprm5  12739  rpexp  12747  phiprmpw  12792  pythagtrip  12835  pcgcd1  12877  prmpwdvds  12899  prmreclem2  12912  prmreclem3  12913  prmreclem5  12915  prmreclem6  12916  vdwlem6  12981  vdwnnlem2  12991  vdwnnlem3  12992  vdwnn  12993  prmlem0  13055  prmlem1a  13056  divsfval  13397  mrisval  13480  ismri  13481  ismri2dad  13487  cidpropd  13561  plttr  14052  acsfiindd  14228  sylow1lem3  14859  sylow2alem2  14877  efgsfo  14996  ablfac1eulem  15255  ablfac1eu  15256  pgpfac1lem1  15257  pgpfac1lem5  15262  islbs  15777  lbsind  15781  lbspss  15783  lbspropd  15800  lspsnne1  15818  islbs2  15855  lbsacsbs  15857  lbsextlem1  15859  lbsextlem3  15861  lbsextlem4  15862  lbsextg  15863  nzrunit  15966  opsrtoslem2  16174  elcls  16758  maxlp  16826  perfi  16834  ordtbaslem  16866  ordtval  16867  ordtbas2  16869  ordtopn1  16872  ordtopn2  16873  ordtcnv  16879  ordtrest  16880  ordtrest2lem  16881  ordtrest2  16882  pnfnei  16898  mnfnei  16899  isreg2  17053  ordthauslem  17059  cmpfi  17083  cmpfii  17084  nconsubb  17097  hausdiag  17287  txkgen  17294  kqdisj  17371  ordthmeolem  17440  fbfinnfr  17484  trfbas  17487  fbunfip  17512  fbasrn  17527  trfil3  17531  ufileu  17562  fin1aufil  17575  hausflim  17624  alexsubALTlem2  17690  alexsubALTlem3  17691  alexsubALTlem4  17692  ptcmplem2  17695  ptcmplem3  17696  stdbdbl  18011  iccntr  18274  reconnlem2  18280  iccpnfcnv  18390  xrhmeo  18392  lebnumlem1  18407  lebnumlem2  18408  lebnumlem3  18409  bcthlem4  18697  minveclem3b  18740  ivthlem2  18760  ivthlem3  18761  mbfmax  18952  mbfposr  18955  i1fd  18984  mbfi1fseqlem4  19021  itg2splitlem  19051  itg2monolem1  19053  itg2cnlem1  19064  dvne0  19306  lhop1lem  19308  deg1nn0clb  19424  dgrle  19573  coemulhi  19583  aaliou3lem9  19678  cos11  19843  logleb  19905  argrege0  19913  logdivle  19921  ellogdm  19934  cxple  19990  cxplt2  19993  cxple3  19996  isosctrlem1  20066  atandm  20120  atans2  20175  atantayl2  20182  ftalem7  20264  isppw2  20301  musum  20379  dchrsum2  20455  bposlem1  20471  lgsmod  20508  lgsdir2lem2  20511  lgsdir2  20515  lgsne0  20520  lgsquadlem1  20541  rpvmasumlem  20584  padicabv  20727  ostth3  20735  ostth  20736  lpni  20792  nmobndseqi  21303  minvecolem5  21406  chpsscon3  22028  chnle  22039  nonbooli  22194  pjnel  22269  specval  22424  nmcfnlbi  22578  stri  22783  hstri  22791  cvbr  22808  cvcon3  22810  chcv1  22881  cvexchlem  22894  chrelat2  22896  ifeqeqx  22980  ballotlemfc0  22998  ballotlemfcc  22999  ballotlem4  23004  ballotlemi1  23008  ballotlemii  23009  ballotlemimin  23011  ballotlem7  23041  eldmgm  23052  erdszelem10  23089  eupath2lem3  23261  eupath2  23262  konigsberg  23269  untelirr  23412  untsucf  23414  untangtr  23418  dedekind  23439  inffz  23452  dfpo2  23469  dfon2lem3  23496  dfon2lem4  23497  dfon2lem7  23500  dfon2lem9  23502  distel  23515  predpoirr  23552  predfrirr  23553  soseq  23609  axdenselem4  23693  axdenselem5  23694  nocvxminlem  23699  axfelem14  23714  elfuns  23815  funpartfv  23844  dfrdg4  23849  axlowdimlem16  23946  axlowdim2  23949  axlowdim  23950  nabi1  24189  nabi2  24190  limsucncmpi  24245  limsucncmp  24246  ordcmp  24247  vxveqv  24406  inttpemp  24492  dstr  24524  nelioo5  24864  bwt2  24945  iintlem1  24963  tethpnc2  25424  pdiveql  25521  nn0prpwlem  25591  nn0prpw  25592  heibor1lem  25886  heiborlem1  25888  heiborlem6  25893  heiborlem8  25895  heiborlem10  25897  smprngopr  26030  ellz1  26199  rencldnfilem  26256  jm2.22  26441  jm2.23  26442  wepwsolem  26491  fnwe2lem2  26501  supeq123d  26511  aomclem8  26512  frlmlbs  26602  unxpwdom3  26609  islindf  26635  islinds2  26636  islindf2  26637  lindfind  26639  lindsind  26640  lindfrn  26644  lindfmm  26650  lsslindf  26653  islindf4  26661  psgnunilem1  26769  psgnunilem5  26770  psgnunilem2  26771  psgnunilem3  26772  rusbcALT  26993  xrltneNEW  27011  stoweidlem14  27084  stoweidlem34  27104  stoweidlem59  27129  en3lpVD  27655  bnj23  27777  bnj1185  27859  bnj1476  27912  bnj1228  28074  bnj1388  28096  bnj1417  28104  cbvexvK  28164  hba1wK  28167  hbe1wK  28168  ax12o10lem3K  28186  ax12o10lem4K  28187  ax12o10lem8K  28195  ax12olem19K  28218  ax12olem21K  28222  ax10lem21X  28241  ax9X  28253  ax12-4  28257  equsexv-x12  28264  a12study10  28287  a12study10n  28288  lcvfbr  28361  lcvbr  28362  lsatcv0  28372  l1cvpat  28395  opltcon3b  28545  cvrfval  28609  cvrval  28610  cvrnbtwn  28612  cvrval2  28615  cvrnbtwn2  28616  cvrnbtwn3  28617  cvrcon3b  28618  cvrnbtwn4  28620  atnlt  28654  iscvlat  28664  cvlexch1  28669  hlsuprexch  28721  hlrelat5N  28741  hlrelat2  28743  cvrval5  28755  3dimlem1  28798  3dim1lem5  28806  3dim2  28808  3dim3  28809  llnnlt  28863  islpln5  28875  lplni2  28877  lvolex3N  28878  lplnnle2at  28881  islpln2a  28888  lplnribN  28891  lplnexllnN  28904  lplnnlt  28905  lvoli3  28917  islvol5  28919  lvoli2  28921  lvolnle3at  28922  islvol2aN  28932  4atlem11  28949  lvolnltN  28958  dalawlem15  29225  4atexlemex2  29411  4atex  29416  4atex2-0aOLDN  29418  4atex2-0cOLDN  29420  lautcvr  29432  ltrnfset  29457  ltrnset  29458  ltrnu  29461  trlfset  29500  trlset  29501  trlval2  29503  cdlemd6  29543  cdleme0nex  29630  cdleme18d  29635  cdleme25b  29694  cdleme25cv  29698  cdleme29b  29715  cdleme31fv  29730  cdleme31fv2  29733  cdlemefrs29bpre0  29736  cdlemefr32sn2aw  29744  cdlemefr29bpre0N  29746  cdlemefr29clN  29747  cdlemefr32fvaN  29749  cdlemefr32fva1  29750  cdlemefs32sn1aw  29754  cdleme32fva  29777  cdleme32fvaw  29779  cdleme40v  29809  cdleme42b  29818  cdleme46f2g2  29833  cdleme46f2g1  29834  cdleme48gfv  29877  cdlemg1fvawlemN  29913  cdlemg1cex  29928  cdlemg6d  29961  cdlemm10N  30459  dicffval  30515  dicfval  30516  dicval  30517  dicfnN  30524  dicvalrelN  30526  dihffval  30571  dihfval  30572  dihlsscpre  30575  dvh4dimat  30779  dvh3dimatN  30780  dvh4dimlem  30784  dvh3dim  30787  dvh4dimN  30788  dvh3dim2  30789  dvh3dim3N  30790  mapdcv  31001  mapdh9aOLDN  31132  hdmapfval  31171  hdmapval  31172  hdmapval2  31176  hdmap11lem2  31186
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator