Theorem notbid 308

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

Step	Hyp	Ref	Expression
1		notbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		notnotb 304	. . 3 |- ( ps <-> -. -. ps )
3		notnotb 304	. . 3 |- ( ch <-> -. -. ch )
4	1, 2, 3	3bitr3g 302	. 2 |- ( ph -> ( -. -. ps <-> -. -. ch ) )
5	4	con4bid 307	1 |- ( ph -> ( -. ps <-> -. ch ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  notbi  309  ifpbi123d  1027  con3ALT  1032  con3OLD  1035  nanbi1  1455  xorbi12d  1478  cbvexvw  1970  hba1wOLD  1975  hbe1w  1976  cbvexv1  2176  cbvex  2272  cbvexv  2275  cbvexd  2278  cbvex2  2280  cbvexdva  2283  drex1  2327  eujustALT  2473  necon3abid  2830  neleq12d  2901  cbvrexf  3166  gencbval  3252  spcegf  3289  spc2gv  3296  spc3gv  3298  cdeqnot  3423  ru  3434  sbcng  3476  sbcrext  3511  sbcrextOLD  3512  cbvrexcsf  3566  difjust  3576  eldif  3584  dfpss3  3693  difeq2  3722  disjne  4022  pssdifcom1  4054  eldifpr  4204  elpwunsn  4224  eldiftp  4228  prel12  4383  prel12g  4387  disjxun  4651  nalset  4795  pwnss  4830  dtru  4857  rexxfrd  4881  rexxfr2d  4883  rexxfrd2  4885  rexxfr  4888  dtruALT  4899  dtruALT2  4911  opthneg  4950  otiunsndisj  4980  poeq1  5038  pocl  5042  swopo  5045  sotric  5061  sotrieq  5062  isso2i  5067  somo  5069  freq1  5084  frirr  5091  fr2nr  5092  frminex  5094  tz7.2  5098  wereu2  5111  poinxp  5182  frinxp  5184  posn  5187  frsn  5189  rexiunxp  5262  rexxpf  5269  intirr  5514  poirr2  5520  cnvpo  5673  predpoirr  5708  predfrirr  5709  nordeq  5742  ordtri1  5756  ordtri3  5759  ordtri3OLD  5760  fvmpti  6281  fndmdif  6321  rexrnmpt  6369  2f1fvneq  6517  f1imapss  6523  cbvexfo  6545  soisoi  6578  isopolem  6595  weniso  6604  canth  6608  riotaclb  6649  rexrnmpt2  6776  ndmovg  6817  sorpssuni  6946  sorpssint  6947  fr3nr  6979  dfwe2  6981  ordsucsssuc  7023  nlimsucg  7042  orduninsuc  7043  dfom2  7067  ssnlim  7083  f1oweALT  7152  frxp  7287  poxp  7289  wfrlem10  7424  smoword  7463  tz7.48lem  7536  oacan  7628  oaword  7629  omlimcl  7658  omeulem1  7662  nnaword  7707  nnmword  7713  nneob  7732  brdifun  7771  swoer  7772  undifixp  7944  boxcutc  7951  2dom  8029  php  8144  nndomo  8154  nnsdomo  8155  unxpdomlem2  8165  frfi  8205  unfilem1  8224  supeq3  8355  supeq123d  8356  supmo  8358  eqsup  8362  supub  8365  sup0  8372  suppr  8377  supisolem  8379  supisoex  8380  eqinf  8390  infval  8392  infmo  8401  infpr  8409  infempty  8412  oieq1  8417  ordtypecbv  8422  ordtypelem7  8429  wemapsolem  8455  canthwdom  8484  zfregcl  8499  zfregclOLD  8501  elirrv  8504  elirr  8505  noinfep  8557  cantnfp1lem3  8577  rankr1clem  8683  carden2b  8793  domtri2  8815  alephord3  8901  alephdom2  8910  alephval3  8933  dfac9  8958  kmlem2  8973  kmlem4  8975  isfin4  9119  isfin7  9123  fin23lem11  9139  isf32lem5  9179  isf34lem4  9199  fin1a2lem6  9227  fin1a2lem7  9228  fin1a2lem12  9233  itunisuc  9241  ac6n  9307  zorn2g  9325  zornn0g  9327  ttukeylem7  9337  axpowndlem3  9421  axpowndlem4  9422  axregnd  9426  elgch  9444  engch  9450  fpwwe2lem13  9464  fpwwe2  9465  pwfseqlem1  9480  pwfseqlem3  9482  hargch  9495  addnidpi  9723  pinq  9749  nqereu  9751  ltsonq  9791  prlem934  9855  ltexprlem7  9864  addcanpr  9868  prlem936  9869  reclem2pr  9870  reclem3pr  9871  supexpr  9876  ltsosr  9915  supsrlem  9932  axpre-lttri  9986  axpre-sup  9990  xrlenlt  10103  axlttri  10109  axsup  10113  ltne  10134  dedekind  10200  readdcan  10210  leadd1  10496  ltsub1  10524  ltsub2  10525  leord1  10555  lediv1  10888  lemuldiv  10903  lerec  10906  le2msq  10923  infm3  10982  suprnub  10988  infregelb  11007  avgle1  11272  avgle2  11273  znnnlt1  11404  indstr  11756  zsupss  11777  uzsupss  11780  rpneg  11863  xralrple  12036  xleneg  12049  xltadd1  12086  xposdif  12092  xmulneg1  12099  xltmul1  12122  xrsupexmnf  12135  xrinfmexpnf  12136  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxrleub  12156  infxrgelb  12165  difreicc  12304  nn0disj  12455  nelfzo  12475  elfznelfzo  12573  fvinim0ffz  12587  injresinjlem  12588  ssnn0fi  12784  leexp2  12915  hashbnd  13123  hasheni  13136  hashbc  13237  wrdsymb0  13339  swrdnd  13432  swrdnd2  13433  repswswrd  13531  repswccat  13532  cshwidxmod  13549  cnpart  13980  sqrtlt  14002  limsuplt  14210  rlimrege0  14310  isercoll  14398  efle  14848  odd2np1  15065  sumodd  15111  divalglem7  15122  ndvdsadd  15134  fldivndvdslt  15138  bitsfval  15145  bitsval  15146  bits0  15150  bitsp1  15153  bitsmod  15158  bitscmp  15160  bitsinv1lem  15163  sadadd2lem2  15172  saddisjlem  15186  bitsshft  15197  gcdneg  15243  algcvgblem  15290  lcmneg  15316  isprm3  15396  dvdsnprmd  15403  isprm5  15419  rpexp  15432  phiprmpw  15481  m1dvdsndvds  15503  pythagtrip  15539  pcgcd1  15581  prmpwdvds  15608  prmreclem2  15621  prmreclem3  15622  prmreclem5  15624  prmreclem6  15625  vdwlem6  15690  vdwnnlem2  15700  vdwnnlem3  15701  vdwnn  15702  prmo1  15741  prmlem0  15812  prmlem1a  15813  divsfval  16207  mrisval  16290  ismri  16291  ismri2dad  16297  cidpropd  16370  plttr  16970  joinval  17005  meetval  17019  acsfiindd  17177  isnsgrp  17288  mgm2nsgrplem2  17406  sgrp2nmndlem3  17412  symgfix2  17836  pmtrdifellem4  17899  psgnunilem1  17913  psgnunilem5  17914  psgnunilem2  17915  psgnunilem3  17916  pmtrsn  17939  sylow1lem3  18015  sylow2alem2  18033  efgsfo  18152  ablfac1eulem  18471  ablfac1eu  18472  pgpfac1lem1  18473  pgpfac1lem5  18478  islbs  19076  lbsind  19080  lbspss  19082  lbspropd  19099  lspsnne1  19117  islbs2  19154  lbsacsbs  19156  lbsextlem1  19158  lbsextlem3  19160  lbsextlem4  19161  lbsextg  19162  nzrunit  19267  opsrtoslem2  19485  cply1coe0  19669  cply1coe0bi  19670  frlmlbs  20136  islindf  20151  islinds2  20152  islindf2  20153  lindfind  20155  lindsind  20156  lindfrn  20160  lindfmm  20166  lsslindf  20169  islindf4  20177  mdetunilem7  20424  mdetunilem8  20425  mdetunilem9  20426  maducoeval2  20446  pmatcollpw3fi1lem1  20591  fvmptnn04ifa  20655  fvmptnn04ifc  20657  fvmptnn04ifd  20658  chfacffsupp  20661  chfacfscmul0  20663  chfacfpmmul0  20667  elcls  20877  maxlp  20951  perfi  20959  ordtbaslem  20992  ordtval  20993  ordtbas2  20995  ordtopn1  20998  ordtopn2  20999  ordtcnv  21005  ordtrest  21006  ordtrest2lem  21007  ordtrest2  21008  pnfnei  21024  mnfnei  21025  isreg2  21181  ordthauslem  21187  cmpfi  21211  cmpfii  21212  bwth  21213  nconnsubb  21226  hausdiag  21448  txkgen  21455  kqdisj  21535  ordthmeolem  21604  fbfinnfr  21645  trfbas  21648  fbunfip  21673  fbasrn  21688  trfil3  21692  ufileu  21723  fin1aufil  21736  hausflim  21785  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem2  21857  ptcmplem3  21858  stdbdbl  22322  iccntr  22624  reconnlem2  22630  iccpnfcnv  22743  xrhmeo  22745  lebnumlem1  22760  lebnumlem2  22761  lebnumlem3  22762  bcthlem4  23124  minveclem3b  23199  ivthlem2  23221  ivthlem3  23222  mbfmax  23416  mbfposr  23419  i1fd  23448  mbfi1fseqlem4  23485  itg2splitlem  23515  itg2monolem1  23517  itg2cnlem1  23528  dvne0  23774  lhop1lem  23776  deg1nn0clb  23850  dgrle  23999  coemulhi  24010  aaliou3lem9  24105  cos11  24279  logleb  24349  argrege0  24357  logdivle  24368  ellogdm  24385  cxple  24441  cxplt2  24444  cxple3  24447  isosctrlem1  24548  atandm  24603  atans2  24658  atantayl2  24665  eldmgm  24748  ftalem7  24805  isppw2  24841  musum  24917  dchrsum2  24993  bposlem1  25009  lgsmod  25048  lgsdir2lem2  25051  lgsdir2  25055  lgsne0  25060  lgsprme0  25064  gausslemma2dlem4  25094  lgsquadlem1  25105  2lgslem3  25129  2lgsoddprm  25141  rpvmasumlem  25176  padicabv  25319  ostth3  25327  ostth  25328  istrkgld  25358  axtgupdim2  25370  tglowdim2l  25545  axlowdimlem16  25837  axlowdim2  25840  axlowdim  25841  numedglnl  26039  usgredg2v  26119  lfuhgr1v0e  26146  cusgrfi  26354  vtxd0nedgb  26384  vtxduhgr0edgnel  26390  1loopgrnb0  26398  1hevtxdg0  26401  vtxdgoddnumeven  26449  wlkp1lem1  26570  wlkp1lem2  26571  wlkp1lem5  26574  crctcsh  26716  clwwlknclwwlkdifs  26873  clwlkclwwlklem2a4  26898  eupth2eucrct  27077  eupth2lem3lem3  27090  eupth2lem3lem4  27091  eupth2lem3lem6  27093  eupth2lem3lem7  27094  eupth2lems  27098  eupth2  27099  konigsberglem4  27117  nfrgr2v  27136  frgrwopreglem3  27178  fusgr2wsp2nb  27198  frgrreggt1  27251  friendshipgt3  27256  lpni  27332  nmobndseqi  27634  minvecolem5  27737  chpsscon3  28362  chnle  28373  nonbooli  28510  pjnel  28585  specval  28757  nmcfnlbi  28911  stri  29116  hstri  29124  cvbr  29141  cvcon3  29143  chcv1  29214  cvexchlem  29227  chrelat2  29229  spc2d  29313  elpreq  29360  ifeqeqx  29361  isoun  29479  suppss3  29502  xrge0infss  29525  infxrge0gelb  29531  eliccelico  29539  elicoelioo  29540  nndiffz1  29548  nn0min  29567  toslublem  29667  tosglblem  29669  isarchi2  29739  archiabl  29752  ordtcnvNEW  29966  ordtrestNEW  29967  ordtrest2NEWlem  29968  ordtrest2NEW  29969  ordtconnlem1  29970  xrge0iifcnv  29979  elzdif0  30024  esumpcvgval  30140  esum2d  30155  ddemeas  30299  omssubadd  30362  oddpwdc  30416  eulerpartlems  30422  eulerpartlemf  30432  eulerpartlemt  30433  eulerpartlemr  30436  eulerpartlemgvv  30438  eulerpartlemn  30443  ballotlemfc0  30554  ballotlemfcc  30555  ballotlem4  30560  ballotlemimin  30567  ballotlem7  30597  plymulx  30625  signsply0  30628  reprinfz1  30700  reprpmtf1o  30704  reprdifc  30705  hgt750lema  30735  hgt750leme  30736  istrkg2d  30744  bnj23  30784  bnj1185  30864  bnj1228  31079  bnj1388  31101  bnj1417  31109  erdszelem10  31182  ismfs  31446  mvtinf  31452  untelirr  31585  untsucf  31587  untangtr  31591  ceqsralv2  31607  inffzOLD  31615  dfpo2  31645  dfon2lem3  31690  dfon2lem4  31691  dfon2lem7  31694  dfon2lem9  31696  distel  31709  soseq  31751  noextenddif  31821  nodenselem4  31837  nodenselem5  31838  nodenselem7  31840  nolt02o  31845  noresle  31846  noprefixmo  31848  nosupdm  31850  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd1  31860  nosupbnd2lem1  31861  nosupbnd2  31862  slenlt  31877  nocvxminlem  31893  slerec  31923  funpartfv  32052  dfrdg4  32058  nn0prpwlem  32317  nn0prpw  32318  limsucncmpi  32444  limsucncmp  32445  ordcmp  32446  unblimceq0  32498  unbdqndv1  32499  bj-hbntbi  32695  bj-cbvexdv  32736  bj-cbvex2v  32738  bj-drex1v  32749  bj-nalset  32794  bj-dtru  32797  bj-ru0  32932  bj-nuliota  33019  topdifinffinlem  33195  topdifinffin  33196  icorempt2  33199  relowlpssretop  33212  finxpreclem2  33227  finxpreclem6  33233  wl-ax11-lem8  33369  leceifl  33398  lindsenlbs  33404  matunitlindflem1  33405  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem21  33430  poimirlem23  33432  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem31  33440  poimir  33442  mblfinlem2  33447  mblfinlem3  33448  ismblfin  33450  cnambfre  33458  itg2addnclem  33461  itg2addnclem2  33462  iblabsnclem  33473  ftc1anclem1  33485  areacirc  33505  heibor1lem  33608  heiborlem1  33610  heiborlem6  33615  heiborlem8  33617  heiborlem10  33619  smprngopr  33851  ecin0  34117  ax12inda  34233  riotaclbgBAD  34240  lcvfbr  34307  lcvbr  34308  lsatcv0  34318  l1cvpat  34341  opltcon3b  34491  cvrfval  34555  cvrval  34556  cvrnbtwn  34558  cvrval2  34561  cvrnbtwn2  34562  cvrnbtwn3  34563  cvrcon3b  34564  cvrnbtwn4  34566  atnlt  34600  iscvlat  34610  cvlexch1  34615  hlsuprexch  34667  hlrelat5N  34687  hlrelat2  34689  cvrval5  34701  3dimlem1  34744  3dim1lem5  34752  3dim2  34754  3dim3  34755  llnnlt  34809  islpln5  34821  lplni2  34823  lvolex3N  34824  lplnnle2at  34827  islpln2a  34834  lplnribN  34837  lplnexllnN  34850  lplnnlt  34851  lvoli3  34863  islvol5  34865  lvoli2  34867  lvolnle3at  34868  islvol2aN  34878  4atlem11  34895  lvolnltN  34904  dalawlem15  35171  4atexlemex2  35357  4atex  35362  4atex2-0aOLDN  35364  4atex2-0cOLDN  35366  lautcvr  35378  ltrnfset  35403  ltrnset  35404  ltrnu  35407  trlfset  35447  trlset  35448  trlval2  35450  cdlemd6  35490  cdleme0nex  35577  cdleme18d  35582  cdleme25b  35642  cdleme25cv  35646  cdleme29b  35663  cdleme31fv  35678  cdleme31fv2  35681  cdlemefrs29bpre0  35684  cdlemefr32sn2aw  35692  cdlemefr29bpre0N  35694  cdlemefr29clN  35695  cdlemefr32fvaN  35697  cdlemefr32fva1  35698  cdlemefs32sn1aw  35702  cdleme32fva  35725  cdleme32fvaw  35727  cdleme40v  35757  cdleme42b  35766  cdleme46f2g2  35781  cdleme46f2g1  35782  cdleme48gfv  35825  cdlemg1fvawlemN  35861  cdlemg1cex  35876  cdlemg6d  35909  cdlemm10N  36407  dicffval  36463  dicfval  36464  dicval  36465  dicfnN  36472  dicvalrelN  36474  dihffval  36519  dihfval  36520  dihlsscpre  36523  dvh4dimat  36727  dvh3dimatN  36728  dvh4dimlem  36732  dvh3dim  36735  dvh4dimN  36736  dvh3dim2  36737  dvh3dim3N  36738  mapdcv  36949  mapdh9aOLDN  37080  hdmapfval  37119  hdmapval  37120  hdmapval2  37124  hdmap11lem2  37134  ellz1  37330  rencldnfilem  37384  jm2.22  37562  jm2.23  37563  wepwsolem  37612  fnwe2lem2  37621  aomclem8  37631  unxpwdom3  37665  ifpbi12  37833  ifpbi123  37835  relintabex  37887  ss2iundf  37951  frege124d  38053  clsk3nimkb  38338  clsk1indlem1  38343  clsk1independent  38344  ntrneineine1lem  38382  ntrneicls11  38388  clsneiel1  38406  clsneiel2  38407  neicvgel1  38417  neicvgel2  38418  radcnvrat  38513  rusbcALT  38640  en3lpVD  39080  eliin2f  39287  nssd  39288  wessf1ornlem  39371  limsupre2lem  39956  icccncfext  40100  stoweidlem14  40231  stoweidlem34  40251  stoweidlem59  40276  etransclem24  40475  nnfoctbdjlem  40672  nnfoctbdj  40673  hspmbllem2  40841  smfmbfcex  40968  nsssmfmbflem  40986  eu2ndop1stv  41202  afvfv0bi  41232  afvco2  41256  ndmaovg  41264  nelbr  41291  otiunsndisjX  41298  fun2dmnopgexmpl  41303  ltnltne  41313  fmtnoinf  41448  odz2prm2pw  41475  prmdvdsfmtnof1lem2  41497  lighneallem3  41524  lighneallem4  41527  isodd3  41565  bits0ALTV  41590  lidldomnnring  41930  zrninitoringc  42071  ztprmneprm  42125  lindepsnlininds  42241  islindeps  42242  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  difmodm1lt  42317  elsetrecslem  42444