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  2713  gencbval  2783  cla4egf  2815  cla42gv  2822  cla43gv  2824  cdeqnot  2923  ru  2934  sbcng  2975  sbcrext  3008  sbcnel12g  3040  cbvrexcsf  3086  difjust  3096  eldif  3104  dfpss3  3204  difeq2  3230  disjne  3442  pssdifcom1  3481  pssdifcom2  3482  prel12  3730  disjxun  3961  nalset  4091  dtru  4139  dtruALT  4145  dtruALT2  4157  poeq1  4254  pocl  4258  swopo  4261  sotric  4277  sotrieq  4278  isso2i  4283  somo  4285  freq1  4300  frirr  4307  fr2nr  4308  frminex  4310  tz7.2  4314  wereu2  4327  nordeq  4348  ordtri1  4362  ordtri3  4365  rexxfrd  4486  rexxfr2d  4488  rexxfr  4491  elpwunsn  4505  fr3nr  4508  dfwe2  4510  ordsucsssuc  4551  nlimsucg  4570  orduninsuc  4571  dfom2  4595  ssnlim  4611  poinxp  4706  frinxp  4708  posn  4711  frsn  4713  rexiunxp  4779  rexxpf  4784  intirr  5014  poirr2  5020  cnvpo  5165  fvmpti  5500  fndmdif  5528  rexrnmpt  5569  f1imapss  5689  cbvexfo  5699  soisoi  5724  isopolem  5741  f1oweALT  5750  weniso  5751  rexrnmpt2  5858  ndmovg  5902  frxp  6124  poxp  6126  sorpssuni  6185  sorpssint  6186  canth  6225  pwnss  6230  riotaclbg  6277  smoword  6316  tz7.48lem  6386  abianfp  6404  oacan  6479  oaword  6480  omlimcl  6509  omeulem1  6513  nnaword  6558  nnmword  6564  nneob  6583  brdifun  6620  swoer  6621  undifixp  6785  boxcutc  6792  2dom  6866  php  6978  nndomo  6987  nnsdomo  6988  unxpdomlem2  7001  frfi  7035  unfilem1  7054  supmo  7136  eqsup  7140  supub  7143  supmaxlem  7148  suppr  7152  supisolem  7154  supisoex  7155  oieq1  7160  ordtypecbv  7165  ordtypelem7  7172  wemapso2lem  7198  canthwdom  7226  zfregcl  7241  elirrv  7244  elirr  7245  noinfep  7293  noinfepOLD  7294  cantnfp1lem3  7315  rankr1clem  7425  carden2b  7533  domtri2  7555  alephord3  7638  alephdom2  7647  alephval3  7670  dfac9  7695  kmlem2  7710  kmlem4  7712  isfin4  7856  isfin7  7860  fin23lem11  7876  isf32lem5  7916  isf34lem4  7936  fin1a2lem6  7964  fin1a2lem7  7965  fin1a2lem12  7970  itunisuc  7978  ac6n  8045  zorn2g  8063  zornn0g  8065  ttukeylem7  8075  axpowndlem2  8153  axpowndlem3  8154  axpowndlem4  8155  axregnd  8159  elgch  8177  engch  8183  fpwwe2lem13  8197  fpwwe2  8198  pwfseqlem1  8213  pwfseqlem3  8215  hargch  8232  addnidpi  8458  pinq  8484  nqereu  8486  ltsonq  8526  prlem934  8590  ltexprlem7  8599  addcanpr  8603  prlem936  8604  reclem2pr  8605  reclem3pr  8606  supexpr  8611  ltsosr  8649  supsrlem  8666  axpre-lttri  8720  axpre-sup  8724  xrlenlt  8823  axlttri  8827  axsup  8831  ltne  8850  readdcan  8919  leadd1  9175  ltsub1  9203  ltsub2  9204  leord1  9233  lediv1  9554  lemuldiv  9568  lerec  9571  le2msq  9589  lbinfm  9640  infm3  9646  suprnub  9650  infmrgelb  9667  infmrlb  9668  avgle1  9883  avgle2  9884  znnnlt1  9982  indstr  10219  zsupss  10239  uzsupss  10242  rpneg  10315  xralrple  10463  xleneg  10476  xltadd1  10507  xposdif  10513  xmulneg1  10520  xltmul1  10543  xrsupexmnf  10554  xrinfmexpnf  10555  xrsupsslem  10556  xrinfmsslem  10557  xrub  10561  supxrleub  10576  infmxrgelb  10584  difreicc  10698  leexp2  11087  hashbnd  11274  hasheni  11278  hashbc  11321  cnpart  11655  sqrlt  11677  limsuplt  11883  rlimrege0  11983  isercoll  12071  efle  12325  odd2np1  12514  divalglem7  12525  ndvdsadd  12534  bitsfval  12541  bitsval  12542  bits0  12546  bitsp1  12549  bitsmod  12554  bitscmp  12556  bitsinv1lem  12559  sadadd2lem2  12568  saddisjlem  12582  bitsshft  12593  gcdneg  12632  algcvgblem  12674  isprm3  12694  isprm5  12718  rpexp  12726  phiprmpw  12771  pythagtrip  12814  pcgcd1  12856  prmpwdvds  12878  prmreclem2  12891  prmreclem3  12892  prmreclem5  12894  prmreclem6  12895  vdwlem6  12960  vdwnnlem2  12970  vdwnnlem3  12971  vdwnn  12972  prmlem0  13034  prmlem1a  13035  divsfval  13376  mrisval  13459  ismri  13460  ismri2dad  13466  cidpropd  13540  plttr  14031  acsfiindd  14207  sylow1lem3  14838  sylow2alem2  14856  efgsfo  14975  ablfac1eulem  15234  ablfac1eu  15235  pgpfac1lem1  15236  pgpfac1lem5  15241  islbs  15756  lbsind  15760  lbspss  15762  lbspropd  15779  lspsnne1  15797  islbs2  15834  lbsacsbs  15836  lbsextlem1  15838  lbsextlem3  15840  lbsextlem4  15841  lbsextg  15842  nzrunit  15945  opsrtoslem2  16153  elcls  16737  maxlp  16805  perfi  16813  ordtbaslem  16845  ordtval  16846  ordtbas2  16848  ordtopn1  16851  ordtopn2  16852  ordtcnv  16858  ordtrest  16859  ordtrest2lem  16860  ordtrest2  16861  pnfnei  16877  mnfnei  16878  isreg2  17032  ordthauslem  17038  cmpfi  17062  cmpfii  17063  nconsubb  17076  hausdiag  17266  txkgen  17273  kqdisj  17350  ordthmeolem  17419  fbfinnfr  17463  trfbas  17466  fbunfip  17491  fbasrn  17506  trfil3  17510  ufileu  17541  fin1aufil  17554  hausflim  17603  alexsubALTlem2  17669  alexsubALTlem3  17670  alexsubALTlem4  17671  ptcmplem2  17674  ptcmplem3  17675  stdbdbl  17990  iccntr  18253  reconnlem2  18259  iccpnfcnv  18369  xrhmeo  18371  lebnumlem1  18386  lebnumlem2  18387  lebnumlem3  18388  bcthlem4  18676  minveclem3b  18719  ivthlem2  18739  ivthlem3  18740  mbfmax  18931  mbfposr  18934  i1fd  18963  mbfi1fseqlem4  19000  itg2splitlem  19030  itg2monolem1  19032  itg2cnlem1  19043  dvne0  19285  lhop1lem  19287  deg1nn0clb  19403  dgrle  19552  coemulhi  19562  aaliou3lem9  19657  cos11  19822  logleb  19884  argrege0  19892  logdivle  19900  ellogdm  19913  cxple  19969  cxplt2  19972  cxple3  19975  isosctrlem1  20045  atandm  20099  atans2  20154  atantayl2  20161  ftalem7  20243  isppw2  20280  musum  20358  dchrsum2  20434  bposlem1  20450  lgsmod  20487  lgsdir2lem2  20490  lgsdir2  20494  lgsne0  20499  lgsquadlem1  20520  rpvmasumlem  20563  padicabv  20706  ostth3  20714  ostth  20715  lpni  20771  nmobndseqi  21282  minvecolem5  21385  chpsscon3  22007  chnle  22018  nonbooli  22173  pjnel  22248  specval  22403  nmcfnlbi  22557  stri  22762  hstri  22770  cvbr  22787  cvcon3  22789  chcv1  22860  cvexchlem  22873  chrelat2  22875  ifeqeqx  22959  ballotlemfc0  22977  ballotlemfcc  22978  ballotlem4  22983  ballotlemi1  22987  ballotlemii  22988  ballotlemimin  22990  ballotlem7  23020  eldmgm  23031  erdszelem10  23068  eupath2lem3  23240  eupath2  23241  konigsberg  23248  untelirr  23391  untsucf  23393  untangtr  23397  dedekind  23418  inffz  23431  dfpo2  23448  dfon2lem3  23475  dfon2lem4  23476  dfon2lem7  23479  dfon2lem9  23481  distel  23494  predpoirr  23531  predfrirr  23532  soseq  23588  axdenselem4  23672  axdenselem5  23673  nocvxminlem  23678  axfelem14  23693  elfuns  23794  funpartfv  23823  dfrdg4  23828  axlowdimlem16  23925  axlowdim2  23928  axlowdim  23929  nabi1  24168  nabi2  24169  limsucncmpi  24224  limsucncmp  24225  ordcmp  24226  vxveqv  24385  inttpemp  24471  dstr  24503  nelioo5  24843  bwt2  24924  iintlem1  24942  tethpnc2  25403  pdiveql  25500  nn0prpwlem  25570  nn0prpw  25571  heibor1lem  25865  heiborlem1  25867  heiborlem6  25872  heiborlem8  25874  heiborlem10  25876  smprngopr  26009  ellz1  26178  rencldnfilem  26235  jm2.22  26420  jm2.23  26421  wepwsolem  26470  fnwe2lem2  26480  supeq123d  26490  aomclem8  26491  frlmlbs  26581  unxpwdom3  26588  islindf  26614  islinds2  26615  islindf2  26616  lindfind  26618  lindsind  26619  lindfrn  26623  lindfmm  26629  lsslindf  26632  islindf4  26640  psgnunilem1  26748  psgnunilem5  26749  psgnunilem2  26750  psgnunilem3  26751  rusbcALT  26972  xrltneNEW  26990  stoweidlem14  27063  stoweidlem34  27083  stoweidlem59  27108  en3lpVD  27634  bnj23  27756  bnj1185  27838  bnj1476  27891  bnj1228  28053  bnj1388  28075  bnj1417  28083  cbvexvK  28143  hba1wK  28146  hbe1wK  28147  ax12o10lem3K  28165  ax12o10lem4K  28166  ax12o10lem8K  28174  ax12olem19K  28197  ax12olem21K  28201  ax10lem21X  28220  ax9X  28232  ax12-4  28236  equsexv-x12  28243  a12study10  28266  a12study10n  28267  lcvfbr  28340  lcvbr  28341  lsatcv0  28351  l1cvpat  28374  opltcon3b  28524  cvrfval  28588  cvrval  28589  cvrnbtwn  28591  cvrval2  28594  cvrnbtwn2  28595  cvrnbtwn3  28596  cvrcon3b  28597  cvrnbtwn4  28599  atnlt  28633  iscvlat  28643  cvlexch1  28648  hlsuprexch  28700  hlrelat5N  28720  hlrelat2  28722  cvrval5  28734  3dimlem1  28777  3dim1lem5  28785  3dim2  28787  3dim3  28788  llnnlt  28842  islpln5  28854  lplni2  28856  lvolex3N  28857  lplnnle2at  28860  islpln2a  28867  lplnribN  28870  lplnexllnN  28883  lplnnlt  28884  lvoli3  28896  islvol5  28898  lvoli2  28900  lvolnle3at  28901  islvol2aN  28911  4atlem11  28928  lvolnltN  28937  dalawlem15  29204  4atexlemex2  29390  4atex  29395  4atex2-0aOLDN  29397  4atex2-0cOLDN  29399  lautcvr  29411  ltrnfset  29436  ltrnset  29437  ltrnu  29440  trlfset  29479  trlset  29480  trlval2  29482  cdlemd6  29522  cdleme0nex  29609  cdleme18d  29614  cdleme25b  29673  cdleme25cv  29677  cdleme29b  29694  cdleme31fv  29709  cdleme31fv2  29712  cdlemefrs29bpre0  29715  cdlemefr32sn2aw  29723  cdlemefr29bpre0N  29725  cdlemefr29clN  29726  cdlemefr32fvaN  29728  cdlemefr32fva1  29729  cdlemefs32sn1aw  29733  cdleme32fva  29756  cdleme32fvaw  29758  cdleme40v  29788  cdleme42b  29797  cdleme46f2g2  29812  cdleme46f2g1  29813  cdleme48gfv  29856  cdlemg1fvawlemN  29892  cdlemg1cex  29907  cdlemg6d  29940  cdlemm10N  30438  dicffval  30494  dicfval  30495  dicval  30496  dicfnN  30503  dicvalrelN  30505  dihffval  30550  dihfval  30551  dihlsscpre  30554  dvh4dimat  30758  dvh3dimatN  30759  dvh4dimlem  30763  dvh3dim  30766  dvh4dimN  30767  dvh3dim2  30768  dvh3dim3N  30769  mapdcv  30980  mapdh9aOLDN  31111  hdmapfval  31150  hdmapval  31151  hdmapval2  31155  hdmap11lem2  31165
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