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  1852  drex1  1859  cbvex  1877  cbvexd  2052  ax11inda  2113  eujustALT  2117  2mo  2191  neeq1  2420  neeq2  2421  necon3abid  2445  neleq1  2503  neleq2  2504  cbvrexf  2704  gencbval  2770  cla4egf  2802  cla42gv  2808  cla43gv  2810  cdeqnot  2909  ru  2920  sbcng  2961  sbcrext  2994  sbcnel12g  3026  cbvrexcsf  3072  difjust  3080  eldif  3088  dfpss3  3183  difeq2  3205  disjne  3407  pssdifcom1  3445  pssdifcom2  3446  prel12  3689  disjxun  3918  nalset  4048  dtru  4095  dtruALT  4101  dtruALT2  4113  poeq1  4210  pocl  4214  swopo  4217  sotric  4233  sotrieq  4234  isso2i  4239  somo  4241  freq1  4256  frirr  4263  fr2nr  4264  frminex  4266  tz7.2  4270  wereu2  4283  nordeq  4304  ordtri1  4318  ordtri3  4321  rexxfrd  4440  rexxfr2d  4442  rexxfr  4445  elpwunsn  4459  fr3nr  4462  dfwe2  4464  ordsucsssuc  4505  nlimsucg  4524  orduninsuc  4525  dfom2  4549  ssnlim  4565  poinxp  4660  frinxp  4662  posn  4665  frsn  4667  rexiunxp  4733  rexxpf  4738  intirr  4968  poirr2  4974  cnvpo  5119  fvmpti  5453  fndmdif  5481  rexrnmpt  5522  f1imapss  5642  cbvexfo  5652  soisoi  5677  isopolem  5694  f1oweALT  5703  weniso  5704  rexrnmpt2  5811  ndmovg  5855  frxp  6077  poxp  6079  sorpssuni  6138  sorpssint  6139  canth  6178  pwnss  6183  riotaclbg  6230  smoword  6269  tz7.48lem  6339  abianfp  6357  oacan  6432  oaword  6433  omlimcl  6462  omeulem1  6466  nnaword  6511  nnmword  6517  nneob  6536  brdifun  6573  swoer  6574  undifixp  6738  boxcutc  6745  2dom  6818  php  6930  nndomo  6939  nnsdomo  6940  unxpdomlem2  6953  frfi  6987  unfilem1  7006  supmo  7087  eqsup  7091  supub  7094  supmaxlem  7099  suppr  7103  supisolem  7105  supisoex  7106  oieq1  7111  ordtypecbv  7116  ordtypelem7  7123  wemapso2lem  7149  canthwdom  7177  zfregcl  7192  elirrv  7195  elirr  7196  noinfep  7244  noinfepOLD  7245  cantnfp1lem3  7266  rankr1clem  7376  carden2b  7484  domtri2  7506  alephord3  7589  alephdom2  7598  alephval3  7621  dfac9  7646  kmlem2  7661  kmlem4  7663  isfin4  7807  isfin7  7811  fin23lem11  7827  isf32lem5  7867  isf34lem4  7887  fin1a2lem6  7915  fin1a2lem7  7916  fin1a2lem12  7921  itunisuc  7929  ac6n  7996  zorn2g  8014  zornn0g  8016  ttukeylem7  8026  axpowndlem2  8100  axpowndlem3  8101  axpowndlem4  8102  axregnd  8106  elgch  8124  engch  8130  fpwwe2lem13  8144  fpwwe2  8145  pwfseqlem1  8160  pwfseqlem3  8162  hargch  8179  addnidpi  8405  pinq  8431  nqereu  8433  ltsonq  8473  prlem934  8537  ltexprlem7  8546  addcanpr  8550  prlem936  8551  reclem2pr  8552  reclem3pr  8553  supexpr  8558  ltsosr  8596  supsrlem  8613  axpre-lttri  8667  axpre-sup  8671  xrlenlt  8770  axlttri  8774  axsup  8778  ltne  8797  readdcan  8866  leadd1  9122  ltsub1  9150  ltsub2  9151  leord1  9180  lediv1  9501  lemuldiv  9515  lerec  9518  le2msq  9536  lbinfm  9587  infm3  9593  suprnub  9597  infmrgelb  9614  infmrlb  9615  avgle1  9830  avgle2  9831  znnnlt1  9929  indstr  10166  zsupss  10186  uzsupss  10189  rpneg  10262  xralrple  10410  xleneg  10423  xltadd1  10454  xposdif  10460  xmulneg1  10467  xltmul1  10490  xrsupexmnf  10501  xrinfmexpnf  10502  xrsupsslem  10503  xrinfmsslem  10504  xrub  10508  supxrleub  10523  infmxrgelb  10531  difreicc  10645  leexp2  11034  hashbnd  11221  hasheni  11225  hashbc  11268  cnpart  11602  sqrlt  11624  limsuplt  11830  rlimrege0  11930  isercoll  12018  efle  12272  odd2np1  12461  divalglem7  12472  ndvdsadd  12481  bitsfval  12488  bitsval  12489  bits0  12493  bitsp1  12496  bitsmod  12501  bitscmp  12503  bitsinv1lem  12506  sadadd2lem2  12515  saddisjlem  12529  bitsshft  12540  gcdneg  12579  algcvgblem  12621  isprm3  12641  isprm5  12665  rpexp  12673  phiprmpw  12718  pythagtrip  12761  pcgcd1  12803  prmpwdvds  12825  prmreclem2  12838  prmreclem3  12839  prmreclem5  12841  prmreclem6  12842  vdwlem6  12907  vdwnnlem2  12917  vdwnnlem3  12918  vdwnn  12919  prmlem0  12981  prmlem1a  12982  divsfval  13323  cidpropd  13457  plttr  13948  sylow1lem3  14746  sylow2alem2  14764  efgsfo  14883  ablfac1eulem  15142  ablfac1eu  15143  pgpfac1lem1  15144  pgpfac1lem5  15149  islbs  15664  lbsind  15668  lbspss  15670  lbspropd  15687  lspsnne1  15705  islbs2  15741  lbsextlem1  15743  lbsextlem3  15745  lbsextlem4  15746  lbsextg  15747  nzrunit  15850  opsrtoslem2  16058  elcls  16642  maxlp  16710  perfi  16718  ordtbaslem  16750  ordtval  16751  ordtbas2  16753  ordtopn1  16756  ordtopn2  16757  ordtcnv  16763  ordtrest  16764  ordtrest2lem  16765  ordtrest2  16766  pnfnei  16782  mnfnei  16783  isreg2  16937  ordthauslem  16943  cmpfi  16967  cmpfii  16968  nconsubb  16981  hausdiag  17171  txkgen  17178  kqdisj  17255  ordthmeolem  17324  fbfinnfr  17368  trfbas  17371  fbunfip  17396  fbasrn  17411  trfil3  17415  ufileu  17446  fin1aufil  17459  hausflim  17508  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALTlem4  17576  ptcmplem2  17579  ptcmplem3  17580  stdbdbl  17895  iccntr  18158  reconnlem2  18164  iccpnfcnv  18274  xrhmeo  18276  lebnumlem1  18291  lebnumlem2  18292  lebnumlem3  18293  bcthlem4  18581  minveclem3b  18624  ivthlem2  18644  ivthlem3  18645  mbfmax  18836  mbfposr  18839  i1fd  18868  mbfi1fseqlem4  18905  itg2splitlem  18935  itg2monolem1  18937  itg2cnlem1  18948  dvne0  19190  lhop1lem  19192  deg1nn0clb  19308  dgrle  19457  coemulhi  19467  aaliou3lem9  19562  cos11  19727  logleb  19789  argrege0  19797  logdivle  19805  ellogdm  19818  isosctrlem1  19862  cxple  19910  cxplt2  19913  cxple3  19916  atandm  20004  atans2  20059  atantayl2  20066  ftalem7  20148  isppw2  20185  musum  20263  dchrsum2  20339  bposlem1  20355  lgsmod  20392  lgsdir2lem2  20395  lgsdir2  20399  lgsne0  20404  lgsquadlem1  20425  rpvmasumlem  20468  padicabv  20611  ostth3  20619  ostth  20620  lpni  20676  nmobndseqi  21187  minvecolem5  21290  chpsscon3  21912  chnle  21923  nonbooli  22078  pjnel  22153  specval  22308  nmcfnlbi  22462  stri  22667  hstri  22675  cvbr  22692  cvcon3  22694  chcv1  22765  cvexchlem  22778  chrelat2  22780  eldmgm  22865  erdszelem10  22902  eupath2lem3  23074  eupath2  23075  konigsberg  23082  untelirr  23225  untsucf  23227  untangtr  23231  dedekind  23252  inffz  23265  dfpo2  23282  dfon2lem3  23309  dfon2lem4  23310  dfon2lem7  23313  dfon2lem9  23315  distel  23328  predpoirr  23365  predfrirr  23366  soseq  23422  axdenselem4  23506  axdenselem5  23507  nocvxminlem  23512  axfelem14  23527  elfuns  23628  funpartfv  23657  dfrdg4  23662  axlowdimlem16  23759  axlowdim2  23762  axlowdim  23763  nabi1  24002  nabi2  24003  limsucncmpi  24058  limsucncmp  24059  ordcmp  24060  vxveqv  24219  inttpemp  24305  dstr  24337  nelioo5  24677  bwt2  24758  iintlem1  24776  tethpnc2  25237  pdiveql  25334  nn0prpwlem  25404  nn0prpw  25405  heibor1lem  25699  heiborlem1  25701  heiborlem6  25706  heiborlem8  25708  heiborlem10  25710  smprngopr  25843  ellz1  26012  rencldnfilem  26069  jm2.22  26254  jm2.23  26255  wepwsolem  26304  fnwe2lem2  26314  supeq123d  26324  aomclem8  26325  frlmlbs  26415  unxpwdom3  26422  islindf  26448  islinds2  26449  islindf2  26450  lindfind  26452  lindsind  26453  lindfrn  26457  lindfmm  26463  lsslindf  26466  islindf4  26474  psgnunilem1  26582  psgnunilem5  26583  psgnunilem2  26584  psgnunilem3  26585  rusbcALT  26806  xrltneNEW  26824  en3lpVD  27311  bnj23  27433  bnj1185  27515  bnj1476  27568  bnj1228  27730  bnj1388  27752  bnj1417  27760  ax12-4  27795  equsexv-x12  27802  a12study10  27825  a12study10n  27826  lcvfbr  27899  lcvbr  27900  lsatcv0  27910  l1cvpat  27933  opltcon3b  28083  cvrfval  28147  cvrval  28148  cvrnbtwn  28150  cvrval2  28153  cvrnbtwn2  28154  cvrnbtwn3  28155  cvrcon3b  28156  cvrnbtwn4  28158  atnlt  28192  iscvlat  28202  cvlexch1  28207  hlsuprexch  28259  hlrelat5N  28279  hlrelat2  28281  cvrval5  28293  3dimlem1  28336  3dim1lem5  28344  3dim2  28346  3dim3  28347  llnnlt  28401  islpln5  28413  lplni2  28415  lvolex3N  28416  lplnnle2at  28419  islpln2a  28426  lplnribN  28429  lplnexllnN  28442  lplnnlt  28443  lvoli3  28455  islvol5  28457  lvoli2  28459  lvolnle3at  28460  islvol2aN  28470  4atlem11  28487  lvolnltN  28496  dalawlem15  28763  4atexlemex2  28949  4atex  28954  4atex2-0aOLDN  28956  4atex2-0cOLDN  28958  lautcvr  28970  ltrnfset  28995  ltrnset  28996  ltrnu  28999  trlfset  29038  trlset  29039  trlval2  29041  cdlemd6  29081  cdleme0nex  29168  cdleme18d  29173  cdleme25b  29232  cdleme25cv  29236  cdleme29b  29253  cdleme31fv  29268  cdleme31fv2  29271  cdlemefrs29bpre0  29274  cdlemefr32sn2aw  29282  cdlemefr29bpre0N  29284  cdlemefr29clN  29285  cdlemefr32fvaN  29287  cdlemefr32fva1  29288  cdlemefs32sn1aw  29292  cdleme32fva  29315  cdleme32fvaw  29317  cdleme40v  29347  cdleme42b  29356  cdleme46f2g2  29371  cdleme46f2g1  29372  cdleme48gfv  29415  cdlemg1fvawlemN  29451  cdlemg1cex  29466  cdlemg6d  29499  cdlemm10N  29997  dicffval  30053  dicfval  30054  dicval  30055  dicfnN  30062  dicvalrelN  30064  dihffval  30109  dihfval  30110  dihlsscpre  30113  dvh4dimat  30317  dvh3dimatN  30318  dvh4dimlem  30322  dvh3dim  30325  dvh4dimN  30326  dvh3dim2  30327  dvh3dim3N  30328  mapdcv  30539  mapdh9aOLDN  30670  hdmapfval  30709  hdmapval  30710  hdmapval2  30714  hdmap11lem2  30724
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