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  1689  hba1w  1693  hbe1w  1694  ax10lem2  1890  ax9  1902  equsex  1915  drex1  1920  cbvex  1938  cbvexd  1962  ax11inda  2152  eujustALT  2159  2mo  2234  neeq1  2467  neeq2  2468  necon3abid  2492  neleq1  2550  neleq2  2551  cbvrexf  2772  gencbval  2845  spcegf  2877  spc2gv  2884  spc3gv  2886  cdeqnot  2992  ru  3003  sbcng  3044  sbcrext  3077  sbcnel12g  3111  cbvrexcsf  3157  difjust  3167  eldif  3175  dfpss3  3275  difeq2  3301  disjne  3513  pssdifcom1  3552  pssdifcom2  3553  prel12  3805  disjxun  4037  nalset  4167  pwnss  4192  dtru  4217  dtruALT  4223  dtruALT2  4235  poeq1  4333  pocl  4337  swopo  4340  sotric  4356  sotrieq  4357  isso2i  4362  somo  4364  freq1  4379  frirr  4386  fr2nr  4387  frminex  4389  tz7.2  4393  wereu2  4406  nordeq  4427  ordtri1  4441  ordtri3  4444  rexxfrd  4565  rexxfr2d  4567  rexxfr  4570  elpwunsn  4584  fr3nr  4587  dfwe2  4589  ordsucsssuc  4630  nlimsucg  4649  orduninsuc  4650  dfom2  4674  ssnlim  4690  poinxp  4769  frinxp  4771  posn  4774  frsn  4776  rexiunxp  4842  rexxpf  4847  intirr  5077  poirr2  5083  cnvpo  5229  fvmpti  5617  fndmdif  5645  rexrnmpt  5686  f1imapss  5806  cbvexfo  5816  soisoi  5841  isopolem  5858  f1oweALT  5867  weniso  5868  rexrnmpt2  5975  ndmovg  6019  frxp  6241  poxp  6243  sorpssuni  6302  sorpssint  6303  canth  6310  riotaclbg  6360  smoword  6399  tz7.48lem  6469  abianfp  6487  oacan  6562  oaword  6563  omlimcl  6592  omeulem1  6596  nnaword  6641  nnmword  6647  nneob  6666  brdifun  6703  swoer  6704  undifixp  6868  boxcutc  6875  2dom  6949  php  7061  nndomo  7070  nnsdomo  7071  unxpdomlem2  7084  frfi  7118  unfilem1  7137  supmo  7219  eqsup  7223  supub  7226  supmaxlem  7231  suppr  7235  supisolem  7237  supisoex  7238  oieq1  7243  ordtypecbv  7248  ordtypelem7  7255  wemapso2lem  7281  canthwdom  7309  zfregcl  7324  elirrv  7327  elirr  7328  noinfep  7376  noinfepOLD  7377  cantnfp1lem3  7398  rankr1clem  7508  carden2b  7616  domtri2  7638  alephord3  7721  alephdom2  7730  alephval3  7753  dfac9  7778  kmlem2  7793  kmlem4  7795  isfin4  7939  isfin7  7943  fin23lem11  7959  isf32lem5  7999  isf34lem4  8019  fin1a2lem6  8047  fin1a2lem7  8048  fin1a2lem12  8053  itunisuc  8061  ac6n  8128  zorn2g  8146  zornn0g  8148  ttukeylem7  8158  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axregnd  8242  elgch  8260  engch  8266  fpwwe2lem13  8280  fpwwe2  8281  pwfseqlem1  8296  pwfseqlem3  8298  hargch  8315  addnidpi  8541  pinq  8567  nqereu  8569  ltsonq  8609  prlem934  8673  ltexprlem7  8682  addcanpr  8686  prlem936  8687  reclem2pr  8688  reclem3pr  8689  supexpr  8694  ltsosr  8732  supsrlem  8749  axpre-lttri  8803  axpre-sup  8807  xrlenlt  8906  axlttri  8910  axsup  8914  ltne  8933  readdcan  9002  leadd1  9258  ltsub1  9286  ltsub2  9287  leord1  9316  lediv1  9637  lemuldiv  9651  lerec  9654  le2msq  9672  lbinfm  9723  infm3  9729  suprnub  9733  infmrgelb  9750  infmrlb  9751  avgle1  9967  avgle2  9968  znnnlt1  10066  indstr  10303  zsupss  10323  uzsupss  10326  rpneg  10399  xralrple  10548  xleneg  10561  xltadd1  10592  xposdif  10598  xmulneg1  10605  xltmul1  10628  xrsupexmnf  10639  xrinfmexpnf  10640  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrleub  10661  infmxrgelb  10669  difreicc  10783  leexp2  11172  hashbnd  11359  hasheni  11363  hashbc  11407  cnpart  11741  sqrlt  11763  limsuplt  11969  rlimrege0  12069  isercoll  12157  efle  12414  odd2np1  12603  divalglem7  12614  ndvdsadd  12623  bitsfval  12630  bitsval  12631  bits0  12635  bitsp1  12638  bitsmod  12643  bitscmp  12645  bitsinv1lem  12648  sadadd2lem2  12657  saddisjlem  12671  bitsshft  12682  gcdneg  12721  algcvgblem  12763  isprm3  12783  isprm5  12807  rpexp  12815  phiprmpw  12860  pythagtrip  12903  pcgcd1  12945  prmpwdvds  12967  prmreclem2  12980  prmreclem3  12981  prmreclem5  12983  prmreclem6  12984  vdwlem6  13049  vdwnnlem2  13059  vdwnnlem3  13060  vdwnn  13061  prmlem0  13123  prmlem1a  13124  divsfval  13465  mrisval  13548  ismri  13549  ismri2dad  13555  cidpropd  13629  plttr  14120  acsfiindd  14296  sylow1lem3  14927  sylow2alem2  14945  efgsfo  15064  ablfac1eulem  15323  ablfac1eu  15324  pgpfac1lem1  15325  pgpfac1lem5  15330  islbs  15845  lbsind  15849  lbspss  15851  lbspropd  15868  lspsnne1  15886  islbs2  15923  lbsacsbs  15925  lbsextlem1  15927  lbsextlem3  15929  lbsextlem4  15930  lbsextg  15931  nzrunit  16034  opsrtoslem2  16242  elcls  16826  maxlp  16894  perfi  16902  ordtbaslem  16934  ordtval  16935  ordtbas2  16937  ordtopn1  16940  ordtopn2  16941  ordtcnv  16947  ordtrest  16948  ordtrest2lem  16949  ordtrest2  16950  pnfnei  16966  mnfnei  16967  isreg2  17121  ordthauslem  17127  cmpfi  17151  cmpfii  17152  nconsubb  17165  hausdiag  17355  txkgen  17362  kqdisj  17439  ordthmeolem  17508  fbfinnfr  17552  trfbas  17555  fbunfip  17580  fbasrn  17595  trfil3  17599  ufileu  17630  fin1aufil  17643  hausflim  17692  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem2  17763  ptcmplem3  17764  stdbdbl  18079  iccntr  18342  reconnlem2  18348  iccpnfcnv  18458  xrhmeo  18460  lebnumlem1  18475  lebnumlem2  18476  lebnumlem3  18477  bcthlem4  18765  minveclem3b  18808  ivthlem2  18828  ivthlem3  18829  mbfmax  19020  mbfposr  19023  i1fd  19052  mbfi1fseqlem4  19089  itg2splitlem  19119  itg2monolem1  19121  itg2cnlem1  19132  dvne0  19374  lhop1lem  19376  deg1nn0clb  19492  dgrle  19641  coemulhi  19651  aaliou3lem9  19746  cos11  19911  logleb  19973  argrege0  19981  logdivle  19989  ellogdm  20002  cxple  20058  cxplt2  20061  cxple3  20064  isosctrlem1  20134  atandm  20188  atans2  20243  atantayl2  20250  ftalem7  20332  isppw2  20369  musum  20447  dchrsum2  20523  bposlem1  20539  lgsmod  20576  lgsdir2lem2  20579  lgsdir2  20583  lgsne0  20588  lgsquadlem1  20609  rpvmasumlem  20652  padicabv  20795  ostth3  20803  ostth  20804  lpni  20862  nmobndseqi  21373  minvecolem5  21476  chpsscon3  22098  chnle  22109  nonbooli  22246  pjnel  22321  specval  22494  nmcfnlbi  22648  stri  22853  hstri  22861  cvbr  22878  cvcon3  22880  chcv1  22951  cvexchlem  22964  chrelat2  22966  ifeqeqx  23050  ballotlemfc0  23067  ballotlemfcc  23068  ballotlem4  23073  ballotlemi1  23077  ballotlemii  23078  ballotlemimin  23080  ballotlem7  23110  ifbieq12d2  23165  elpreq  23204  isoun  23257  eliccelico  23285  elicoelioo  23286  xrge0iifcnv  23330  eldifpr  23409  eldiftp  23410  esumpcvgval  23461  eldmgm  23709  erdszelem10  23746  eupath2lem3  23918  eupath2  23919  konigsberg  23926  untelirr  24069  untsucf  24071  untangtr  24075  dedekind  24097  inffz  24110  dfpo2  24183  dfon2lem3  24212  dfon2lem4  24213  dfon2lem7  24216  dfon2lem9  24218  distel  24231  predpoirr  24268  predfrirr  24269  soseq  24325  nodenselem4  24409  nodenselem5  24410  nocvxminlem  24415  nofulllem4  24430  funpartfv  24555  dfrdg4  24560  axlowdimlem16  24657  axlowdim2  24660  axlowdim  24661  nabi1  24900  nabi2  24901  limsucncmpi  24956  limsucncmp  24957  ordcmp  24958  leceifl  24999  itg2addnclem  25003  itg2addnclem2  25004  itgaddnclem2  25010  iblabsnclem  25014  areacirc  25034  vxveqv  25157  inttpemp  25242  dstr  25274  nelioo5  25614  bwt2  25695  iintlem1  25713  tethpnc2  26174  pdiveql  26271  nn0prpwlem  26341  nn0prpw  26342  heibor1lem  26636  heiborlem1  26638  heiborlem6  26643  heiborlem8  26645  heiborlem10  26647  smprngopr  26780  ellz1  26949  rencldnfilem  27006  jm2.22  27191  jm2.23  27192  wepwsolem  27241  fnwe2lem2  27251  supeq123d  27261  aomclem8  27262  frlmlbs  27352  unxpwdom3  27359  islindf  27385  islinds2  27386  islindf2  27387  lindfind  27389  lindsind  27390  lindfrn  27394  lindfmm  27400  lsslindf  27403  islindf4  27411  psgnunilem1  27519  psgnunilem5  27520  psgnunilem2  27521  psgnunilem3  27522  rusbcALT  27742  xrltneNEW  27760  stoweidlem14  27866  stoweidlem34  27886  stoweidlem59  27911  eu2ndop1stv  28083  afvfv0bi  28120  afvco2  28144  ndmaovg  28152  elfznelfzo  28213  injresinjlem  28214  usgra1v  28260  nbusgra  28277  nbgra0nb  28278  spthispth  28359  wlkdvspthlem  28365  frgra2v  28423  en3lpVD  28937  bnj23  29060  bnj1185  29142  bnj1476  29195  bnj1228  29357  bnj1388  29379  bnj1417  29387  ax9NEW7  29445  equsexNEW7  29467  drex1NEW7  29471  cbvexwAUX7  29495  cbvexOLD7  29680  cbvexdOLD7  29689  ax12-4  29728  equsexv-x12  29735  a12study10  29758  a12study10n  29759  lcvfbr  29832  lcvbr  29833  lsatcv0  29843  l1cvpat  29866  opltcon3b  30016  cvrfval  30080  cvrval  30081  cvrnbtwn  30083  cvrval2  30086  cvrnbtwn2  30087  cvrnbtwn3  30088  cvrcon3b  30089  cvrnbtwn4  30091  atnlt  30125  iscvlat  30135  cvlexch1  30140  hlsuprexch  30192  hlrelat5N  30212  hlrelat2  30214  cvrval5  30226  3dimlem1  30269  3dim1lem5  30277  3dim2  30279  3dim3  30280  llnnlt  30334  islpln5  30346  lplni2  30348  lvolex3N  30349  lplnnle2at  30352  islpln2a  30359  lplnribN  30362  lplnexllnN  30375  lplnnlt  30376  lvoli3  30388  islvol5  30390  lvoli2  30392  lvolnle3at  30393  islvol2aN  30403  4atlem11  30420  lvolnltN  30429  dalawlem15  30696  4atexlemex2  30882  4atex  30887  4atex2-0aOLDN  30889  4atex2-0cOLDN  30891  lautcvr  30903  ltrnfset  30928  ltrnset  30929  ltrnu  30932  trlfset  30971  trlset  30972  trlval2  30974  cdlemd6  31014  cdleme0nex  31101  cdleme18d  31106  cdleme25b  31165  cdleme25cv  31169  cdleme29b  31186  cdleme31fv  31201  cdleme31fv2  31204  cdlemefrs29bpre0  31207  cdlemefr32sn2aw  31215  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdlemefs32sn1aw  31225  cdleme32fva  31248  cdleme32fvaw  31250  cdleme40v  31280  cdleme42b  31289  cdleme46f2g2  31304  cdleme46f2g1  31305  cdleme48gfv  31348  cdlemg1fvawlemN  31384  cdlemg1cex  31399  cdlemg6d  31432  cdlemm10N  31930  dicffval  31986  dicfval  31987  dicval  31988  dicfnN  31995  dicvalrelN  31997  dihffval  32042  dihfval  32043  dihlsscpre  32046  dvh4dimat  32250  dvh3dimatN  32251  dvh4dimlem  32255  dvh3dim  32258  dvh4dimN  32259  dvh3dim2  32260  dvh3dim3N  32261  mapdcv  32472  mapdh9aOLDN  32603  hdmapfval  32642  hdmapval  32643  hdmapval2  32647  hdmap11lem2  32657
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