MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notbid Structured version   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 3    -> wi 4    <-> wb 178
This theorem is referenced by:  notbi  288  con3th  926  nanbi1  1305  xorbi12d  1325  cbvexvw  1718  hba1w  1723  hbe1w  1724  cbvex  1984  cbvexd  1989  equsexOLD  2004  ax10lem2OLD  2027  ax9OLD  2034  drex1  2060  ax11inda  2279  eujustALT  2286  2mo  2361  neeq1  2611  neeq2  2612  necon3abid  2636  neleq1  2701  neleq2  2702  cbvrexf  2929  gencbval  3002  spcegf  3034  spc2gv  3041  spc3gv  3043  cdeqnot  3151  ru  3162  sbcng  3203  sbcrext  3236  sbcnel12g  3270  cbvrexcsf  3314  difjust  3324  eldif  3332  dfpss3  3435  difeq2  3461  disjne  3675  pssdifcom1  3715  pssdifcom2  3716  prel12  3977  disjxun  4213  nalset  4343  pwnss  4368  dtru  4393  dtruALT  4399  dtruALT2  4411  poeq1  4509  pocl  4513  swopo  4516  sotric  4532  sotrieq  4533  isso2i  4538  somo  4540  freq1  4555  frirr  4562  fr2nr  4563  frminex  4565  tz7.2  4569  wereu2  4582  nordeq  4603  ordtri1  4617  ordtri3  4620  rexxfrd  4741  rexxfr2d  4743  rexxfr  4746  elpwunsn  4760  fr3nr  4763  dfwe2  4765  ordsucsssuc  4806  nlimsucg  4825  orduninsuc  4826  dfom2  4850  ssnlim  4866  poinxp  4944  frinxp  4946  posn  4949  frsn  4951  rexiunxp  5018  rexxpf  5023  intirr  5255  poirr2  5261  cnvpo  5413  fvmpti  5808  fndmdif  5837  rexrnmpt  5882  f1imapss  6015  cbvexfo  6026  soisoi  6051  isopolem  6068  f1oweALT  6077  weniso  6078  rexrnmpt2  6188  ndmovg  6233  frxp  6459  poxp  6461  sorpssuni  6534  sorpssint  6535  canth  6542  riotaclbg  6592  smoword  6631  tz7.48lem  6701  abianfp  6719  oacan  6794  oaword  6795  omlimcl  6824  omeulem1  6828  nnaword  6873  nnmword  6879  nneob  6898  brdifun  6935  swoer  6936  undifixp  7101  boxcutc  7108  2dom  7182  php  7294  nndomo  7303  nnsdomo  7304  unxpdomlem2  7317  frfi  7355  unfilem1  7374  supeq3  7457  supeq123d  7458  supmo  7460  eqsup  7464  supub  7467  supmaxlem  7472  suppr  7476  supisolem  7478  supisoex  7479  oieq1  7484  ordtypecbv  7489  ordtypelem7  7496  wemapso2lem  7522  canthwdom  7550  zfregcl  7565  elirrv  7568  elirr  7569  noinfep  7617  noinfepOLD  7618  cantnfp1lem3  7639  rankr1clem  7749  carden2b  7859  domtri2  7881  alephord3  7964  alephdom2  7973  alephval3  7996  dfac9  8021  kmlem2  8036  kmlem4  8038  isfin4  8182  isfin7  8186  fin23lem11  8202  isf32lem5  8242  isf34lem4  8262  fin1a2lem6  8290  fin1a2lem7  8291  fin1a2lem12  8296  itunisuc  8304  ac6n  8370  zorn2g  8388  zornn0g  8390  ttukeylem7  8400  axpowndlem2  8478  axpowndlem3  8479  axpowndlem4  8480  axregnd  8484  elgch  8502  engch  8508  fpwwe2lem13  8522  fpwwe2  8523  pwfseqlem1  8538  pwfseqlem3  8540  hargch  8553  addnidpi  8783  pinq  8809  nqereu  8811  ltsonq  8851  prlem934  8915  ltexprlem7  8924  addcanpr  8928  prlem936  8929  reclem2pr  8930  reclem3pr  8931  supexpr  8936  ltsosr  8974  supsrlem  8991  axpre-lttri  9045  axpre-sup  9049  xrlenlt  9148  axlttri  9152  axsup  9156  ltne  9175  readdcan  9245  leadd1  9501  ltsub1  9529  ltsub2  9530  leord1  9559  lediv1  9880  lemuldiv  9894  lerec  9897  le2msq  9915  lbinfm  9966  infm3  9972  suprnub  9976  infmrgelb  9993  infmrlb  9994  avgle1  10212  avgle2  10213  znnnlt1  10313  indstr  10550  zsupss  10570  uzsupss  10573  rpneg  10646  xralrple  10796  xleneg  10809  xltadd1  10840  xposdif  10846  xmulneg1  10853  xltmul1  10876  xrsupexmnf  10888  xrinfmexpnf  10889  xrsupsslem  10890  xrinfmsslem  10891  xrub  10895  supxrleub  10910  infmxrgelb  10918  difreicc  11033  elfznelfzo  11197  injresinjlem  11204  leexp2  11439  hashbnd  11629  hasheni  11637  hashbc  11707  cnpart  12050  sqrlt  12072  limsuplt  12278  rlimrege0  12378  isercoll  12466  efle  12724  odd2np1  12913  divalglem7  12924  ndvdsadd  12933  bitsfval  12940  bitsval  12941  bits0  12945  bitsp1  12948  bitsmod  12953  bitscmp  12955  bitsinv1lem  12958  sadadd2lem2  12967  saddisjlem  12981  bitsshft  12992  gcdneg  13031  algcvgblem  13073  isprm3  13093  isprm5  13117  rpexp  13125  phiprmpw  13170  pythagtrip  13213  pcgcd1  13255  prmpwdvds  13277  prmreclem2  13290  prmreclem3  13291  prmreclem5  13293  prmreclem6  13294  vdwlem6  13359  vdwnnlem2  13369  vdwnnlem3  13370  vdwnn  13371  prmlem0  13433  prmlem1a  13434  divsfval  13777  mrisval  13860  ismri  13861  ismri2dad  13867  cidpropd  13941  plttr  14432  acsfiindd  14608  sylow1lem3  15239  sylow2alem2  15257  efgsfo  15376  ablfac1eulem  15635  ablfac1eu  15636  pgpfac1lem1  15637  pgpfac1lem5  15642  islbs  16153  lbsind  16157  lbspss  16159  lbspropd  16176  lspsnne1  16194  islbs2  16231  lbsacsbs  16233  lbsextlem1  16235  lbsextlem3  16237  lbsextlem4  16238  lbsextg  16239  nzrunit  16342  opsrtoslem2  16550  elcls  17142  maxlp  17216  perfi  17224  ordtbaslem  17257  ordtval  17258  ordtbas2  17260  ordtopn1  17263  ordtopn2  17264  ordtcnv  17270  ordtrest  17271  ordtrest2lem  17272  ordtrest2  17273  pnfnei  17289  mnfnei  17290  isreg2  17446  ordthauslem  17452  cmpfi  17476  cmpfii  17477  bwth  17478  nconsubb  17491  hausdiag  17682  txkgen  17689  kqdisj  17769  ordthmeolem  17838  fbfinnfr  17878  trfbas  17881  fbunfip  17906  fbasrn  17921  trfil3  17925  ufileu  17956  fin1aufil  17969  hausflim  18018  alexsubALTlem2  18084  alexsubALTlem3  18085  alexsubALTlem4  18086  ptcmplem2  18089  ptcmplem3  18090  stdbdbl  18552  iccntr  18857  reconnlem2  18863  iccpnfcnv  18974  xrhmeo  18976  lebnumlem1  18991  lebnumlem2  18992  lebnumlem3  18993  bcthlem4  19285  minveclem3b  19334  ivthlem2  19354  ivthlem3  19355  mbfmax  19544  mbfposr  19547  i1fd  19576  mbfi1fseqlem4  19613  itg2splitlem  19643  itg2monolem1  19645  itg2cnlem1  19656  dvne0  19900  lhop1lem  19902  deg1nn0clb  20018  dgrle  20167  coemulhi  20177  aaliou3lem9  20272  cos11  20440  logleb  20503  argrege0  20511  logdivle  20522  ellogdm  20535  cxple  20591  cxplt2  20594  cxple3  20597  isosctrlem1  20667  atandm  20721  atans2  20776  atantayl2  20783  ftalem7  20866  isppw2  20903  musum  20981  dchrsum2  21057  bposlem1  21073  lgsmod  21110  lgsdir2lem2  21113  lgsdir2  21117  lgsne0  21122  lgsquadlem1  21143  rpvmasumlem  21186  padicabv  21329  ostth3  21337  ostth  21338  usgra1v  21414  usgraidx2v  21417  nbgra0nb  21446  cusgrafilem3  21495  spthispth  21578  wlkdvspthlem  21612  eupath2lem3  21706  eupath2  21707  konigsberg  21714  lpni  21772  nmobndseqi  22285  minvecolem5  22388  chpsscon3  23010  chnle  23021  nonbooli  23158  pjnel  23233  specval  23406  nmcfnlbi  23560  stri  23765  hstri  23773  cvbr  23790  cvcon3  23792  chcv1  23863  cvexchlem  23876  chrelat2  23878  elpreq  24004  ifeqeqx  24006  ifbieq12d2  24007  isoun  24094  eliccelico  24145  elicoelioo  24146  toslub  24196  tosglb  24197  isarchi2  24260  xrge0iifcnv  24324  elzdif0  24369  eldifpr  24397  eldiftp  24398  esumpcvgval  24473  ballotlemfc0  24755  ballotlemfcc  24756  ballotlem4  24761  ballotlemimin  24768  ballotlem7  24798  eldmgm  24811  erdszelem10  24891  untelirr  25162  untsucf  25164  untangtr  25168  dedekind  25192  inffz  25205  dfpo2  25383  dfon2lem3  25417  dfon2lem4  25418  dfon2lem7  25421  dfon2lem9  25423  distel  25436  predpoirr  25477  predfrirr  25478  soseq  25534  wfrlem10  25552  nodenselem4  25644  nodenselem5  25645  nocvxminlem  25650  nofulllem4  25665  funpartfv  25795  dfrdg4  25800  axlowdimlem16  25901  axlowdim2  25904  axlowdim  25905  limsucncmpi  26200  limsucncmp  26201  ordcmp  26202  leceifl  26248  mblfinlem2  26256  mblfinlem3  26257  ismblfin  26259  cnambfre  26267  dvtanlem  26268  itg2addnclem  26270  itg2addnclem2  26271  iblabsnclem  26282  ftc1anclem1  26294  areacirc  26311  nn0prpwlem  26339  nn0prpw  26340  heibor1lem  26532  heiborlem1  26534  heiborlem6  26539  heiborlem8  26541  heiborlem10  26543  smprngopr  26676  ellz1  26839  rencldnfilem  26895  jm2.22  27080  jm2.23  27081  wepwsolem  27130  fnwe2lem2  27140  aomclem8  27150  frlmlbs  27240  unxpwdom3  27247  islindf  27273  islinds2  27274  islindf2  27275  lindfind  27277  lindsind  27278  lindfrn  27282  lindfmm  27288  lsslindf  27291  islindf4  27299  psgnunilem1  27407  psgnunilem5  27408  psgnunilem2  27409  psgnunilem3  27410  rusbcALT  27630  xrltneNEW  27647  stoweidlem14  27753  stoweidlem34  27773  stoweidlem59  27798  eu2ndop1stv  27970  afvfv0bi  28006  afvco2  28030  ndmaovg  28038  otiunsndisj  28081  otiunsndisjX  28082  rexxfrd2  28088  2f1fvneq  28095  ltnltne  28117  wrdsymb0  28202  swrdnd  28216  swrdvalodm2  28222  swrdvalodm  28223  2cshwmod  28291  lswrd0  28295  2cshwcom  28301  frgra2v  28463  frgrancvvdeqlem2  28494  2spotiundisj  28525  usg2spot2nb  28528  2spotmdisj  28531  en3lpVD  29031  bnj23  29157  bnj1185  29239  bnj1476  29292  bnj1228  29454  bnj1388  29476  bnj1417  29484  ax9NEW7  29542  equsexNEW7  29564  drex1NEW7  29568  cbvexwAUX7  29594  cbvexOLD7  29800  cbvexdOLD7  29809  lcvfbr  29892  lcvbr  29893  lsatcv0  29903  l1cvpat  29926  opltcon3b  30076  cvrfval  30140  cvrval  30141  cvrnbtwn  30143  cvrval2  30146  cvrnbtwn2  30147  cvrnbtwn3  30148  cvrcon3b  30149  cvrnbtwn4  30151  atnlt  30185  iscvlat  30195  cvlexch1  30200  hlsuprexch  30252  hlrelat5N  30272  hlrelat2  30274  cvrval5  30286  3dimlem1  30329  3dim1lem5  30337  3dim2  30339  3dim3  30340  llnnlt  30394  islpln5  30406  lplni2  30408  lvolex3N  30409  lplnnle2at  30412  islpln2a  30419  lplnribN  30422  lplnexllnN  30435  lplnnlt  30436  lvoli3  30448  islvol5  30450  lvoli2  30452  lvolnle3at  30453  islvol2aN  30463  4atlem11  30480  lvolnltN  30489  dalawlem15  30756  4atexlemex2  30942  4atex  30947  4atex2-0aOLDN  30949  4atex2-0cOLDN  30951  lautcvr  30963  ltrnfset  30988  ltrnset  30989  ltrnu  30992  trlfset  31031  trlset  31032  trlval2  31034  cdlemd6  31074  cdleme0nex  31161  cdleme18d  31166  cdleme25b  31225  cdleme25cv  31229  cdleme29b  31246  cdleme31fv  31261  cdleme31fv2  31264  cdlemefrs29bpre0  31267  cdlemefr32sn2aw  31275  cdlemefr29bpre0N  31277  cdlemefr29clN  31278  cdlemefr32fvaN  31280  cdlemefr32fva1  31281  cdlemefs32sn1aw  31285  cdleme32fva  31308  cdleme32fvaw  31310  cdleme40v  31340  cdleme42b  31349  cdleme46f2g2  31364  cdleme46f2g1  31365  cdleme48gfv  31408  cdlemg1fvawlemN  31444  cdlemg1cex  31459  cdlemg6d  31492  cdlemm10N  31990  dicffval  32046  dicfval  32047  dicval  32048  dicfnN  32055  dicvalrelN  32057  dihffval  32102  dihfval  32103  dihlsscpre  32106  dvh4dimat  32310  dvh3dimatN  32311  dvh4dimlem  32315  dvh3dim  32318  dvh4dimN  32319  dvh3dim2  32320  dvh3dim3N  32321  mapdcv  32532  mapdh9aOLDN  32663  hdmapfval  32702  hdmapval  32703  hdmapval2  32707  hdmap11lem2  32717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator