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  926  xorbi12d  1308  cbvexvw  1678  hba1w  1682  hbe1w  1683  ax10lem2  1878  ax9  1890  equsex  1904  drex1  1909  cbvex  1927  cbvexd  1954  ax11inda  2140  eujustALT  2147  2mo  2222  neeq1  2455  neeq2  2456  necon3abid  2480  neleq1  2538  neleq2  2539  cbvrexf  2760  gencbval  2833  spcegf  2865  spc2gv  2872  spc3gv  2874  cdeqnot  2980  ru  2991  sbcng  3032  sbcrext  3065  sbcnel12g  3099  cbvrexcsf  3145  difjust  3155  eldif  3163  dfpss3  3263  difeq2  3289  disjne  3501  pssdifcom1  3540  pssdifcom2  3541  prel12  3790  disjxun  4022  nalset  4152  dtru  4200  dtruALT  4206  dtruALT2  4218  poeq1  4316  pocl  4320  swopo  4323  sotric  4339  sotrieq  4340  isso2i  4345  somo  4347  freq1  4362  frirr  4369  fr2nr  4370  frminex  4372  tz7.2  4376  wereu2  4389  nordeq  4410  ordtri1  4424  ordtri3  4427  rexxfrd  4548  rexxfr2d  4550  rexxfr  4553  elpwunsn  4567  fr3nr  4570  dfwe2  4572  ordsucsssuc  4613  nlimsucg  4632  orduninsuc  4633  dfom2  4657  ssnlim  4673  poinxp  4752  frinxp  4754  posn  4757  frsn  4759  rexiunxp  4825  rexxpf  4830  intirr  5060  poirr2  5066  cnvpo  5211  fvmpti  5562  fndmdif  5590  rexrnmpt  5631  f1imapss  5751  cbvexfo  5761  soisoi  5786  isopolem  5803  f1oweALT  5812  weniso  5813  rexrnmpt2  5920  ndmovg  5964  frxp  6186  poxp  6188  sorpssuni  6247  sorpssint  6248  canth  6287  pwnss  6292  riotaclbg  6339  smoword  6378  tz7.48lem  6448  abianfp  6466  oacan  6541  oaword  6542  omlimcl  6571  omeulem1  6575  nnaword  6620  nnmword  6626  nneob  6645  brdifun  6682  swoer  6683  undifixp  6847  boxcutc  6854  2dom  6928  php  7040  nndomo  7049  nnsdomo  7050  unxpdomlem2  7063  frfi  7097  unfilem1  7116  supmo  7198  eqsup  7202  supub  7205  supmaxlem  7210  suppr  7214  supisolem  7216  supisoex  7217  oieq1  7222  ordtypecbv  7227  ordtypelem7  7234  wemapso2lem  7260  canthwdom  7288  zfregcl  7303  elirrv  7306  elirr  7307  noinfep  7355  noinfepOLD  7356  cantnfp1lem3  7377  rankr1clem  7487  carden2b  7595  domtri2  7617  alephord3  7700  alephdom2  7709  alephval3  7732  dfac9  7757  kmlem2  7772  kmlem4  7774  isfin4  7918  isfin7  7922  fin23lem11  7938  isf32lem5  7978  isf34lem4  7998  fin1a2lem6  8026  fin1a2lem7  8027  fin1a2lem12  8032  itunisuc  8040  ac6n  8107  zorn2g  8125  zornn0g  8127  ttukeylem7  8137  axpowndlem2  8215  axpowndlem3  8216  axpowndlem4  8217  axregnd  8221  elgch  8239  engch  8245  fpwwe2lem13  8259  fpwwe2  8260  pwfseqlem1  8275  pwfseqlem3  8277  hargch  8294  addnidpi  8520  pinq  8546  nqereu  8548  ltsonq  8588  prlem934  8652  ltexprlem7  8661  addcanpr  8665  prlem936  8666  reclem2pr  8667  reclem3pr  8668  supexpr  8673  ltsosr  8711  supsrlem  8728  axpre-lttri  8782  axpre-sup  8786  xrlenlt  8885  axlttri  8889  axsup  8893  ltne  8912  readdcan  8981  leadd1  9237  ltsub1  9265  ltsub2  9266  leord1  9295  lediv1  9616  lemuldiv  9630  lerec  9633  le2msq  9651  lbinfm  9702  infm3  9708  suprnub  9712  infmrgelb  9729  infmrlb  9730  avgle1  9946  avgle2  9947  znnnlt1  10045  indstr  10282  zsupss  10302  uzsupss  10305  rpneg  10378  xralrple  10526  xleneg  10539  xltadd1  10570  xposdif  10576  xmulneg1  10583  xltmul1  10606  xrsupexmnf  10617  xrinfmexpnf  10618  xrsupsslem  10619  xrinfmsslem  10620  xrub  10624  supxrleub  10639  infmxrgelb  10647  difreicc  10761  leexp2  11150  hashbnd  11337  hasheni  11341  hashbc  11385  cnpart  11719  sqrlt  11741  limsuplt  11947  rlimrege0  12047  isercoll  12135  efle  12392  odd2np1  12581  divalglem7  12592  ndvdsadd  12601  bitsfval  12608  bitsval  12609  bits0  12613  bitsp1  12616  bitsmod  12621  bitscmp  12623  bitsinv1lem  12626  sadadd2lem2  12635  saddisjlem  12649  bitsshft  12660  gcdneg  12699  algcvgblem  12741  isprm3  12761  isprm5  12785  rpexp  12793  phiprmpw  12838  pythagtrip  12881  pcgcd1  12923  prmpwdvds  12945  prmreclem2  12958  prmreclem3  12959  prmreclem5  12961  prmreclem6  12962  vdwlem6  13027  vdwnnlem2  13037  vdwnnlem3  13038  vdwnn  13039  prmlem0  13101  prmlem1a  13102  divsfval  13443  mrisval  13526  ismri  13527  ismri2dad  13533  cidpropd  13607  plttr  14098  acsfiindd  14274  sylow1lem3  14905  sylow2alem2  14923  efgsfo  15042  ablfac1eulem  15301  ablfac1eu  15302  pgpfac1lem1  15303  pgpfac1lem5  15308  islbs  15823  lbsind  15827  lbspss  15829  lbspropd  15846  lspsnne1  15864  islbs2  15901  lbsacsbs  15903  lbsextlem1  15905  lbsextlem3  15907  lbsextlem4  15908  lbsextg  15909  nzrunit  16012  opsrtoslem2  16220  elcls  16804  maxlp  16872  perfi  16880  ordtbaslem  16912  ordtval  16913  ordtbas2  16915  ordtopn1  16918  ordtopn2  16919  ordtcnv  16925  ordtrest  16926  ordtrest2lem  16927  ordtrest2  16928  pnfnei  16944  mnfnei  16945  isreg2  17099  ordthauslem  17105  cmpfi  17129  cmpfii  17130  nconsubb  17143  hausdiag  17333  txkgen  17340  kqdisj  17417  ordthmeolem  17486  fbfinnfr  17530  trfbas  17533  fbunfip  17558  fbasrn  17573  trfil3  17577  ufileu  17608  fin1aufil  17621  hausflim  17670  alexsubALTlem2  17736  alexsubALTlem3  17737  alexsubALTlem4  17738  ptcmplem2  17741  ptcmplem3  17742  stdbdbl  18057  iccntr  18320  reconnlem2  18326  iccpnfcnv  18436  xrhmeo  18438  lebnumlem1  18453  lebnumlem2  18454  lebnumlem3  18455  bcthlem4  18743  minveclem3b  18786  ivthlem2  18806  ivthlem3  18807  mbfmax  18998  mbfposr  19001  i1fd  19030  mbfi1fseqlem4  19067  itg2splitlem  19097  itg2monolem1  19099  itg2cnlem1  19110  dvne0  19352  lhop1lem  19354  deg1nn0clb  19470  dgrle  19619  coemulhi  19629  aaliou3lem9  19724  cos11  19889  logleb  19951  argrege0  19959  logdivle  19967  ellogdm  19980  cxple  20036  cxplt2  20039  cxple3  20042  isosctrlem1  20112  atandm  20166  atans2  20221  atantayl2  20228  ftalem7  20310  isppw2  20347  musum  20425  dchrsum2  20501  bposlem1  20517  lgsmod  20554  lgsdir2lem2  20557  lgsdir2  20561  lgsne0  20566  lgsquadlem1  20587  rpvmasumlem  20630  padicabv  20773  ostth3  20781  ostth  20782  lpni  20838  nmobndseqi  21349  minvecolem5  21452  chpsscon3  22074  chnle  22085  nonbooli  22222  pjnel  22297  specval  22470  nmcfnlbi  22624  stri  22829  hstri  22837  cvbr  22854  cvcon3  22856  chcv1  22927  cvexchlem  22940  chrelat2  22942  ifeqeqx  23026  ballotlemfc0  23044  ballotlemfcc  23045  ballotlem4  23050  ballotlemi1  23054  ballotlemii  23055  ballotlemimin  23057  ballotlem7  23087  eldmgm  23098  erdszelem10  23135  eupath2lem3  23307  eupath2  23308  konigsberg  23315  untelirr  23458  untsucf  23460  untangtr  23464  dedekind  23485  inffz  23498  dfpo2  23515  dfon2lem3  23542  dfon2lem4  23543  dfon2lem7  23546  dfon2lem9  23548  distel  23561  predpoirr  23598  predfrirr  23599  soseq  23655  axdenselem4  23739  axdenselem5  23740  nocvxminlem  23745  axfelem14  23760  elfuns  23861  funpartfv  23890  dfrdg4  23895  axlowdimlem16  23992  axlowdim2  23995  axlowdim  23996  nabi1  24235  nabi2  24236  limsucncmpi  24291  limsucncmp  24292  ordcmp  24293  vxveqv  24452  inttpemp  24538  dstr  24570  nelioo5  24910  bwt2  24991  iintlem1  25009  tethpnc2  25470  pdiveql  25567  nn0prpwlem  25637  nn0prpw  25638  heibor1lem  25932  heiborlem1  25934  heiborlem6  25939  heiborlem8  25941  heiborlem10  25943  smprngopr  26076  ellz1  26245  rencldnfilem  26302  jm2.22  26487  jm2.23  26488  wepwsolem  26537  fnwe2lem2  26547  supeq123d  26557  aomclem8  26558  frlmlbs  26648  unxpwdom3  26655  islindf  26681  islinds2  26682  islindf2  26683  lindfind  26685  lindsind  26686  lindfrn  26690  lindfmm  26696  lsslindf  26699  islindf4  26707  psgnunilem1  26815  psgnunilem5  26816  psgnunilem2  26817  psgnunilem3  26818  rusbcALT  27038  xrltneNEW  27056  stoweidlem14  27162  stoweidlem34  27182  stoweidlem59  27207  afvfv0bi  27392  afvco2  27414  ndmaovg  27423  eldifpr  27521  eldiftp  27522  en3lpVD  27889  bnj23  28011  bnj1185  28093  bnj1476  28146  bnj1228  28308  bnj1388  28330  bnj1417  28338  ax12-4  28373  equsexv-x12  28380  a12study10  28403  a12study10n  28404  lcvfbr  28477  lcvbr  28478  lsatcv0  28488  l1cvpat  28511  opltcon3b  28661  cvrfval  28725  cvrval  28726  cvrnbtwn  28728  cvrval2  28731  cvrnbtwn2  28732  cvrnbtwn3  28733  cvrcon3b  28734  cvrnbtwn4  28736  atnlt  28770  iscvlat  28780  cvlexch1  28785  hlsuprexch  28837  hlrelat5N  28857  hlrelat2  28859  cvrval5  28871  3dimlem1  28914  3dim1lem5  28922  3dim2  28924  3dim3  28925  llnnlt  28979  islpln5  28991  lplni2  28993  lvolex3N  28994  lplnnle2at  28997  islpln2a  29004  lplnribN  29007  lplnexllnN  29020  lplnnlt  29021  lvoli3  29033  islvol5  29035  lvoli2  29037  lvolnle3at  29038  islvol2aN  29048  4atlem11  29065  lvolnltN  29074  dalawlem15  29341  4atexlemex2  29527  4atex  29532  4atex2-0aOLDN  29534  4atex2-0cOLDN  29536  lautcvr  29548  ltrnfset  29573  ltrnset  29574  ltrnu  29577  trlfset  29616  trlset  29617  trlval2  29619  cdlemd6  29659  cdleme0nex  29746  cdleme18d  29751  cdleme25b  29810  cdleme25cv  29814  cdleme29b  29831  cdleme31fv  29846  cdleme31fv2  29849  cdlemefrs29bpre0  29852  cdlemefr32sn2aw  29860  cdlemefr29bpre0N  29862  cdlemefr29clN  29863  cdlemefr32fvaN  29865  cdlemefr32fva1  29866  cdlemefs32sn1aw  29870  cdleme32fva  29893  cdleme32fvaw  29895  cdleme40v  29925  cdleme42b  29934  cdleme46f2g2  29949  cdleme46f2g1  29950  cdleme48gfv  29993  cdlemg1fvawlemN  30029  cdlemg1cex  30044  cdlemg6d  30077  cdlemm10N  30575  dicffval  30631  dicfval  30632  dicval  30633  dicfnN  30640  dicvalrelN  30642  dihffval  30687  dihfval  30688  dihlsscpre  30691  dvh4dimat  30895  dvh3dimatN  30896  dvh4dimlem  30900  dvh3dim  30903  dvh4dimN  30904  dvh3dim2  30905  dvh3dim3N  30906  mapdcv  31117  mapdh9aOLDN  31248  hdmapfval  31287  hdmapval  31288  hdmapval2  31292  hdmap11lem2  31302
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