MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notbid Unicode version

Theorem notbid 286
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 283 . . 3  |-  ( ps  <->  -. 
-.  ps )
3 notnot 283 . . 3  |-  ( ch  <->  -. 
-.  ch )
41, 2, 33bitr3g 279 . 2  |-  ( ph  ->  ( -.  -.  ps  <->  -. 
-.  ch ) )
54con4bid 285 1  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  notbi  287  con3th  925  nanbi1  1304  xorbi12d  1324  cbvexvw  1717  hba1w  1722  hbe1w  1723  cbvex  1983  cbvexd  1988  equsexOLD  2003  ax10lem2OLD  2026  ax9OLD  2033  drex1  2055  ax11inda  2276  eujustALT  2283  2mo  2358  neeq1  2601  neeq2  2602  necon3abid  2626  neleq1  2686  neleq2  2687  cbvrexf  2914  gencbval  2987  spcegf  3019  spc2gv  3026  spc3gv  3028  cdeqnot  3136  ru  3147  sbcng  3188  sbcrext  3221  sbcnel12g  3255  cbvrexcsf  3299  difjust  3309  eldif  3317  dfpss3  3420  difeq2  3446  disjne  3660  pssdifcom1  3700  pssdifcom2  3701  prel12  3962  disjxun  4197  nalset  4327  pwnss  4352  dtru  4377  dtruALT  4383  dtruALT2  4395  poeq1  4493  pocl  4497  swopo  4500  sotric  4516  sotrieq  4517  isso2i  4522  somo  4524  freq1  4539  frirr  4546  fr2nr  4547  frminex  4549  tz7.2  4553  wereu2  4566  nordeq  4587  ordtri1  4601  ordtri3  4604  rexxfrd  4724  rexxfr2d  4726  rexxfr  4729  elpwunsn  4743  fr3nr  4746  dfwe2  4748  ordsucsssuc  4789  nlimsucg  4808  orduninsuc  4809  dfom2  4833  ssnlim  4849  poinxp  4927  frinxp  4929  posn  4932  frsn  4934  rexiunxp  5001  rexxpf  5006  intirr  5238  poirr2  5244  cnvpo  5396  fvmpti  5791  fndmdif  5820  rexrnmpt  5865  f1imapss  5998  cbvexfo  6009  soisoi  6034  isopolem  6051  f1oweALT  6060  weniso  6061  rexrnmpt2  6171  ndmovg  6216  frxp  6442  poxp  6444  sorpssuni  6517  sorpssint  6518  canth  6525  riotaclbg  6575  smoword  6614  tz7.48lem  6684  abianfp  6702  oacan  6777  oaword  6778  omlimcl  6807  omeulem1  6811  nnaword  6856  nnmword  6862  nneob  6881  brdifun  6918  swoer  6919  undifixp  7084  boxcutc  7091  2dom  7165  php  7277  nndomo  7286  nnsdomo  7287  unxpdomlem2  7300  frfi  7338  unfilem1  7357  supmo  7441  eqsup  7445  supub  7448  supmaxlem  7453  suppr  7457  supisolem  7459  supisoex  7460  oieq1  7465  ordtypecbv  7470  ordtypelem7  7477  wemapso2lem  7503  canthwdom  7531  zfregcl  7546  elirrv  7549  elirr  7550  noinfep  7598  noinfepOLD  7599  cantnfp1lem3  7620  rankr1clem  7730  carden2b  7838  domtri2  7860  alephord3  7943  alephdom2  7952  alephval3  7975  dfac9  8000  kmlem2  8015  kmlem4  8017  isfin4  8161  isfin7  8165  fin23lem11  8181  isf32lem5  8221  isf34lem4  8241  fin1a2lem6  8269  fin1a2lem7  8270  fin1a2lem12  8275  itunisuc  8283  ac6n  8349  zorn2g  8367  zornn0g  8369  ttukeylem7  8379  axpowndlem2  8457  axpowndlem3  8458  axpowndlem4  8459  axregnd  8463  elgch  8481  engch  8487  fpwwe2lem13  8501  fpwwe2  8502  pwfseqlem1  8517  pwfseqlem3  8519  hargch  8536  addnidpi  8762  pinq  8788  nqereu  8790  ltsonq  8830  prlem934  8894  ltexprlem7  8903  addcanpr  8907  prlem936  8908  reclem2pr  8909  reclem3pr  8910  supexpr  8915  ltsosr  8953  supsrlem  8970  axpre-lttri  9024  axpre-sup  9028  xrlenlt  9127  axlttri  9131  axsup  9135  ltne  9154  readdcan  9224  leadd1  9480  ltsub1  9508  ltsub2  9509  leord1  9538  lediv1  9859  lemuldiv  9873  lerec  9876  le2msq  9894  lbinfm  9945  infm3  9951  suprnub  9955  infmrgelb  9972  infmrlb  9973  avgle1  10191  avgle2  10192  znnnlt1  10292  indstr  10529  zsupss  10549  uzsupss  10552  rpneg  10625  xralrple  10775  xleneg  10788  xltadd1  10819  xposdif  10825  xmulneg1  10832  xltmul1  10855  xrsupexmnf  10867  xrinfmexpnf  10868  xrsupsslem  10869  xrinfmsslem  10870  xrub  10874  supxrleub  10889  infmxrgelb  10897  difreicc  11012  elfznelfzo  11175  injresinjlem  11182  leexp2  11417  hashbnd  11607  hasheni  11615  hashbc  11685  cnpart  12028  sqrlt  12050  limsuplt  12256  rlimrege0  12356  isercoll  12444  efle  12702  odd2np1  12891  divalglem7  12902  ndvdsadd  12911  bitsfval  12918  bitsval  12919  bits0  12923  bitsp1  12926  bitsmod  12931  bitscmp  12933  bitsinv1lem  12936  sadadd2lem2  12945  saddisjlem  12959  bitsshft  12970  gcdneg  13009  algcvgblem  13051  isprm3  13071  isprm5  13095  rpexp  13103  phiprmpw  13148  pythagtrip  13191  pcgcd1  13233  prmpwdvds  13255  prmreclem2  13268  prmreclem3  13269  prmreclem5  13271  prmreclem6  13272  vdwlem6  13337  vdwnnlem2  13347  vdwnnlem3  13348  vdwnn  13349  prmlem0  13411  prmlem1a  13412  divsfval  13755  mrisval  13838  ismri  13839  ismri2dad  13845  cidpropd  13919  plttr  14410  acsfiindd  14586  sylow1lem3  15217  sylow2alem2  15235  efgsfo  15354  ablfac1eulem  15613  ablfac1eu  15614  pgpfac1lem1  15615  pgpfac1lem5  15620  islbs  16131  lbsind  16135  lbspss  16137  lbspropd  16154  lspsnne1  16172  islbs2  16209  lbsacsbs  16211  lbsextlem1  16213  lbsextlem3  16215  lbsextlem4  16216  lbsextg  16217  nzrunit  16320  opsrtoslem2  16528  elcls  17120  maxlp  17194  perfi  17202  ordtbaslem  17235  ordtval  17236  ordtbas2  17238  ordtopn1  17241  ordtopn2  17242  ordtcnv  17248  ordtrest  17249  ordtrest2lem  17250  ordtrest2  17251  pnfnei  17267  mnfnei  17268  isreg2  17424  ordthauslem  17430  cmpfi  17454  cmpfii  17455  bwth  17456  nconsubb  17469  hausdiag  17660  txkgen  17667  kqdisj  17747  ordthmeolem  17816  fbfinnfr  17856  trfbas  17859  fbunfip  17884  fbasrn  17899  trfil3  17903  ufileu  17934  fin1aufil  17947  hausflim  17996  alexsubALTlem2  18062  alexsubALTlem3  18063  alexsubALTlem4  18064  ptcmplem2  18067  ptcmplem3  18068  stdbdbl  18530  iccntr  18835  reconnlem2  18841  iccpnfcnv  18952  xrhmeo  18954  lebnumlem1  18969  lebnumlem2  18970  lebnumlem3  18971  bcthlem4  19263  minveclem3b  19312  ivthlem2  19332  ivthlem3  19333  mbfmax  19524  mbfposr  19527  i1fd  19556  mbfi1fseqlem4  19593  itg2splitlem  19623  itg2monolem1  19625  itg2cnlem1  19636  dvne0  19878  lhop1lem  19880  deg1nn0clb  19996  dgrle  20145  coemulhi  20155  aaliou3lem9  20250  cos11  20418  logleb  20481  argrege0  20489  logdivle  20500  ellogdm  20513  cxple  20569  cxplt2  20572  cxple3  20575  isosctrlem1  20645  atandm  20699  atans2  20754  atantayl2  20761  ftalem7  20844  isppw2  20881  musum  20959  dchrsum2  21035  bposlem1  21051  lgsmod  21088  lgsdir2lem2  21091  lgsdir2  21095  lgsne0  21100  lgsquadlem1  21121  rpvmasumlem  21164  padicabv  21307  ostth3  21315  ostth  21316  usgra1v  21392  usgraidx2v  21395  nbgra0nb  21424  cusgrafilem3  21473  spthispth  21556  wlkdvspthlem  21590  eupath2lem3  21684  eupath2  21685  konigsberg  21692  lpni  21750  nmobndseqi  22263  minvecolem5  22366  chpsscon3  22988  chnle  22999  nonbooli  23136  pjnel  23211  specval  23384  nmcfnlbi  23538  stri  23743  hstri  23751  cvbr  23768  cvcon3  23770  chcv1  23841  cvexchlem  23854  chrelat2  23856  elpreq  23982  ifeqeqx  23984  ifbieq12d2  23985  isoun  24072  eliccelico  24123  elicoelioo  24124  toslub  24174  tosglb  24175  isarchi2  24238  xrge0iifcnv  24302  elzdif0  24347  eldifpr  24375  eldiftp  24376  esumpcvgval  24451  ballotlemfc0  24733  ballotlemfcc  24734  ballotlem4  24739  ballotlemimin  24746  ballotlem7  24776  eldmgm  24789  erdszelem10  24869  untelirr  25140  untsucf  25142  untangtr  25146  dedekind  25170  inffz  25183  dfpo2  25362  dfon2lem3  25391  dfon2lem4  25392  dfon2lem7  25395  dfon2lem9  25397  distel  25410  predpoirr  25447  predfrirr  25448  soseq  25504  nodenselem4  25588  nodenselem5  25589  nocvxminlem  25594  nofulllem4  25609  funpartfv  25735  dfrdg4  25740  axlowdimlem16  25839  axlowdim2  25842  axlowdim  25843  limsucncmpi  26138  limsucncmp  26139  ordcmp  26140  leceifl  26183  mblfinlem  26185  mblfinlem2  26186  ismblfin  26188  cnambfre  26196  itg2addnclem  26197  itg2addnclem2  26198  iblabsnclem  26209  areacirc  26229  nn0prpwlem  26257  nn0prpw  26258  heibor1lem  26450  heiborlem1  26452  heiborlem6  26457  heiborlem8  26459  heiborlem10  26461  smprngopr  26594  ellz1  26757  rencldnfilem  26813  jm2.22  26998  jm2.23  26999  wepwsolem  27048  fnwe2lem2  27058  supeq123d  27068  aomclem8  27069  frlmlbs  27159  unxpwdom3  27166  islindf  27192  islinds2  27193  islindf2  27194  lindfind  27196  lindsind  27197  lindfrn  27201  lindfmm  27207  lsslindf  27210  islindf4  27218  psgnunilem1  27326  psgnunilem5  27327  psgnunilem2  27328  psgnunilem3  27329  rusbcALT  27549  xrltneNEW  27566  stoweidlem14  27672  stoweidlem34  27692  stoweidlem59  27717  eu2ndop1stv  27889  afvfv0bi  27925  afvco2  27949  ndmaovg  27957  otiunsndisj  27996  otiunsndisjX  27997  2f1fvneq  28000  swrdnd  28043  swrdccat3  28071  swrdccat3b  28073  frgra2v  28145  frgrancvvdeqlem2  28176  2spotiundisj  28207  usg2spot2nb  28210  2spotmdisj  28213  en3lpVD  28709  bnj23  28835  bnj1185  28917  bnj1476  28970  bnj1228  29132  bnj1388  29154  bnj1417  29162  ax9NEW7  29220  equsexNEW7  29242  drex1NEW7  29246  cbvexwAUX7  29270  cbvexOLD7  29456  cbvexdOLD7  29465  lcvfbr  29549  lcvbr  29550  lsatcv0  29560  l1cvpat  29583  opltcon3b  29733  cvrfval  29797  cvrval  29798  cvrnbtwn  29800  cvrval2  29803  cvrnbtwn2  29804  cvrnbtwn3  29805  cvrcon3b  29806  cvrnbtwn4  29808  atnlt  29842  iscvlat  29852  cvlexch1  29857  hlsuprexch  29909  hlrelat5N  29929  hlrelat2  29931  cvrval5  29943  3dimlem1  29986  3dim1lem5  29994  3dim2  29996  3dim3  29997  llnnlt  30051  islpln5  30063  lplni2  30065  lvolex3N  30066  lplnnle2at  30069  islpln2a  30076  lplnribN  30079  lplnexllnN  30092  lplnnlt  30093  lvoli3  30105  islvol5  30107  lvoli2  30109  lvolnle3at  30110  islvol2aN  30120  4atlem11  30137  lvolnltN  30146  dalawlem15  30413  4atexlemex2  30599  4atex  30604  4atex2-0aOLDN  30606  4atex2-0cOLDN  30608  lautcvr  30620  ltrnfset  30645  ltrnset  30646  ltrnu  30649  trlfset  30688  trlset  30689  trlval2  30691  cdlemd6  30731  cdleme0nex  30818  cdleme18d  30823  cdleme25b  30882  cdleme25cv  30886  cdleme29b  30903  cdleme31fv  30918  cdleme31fv2  30921  cdlemefrs29bpre0  30924  cdlemefr32sn2aw  30932  cdlemefr29bpre0N  30934  cdlemefr29clN  30935  cdlemefr32fvaN  30937  cdlemefr32fva1  30938  cdlemefs32sn1aw  30942  cdleme32fva  30965  cdleme32fvaw  30967  cdleme40v  30997  cdleme42b  31006  cdleme46f2g2  31021  cdleme46f2g1  31022  cdleme48gfv  31065  cdlemg1fvawlemN  31101  cdlemg1cex  31116  cdlemg6d  31149  cdlemm10N  31647  dicffval  31703  dicfval  31704  dicval  31705  dicfnN  31712  dicvalrelN  31714  dihffval  31759  dihfval  31760  dihlsscpre  31763  dvh4dimat  31967  dvh3dimatN  31968  dvh4dimlem  31972  dvh3dim  31975  dvh4dimN  31976  dvh3dim2  31977  dvh3dim3N  31978  mapdcv  32189  mapdh9aOLDN  32320  hdmapfval  32359  hdmapval  32360  hdmapval2  32364  hdmap11lem2  32374
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 178
  Copyright terms: Public domain W3C validator