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  eldmgm  23105  erdszelem10  23142  eupath2lem3  23314  eupath2  23315  konigsberg  23322  untelirr  23465  untsucf  23467  untangtr  23471  dedekind  23493  inffz  23506  dfpo2  23523  dfon2lem3  23552  dfon2lem4  23553  dfon2lem7  23556  dfon2lem9  23558  distel  23571  predpoirr  23608  predfrirr  23609  soseq  23665  nodenselem4  23749  nodenselem5  23750  nocvxminlem  23755  nofulllem4  23770  funpartfv  23894  dfrdg4  23899  axlowdimlem16  23996  axlowdim2  23999  axlowdim  24000  nabi1  24239  nabi2  24240  limsucncmpi  24295  limsucncmp  24296  ordcmp  24297  areacirc  24343  vxveqv  24466  inttpemp  24551  dstr  24583  nelioo5  24923  bwt2  25004  iintlem1  25022  tethpnc2  25483  pdiveql  25580  nn0prpwlem  25650  nn0prpw  25651  heibor1lem  25945  heiborlem1  25947  heiborlem6  25952  heiborlem8  25954  heiborlem10  25956  smprngopr  26089  ellz1  26258  rencldnfilem  26315  jm2.22  26500  jm2.23  26501  wepwsolem  26550  fnwe2lem2  26560  supeq123d  26570  aomclem8  26571  frlmlbs  26661  unxpwdom3  26668  islindf  26694  islinds2  26695  islindf2  26696  lindfind  26698  lindsind  26699  lindfrn  26703  lindfmm  26709  lsslindf  26712  islindf4  26720  psgnunilem1  26828  psgnunilem5  26829  psgnunilem2  26830  psgnunilem3  26831  rusbcALT  27051  xrltneNEW  27069  stoweidlem14  27175  stoweidlem34  27195  stoweidlem59  27220  afvfv0bi  27427  afvco2  27449  ndmaovg  27456  frgra2v  27539  eldifpr  27623  eldiftp  27624  en3lpVD  27994  bnj23  28117  bnj1185  28199  bnj1476  28252  bnj1228  28414  bnj1388  28436  bnj1417  28444  ax12-4  28479  equsexv-x12  28486  a12study10  28509  a12study10n  28510  lcvfbr  28583  lcvbr  28584  lsatcv0  28594  l1cvpat  28617  opltcon3b  28767  cvrfval  28831  cvrval  28832  cvrnbtwn  28834  cvrval2  28837  cvrnbtwn2  28838  cvrnbtwn3  28839  cvrcon3b  28840  cvrnbtwn4  28842  atnlt  28876  iscvlat  28886  cvlexch1  28891  hlsuprexch  28943  hlrelat5N  28963  hlrelat2  28965  cvrval5  28977  3dimlem1  29020  3dim1lem5  29028  3dim2  29030  3dim3  29031  llnnlt  29085  islpln5  29097  lplni2  29099  lvolex3N  29100  lplnnle2at  29103  islpln2a  29110  lplnribN  29113  lplnexllnN  29126  lplnnlt  29127  lvoli3  29139  islvol5  29141  lvoli2  29143  lvolnle3at  29144  islvol2aN  29154  4atlem11  29171  lvolnltN  29180  dalawlem15  29447  4atexlemex2  29633  4atex  29638  4atex2-0aOLDN  29640  4atex2-0cOLDN  29642  lautcvr  29654  ltrnfset  29679  ltrnset  29680  ltrnu  29683  trlfset  29722  trlset  29723  trlval2  29725  cdlemd6  29765  cdleme0nex  29852  cdleme18d  29857  cdleme25b  29916  cdleme25cv  29920  cdleme29b  29937  cdleme31fv  29952  cdleme31fv2  29955  cdlemefrs29bpre0  29958  cdlemefr32sn2aw  29966  cdlemefr29bpre0N  29968  cdlemefr29clN  29969  cdlemefr32fvaN  29971  cdlemefr32fva1  29972  cdlemefs32sn1aw  29976  cdleme32fva  29999  cdleme32fvaw  30001  cdleme40v  30031  cdleme42b  30040  cdleme46f2g2  30055  cdleme46f2g1  30056  cdleme48gfv  30099  cdlemg1fvawlemN  30135  cdlemg1cex  30150  cdlemg6d  30183  cdlemm10N  30681  dicffval  30737  dicfval  30738  dicval  30739  dicfnN  30746  dicvalrelN  30748  dihffval  30793  dihfval  30794  dihlsscpre  30797  dvh4dimat  31001  dvh3dimatN  31002  dvh4dimlem  31006  dvh3dim  31009  dvh4dimN  31010  dvh3dim2  31011  dvh3dim3N  31012  mapdcv  31223  mapdh9aOLDN  31354  hdmapfval  31393  hdmapval  31394  hdmapval2  31398  hdmap11lem2  31408
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