Theorem notbid 318

Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)

Hypothesis

Ref	Expression
notbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
notbid	⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Proof of Theorem notbid

Step	Hyp	Ref	Expression
1		notbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		notnotb 315	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
3		notnotb 315	. . 3 ⊢ (𝜒 ↔ ¬ ¬ 𝜒)
4	1, 2, 3	3bitr3g 313	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
5	4	con4bid 317	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  notbi  319  annotanannot  835  con3ALT  1085  xorbi12d  1527  equsexvw  2007  cbvexvw  2039  cbvexdvaw  2041  excomimw  2046  hbe1w  2052  19.8aw  2054  exexw  2055  ru0  2133  cbvexv1  2345  cbvex2v  2347  drex1v  2373  cbvex  2402  cbvex2  2415  drex1  2444  eujustALT  2571  necon3abid  2967  neleq12d  3040  cbvrexdva  3216  cbvrexfw  3276  rexeqbidvvOLD  3306  cbvrexdva2  3318  cbvrexf  3330  cbvexeqsetf  3454  cgsex4gOLD  3487  ceqsex  3488  ceqsexv  3489  gencbval  3500  spcegf  3545  spc2gv  3553  spc2d  3555  spc3gv  3557  ceqsralbv  3610  cdeqnot  3725  rru  3736  ruOLD  3738  sbcng  3787  sbcrext  3822  cbvrexcsf  3891  difjust  3902  eldif  3910  dfpss3  4040  dfdif3OLD  4069  difeq2  4071  disjne  4406  pssdifcom1  4441  eldifpr  4614  rexsng  4632  elpwunsn  4640  eldiftp  4643  rexprg  4653  preqsnd  4814  disjxun  5095  nalset  5257  dtruALT2  5314  dtruALT  5332  rexxfrd  5353  rexxfr2d  5355  rexxfrd2  5357  rexxfr  5360  opthneg  5428  snopeqop  5453  otiunsndisj  5467  poeq1  5534  pocl  5539  swopo  5542  sotric  5561  sotrieq  5562  isso2i  5568  somo  5570  freq1  5590  frirr  5599  fr2nr  5600  frminex  5602  tz7.2  5606  wereu2  5620  poinxp  5704  frinxp  5706  posn  5709  frsn  5711  rexiunxp  5788  rexxpf  5795  intirr  6074  poirr2  6080  cnvpo  6244  dfpo2  6253  predpoirr  6290  predfrirr  6291  frpomin  6297  nordeq  6335  ordtri1  6349  ordtri3  6352  fvmpti  6939  fndmdif  6987  rexrnmptw  7040  rexrnmpt  7042  rexima  7184  f1imapss  7212  f1ounsn  7218  cbvexfo  7236  nf1const  7250  soisoi  7274  isopolem  7291  weniso  7300  imaeqsalvOLD  7310  canth  7312  riotaclb  7356  rexrnmpo  7498  ndmovg  7541  sorpssuni  7677  sorpssint  7678  fr3nr  7717  dfwe2  7719  ordsucsssuc  7765  nlimsucg  7784  orduninsuc  7785  dfom2  7810  ssnlim  7828  resf1extb  7876  f1oweALT  7916  frxp  8068  poxp  8070  frxp2  8086  frxp3  8093  xpord3inddlem  8096  soseq  8101  suppofssd  8145  suppcoss  8149  smoword  8298  tz7.48lem  8372  oacan  8475  oaword  8476  omlimcl  8505  omeulem1  8509  nnaword  8555  nnmword  8561  nneob  8584  naddss1  8617  brdifun  8666  swoer  8667  undifixp  8874  boxcutc  8881  2dom  8969  php  9133  phpeqd  9138  nndomog  9139  onomeneq  9140  nnsdomo  9145  unxpdomlem2  9159  frfi  9187  unfilem1  9207  tfsnfin2  9265  supeq3  9354  supeq123d  9355  supmo  9357  eqsup  9361  supub  9364  sup0  9372  suppr  9377  supisolem  9379  supisoex  9380  eqinf  9390  infval  9392  infmo  9402  infpr  9410  infempty  9414  oieq1  9419  ordtypecbv  9424  ordtypelem7  9431  wemapsolem  9457  canthwdom  9486  zfregcl  9501  zfregclOLD  9502  elirrv  9504  elirrvOLD  9505  elirr  9506  noinfep  9571  cantnfp1lem3  9591  ttrcltr  9627  rankr1clem  9734  carden2b  9881  domtri2  9903  alephord3  9990  alephdom2  9999  alephval3  10022  dfac9  10049  kmlem2  10064  kmlem4  10066  isfin4  10209  isfin7  10213  fin23lem11  10229  isf32lem5  10269  isf34lem4  10289  fin1a2lem6  10317  fin1a2lem7  10318  fin1a2lem12  10323  itunisuc  10331  ac6n  10397  zorn2g  10415  zornn0g  10417  ttukeylem7  10427  infinfg  10478  axpowndlem3  10512  axpowndlem4  10513  axregnd  10517  elgch  10535  engch  10541  fpwwe2lem12  10555  fpwwe2  10556  pwfseqlem1  10571  pwfseqlem3  10573  hargch  10586  addnidpi  10814  pinq  10840  nqereu  10842  ltsonq  10882  prlem934  10946  ltexprlem7  10955  addcanpr  10959  prlem936  10960  reclem2pr  10961  reclem3pr  10962  supexpr  10967  ltsosr  11007  supsrlem  11024  axpre-lttri  11078  axpre-sup  11082  xrlenlt  11199  axlttri  11206  axsup  11210  ltne  11232  dedekind  11298  readdcan  11309  leadd1  11607  ltsub1  11635  ltsub2  11636  leord1  11666  lediv1  12009  lemuldiv  12024  lerec  12027  le2msq  12044  infm3  12103  suprnub  12109  infregelb  12128  avgle1  12383  avgle2  12384  znnnlt1  12520  indstr  12831  zsupss  12852  uzsupss  12855  rpneg  12941  xralrple  13122  xleneg  13135  xltadd1  13173  xposdif  13179  xmulneg1  13186  xltmul1  13209  xrsupexmnf  13222  xrinfmexpnf  13223  xrsupsslem  13224  xrinfmsslem  13225  xrub  13229  supxrleub  13243  infxrgelb  13253  difreicc  13402  nn0disj  13562  nelfzo  13582  elfznelfzo  13691  fvinim0ffz  13707  injresinjlem  13708  ssnn0fi  13910  leexp2  14096  exp11nnd  14186  hashbnd  14261  hasheni  14273  hashfundm  14367  hashbc  14378  wrdsymb0  14474  swrdnd  14580  swrdnd2  14581  pfxnd0  14614  repswswrd  14709  repswccat  14711  cshwidxmod  14728  cnpart  15165  sqrtlt  15186  limsuplt  15404  rlimrege0  15504  isercoll  15593  efle  16045  odd2np1  16270  sumodd  16317  divalglem7  16328  ndvdsadd  16339  fldivndvdslt  16345  bitsfval  16352  bitsval  16353  bits0  16357  bitsp1  16360  bitsmod  16365  bitscmp  16367  bitsinv1lem  16370  sadadd2lem2  16379  saddisjlem  16393  bitsshft  16404  gcdneg  16451  algcvgblem  16506  lcmneg  16532  isprm3  16612  dvdsnprmd  16619  isprm5  16636  rpexp  16651  phiprmpw  16705  m1dvdsndvds  16728  pythagtrip  16764  pcgcd1  16807  prmpwdvds  16834  prmreclem2  16847  prmreclem3  16848  prmreclem5  16850  prmreclem6  16851  vdwlem6  16916  vdwnnlem2  16926  vdwnnlem3  16927  vdwnn  16928  prmlem0  17035  prmlem1a  17036  divsfval  17470  mrisval  17555  ismri  17556  ismri2dad  17562  cidpropd  17635  cat1lem  18022  plttr  18265  joinval  18300  meetval  18314  acsfiindd  18478  isnsgrp  18650  smndex1n0mnd  18839  mgm2nsgrplem2  18846  sgrp2nmndlem3  18852  symgpssefmnd  19327  symgfix2  19347  pmtrdifellem4  19410  psgnunilem1  19424  psgnunilem5  19425  psgnunilem2  19426  psgnunilem3  19427  pmtrsn  19450  sylow1lem3  19531  sylow2alem2  19549  efgsfo  19670  ablfac1eulem  20005  ablfac1eu  20006  pgpfac1lem1  20007  pgpfac1lem5  20012  nzrunit  20459  zrninitoringc  20611  islbs  21030  lbsind  21034  lbspss  21036  lbspropd  21053  lspsnne1  21074  islbs2  21111  lbsacsbs  21113  lbsextlem1  21115  lbsextlem3  21117  lbsextlem4  21118  lbsextg  21119  frlmlbs  21754  islindf  21769  islinds2  21770  islindf2  21771  lindfind  21773  lindsind  21774  lindfrn  21778  lindfmm  21784  lsslindf  21787  islindf4  21795  opsrtoslem2  22013  psdmul  22111  cply1coe0  22247  cply1coe0bi  22248  mdetunilem7  22564  mdetunilem8  22565  mdetunilem9  22566  maducoeval2  22586  pmatcollpw3fi1lem1  22732  fvmptnn04ifa  22796  fvmptnn04ifc  22798  fvmptnn04ifd  22799  chfacffsupp  22802  chfacfscmul0  22804  chfacfpmmul0  22808  elcls  23019  maxlp  23093  perfi  23101  ordtbaslem  23134  ordtval  23135  ordtbas2  23137  ordtopn1  23140  ordtopn2  23141  ordtcnv  23147  ordtrest  23148  ordtrest2lem  23149  ordtrest2  23150  pnfnei  23166  mnfnei  23167  isreg2  23323  ordthauslem  23329  cmpfi  23354  cmpfii  23355  bwth  23356  nconnsubb  23369  hausdiag  23591  txkgen  23598  kqdisj  23678  ordthmeolem  23747  fbfinnfr  23787  trfbas  23790  fbunfip  23815  fbasrn  23830  trfil3  23834  ufileu  23865  fin1aufil  23878  hausflim  23927  alexsubALTlem2  23994  alexsubALTlem3  23995  alexsubALTlem4  23996  ptcmplem2  23999  ptcmplem3  24000  stdbdbl  24463  iccntr  24768  reconnlem2  24774  iccpnfcnv  24900  xrhmeo  24902  lebnumlem1  24918  lebnumlem2  24919  lebnumlem3  24920  bcthlem4  25285  minveclem3b  25386  ivthlem2  25411  ivthlem3  25412  mbfmax  25608  mbfposr  25611  i1fd  25640  mbfi1fseqlem4  25677  itg2splitlem  25707  itg2monolem1  25709  itg2cnlem1  25720  dvne0  25974  lhop1lem  25976  deg1nn0clb  26053  dgrle  26206  coemulhi  26217  aaliou3lem9  26316  cos11  26500  logleb  26570  argrege0  26578  logdivle  26589  ellogdm  26606  cxple  26662  cxplt2  26665  cxple3  26668  isosctrlem1  26786  atandm  26844  atans2  26899  atantayl2  26906  eldmgm  26990  ftalem7  27047  isppw2  27083  musum  27159  dchrsum2  27237  bposlem1  27253  lgsmod  27292  lgsdir2lem2  27295  lgsdir2  27299  lgsne0  27304  lgsprme0  27308  gausslemma2dlem4  27338  lgsquadlem1  27349  2lgslem3  27373  2lgsoddprm  27385  2sq2  27402  addsqrexnreu  27411  rpvmasumlem  27456  padicabv  27599  ostth3  27607  ostth  27608  noextenddif  27638  nodenselem4  27657  nodenselem5  27658  nodenselem7  27660  nolt02o  27665  nogt01o  27666  noresle  27667  nosupprefixmo  27670  noinfprefixmo  27671  nosupcbv  27672  nosupdm  27674  nosupfv  27676  nosupres  27677  nosupbnd1lem1  27678  nosupbnd1lem3  27680  nosupbnd1lem5  27682  nosupbnd1  27684  nosupbnd2lem1  27685  nosupbnd2  27686  noinfcbv  27687  noinfdm  27689  noinffv  27691  noinfres  27692  noinfbnd1lem1  27693  noinfbnd1lem3  27695  noinfbnd1lem5  27697  noinfbnd1  27699  noinfbnd2lem1  27700  noinfbnd2  27701  slenlt  27722  sltne  27744  nocvxminlem  27752  slerec  27795  eqscut3  27800  cuteq1  27813  newbday  27882  sltlpss  27888  cofcutr  27904  lrrecfr  27923  addsval  27942  sltadd2  27971  sleneg  28026  slesubsubbd  28066  slesubsub2bd  28067  slesubsub3bd  28068  slesubaddd  28073  sltmul2  28151  slemul2d  28154  slemul1d  28155  onscutlt  28243  onsle  28247  pw2cut2  28439  bdaypw2bnd  28442  bdayfinbndlem1  28444  istrkgld  28512  axtgupdim2  28524  tglowdim2l  28703  axlowdimlem16  29011  axlowdim2  29014  axlowdim  29015  numedglnl  29198  usgredg2v  29281  lfuhgr1v0e  29308  cusgrfi  29513  vtxd0nedgb  29543  vtxduhgr0edgnel  29549  1loopgrnb0  29557  1hevtxdg0  29560  vtxdgoddnumeven  29608  wlkp1lem1  29726  wlkp1lem2  29727  wlkp1lem5  29730  dfpth2  29783  crctcsh  29878  clwlkclwwlklem2a4  30053  eupth2eucrct  30273  eupth2lem3lem3  30286  eupth2lem3lem4  30287  eupth2lem3lem6  30289  eupth2lem3lem7  30290  eupth2lems  30294  eupth2  30295  konigsberglem4  30311  nfrgr2v  30328  frgrwopreglem3  30370  fusgr2wsp2nb  30390  frgrreggt1  30449  friendshipgt3  30454  lpni  30536  nmobndseqi  30835  minvecolem5  30937  chpsscon3  31559  chnle  31570  nonbooli  31707  pjnel  31782  specval  31954  nmcfnlbi  32108  stri  32313  hstri  32321  cvbr  32338  cvcon3  32340  chcv1  32411  cvexchlem  32424  chrelat2  32426  nelun  32568  elpreq  32583  nelpr  32586  ifeqeqx  32597  nfpconfp  32690  suppiniseg  32744  isoun  32760  suppss3  32781  xrge0infss  32819  infxrge0gelb  32825  eliccelico  32836  elicoelioo  32837  nndiffz1  32845  hashgt1  32867  expgt0b  32876  nn0min  32880  ccatws1f1o  33012  toslublem  33033  tosglblem  33035  pmtrcnel  33150  cycpmco2  33194  isarchi2  33246  archiabl  33259  elrgspnlem2  33304  elrgspnlem3  33305  0nellinds  33430  lindssn  33438  lindfpropd  33442  ssdifidlprm  33518  mxidlirred  33532  ssmxidl  33534  esplyind  33710  lbslsat  33752  lindsunlem  33760  rtelextdg2lem  33862  constrsqrtcl  33915  ordtcnvNEW  34056  ordtrestNEW  34057  ordtrest2NEWlem  34058  ordtrest2NEW  34059  ordtconnlem1  34060  xrge0iifcnv  34069  esumpcvgval  34214  esum2d  34229  ddemeas  34372  omssubadd  34436  oddpwdc  34490  eulerpartlems  34496  eulerpartlemf  34506  eulerpartlemt  34507  eulerpartlemr  34510  eulerpartlemgvv  34512  eulerpartlemn  34517  ballotlemfc0  34629  ballotlemfcc  34630  ballotlem4  34635  ballotlemimin  34642  ballotlem7  34672  plymulx  34684  signsply0  34687  reprinfz1  34758  reprpmtf1o  34762  reprdifc  34763  hgt750lema  34793  hgt750leme  34794  istrkg2d  34802  bnj23  34853  bnj1185  34928  bnj1228  35146  bnj1388  35168  bnj1417  35176  nummin  35228  axnulg  35243  fineqvnttrclselem1  35256  onvf1odlem2  35277  onvf1odlem3  35278  revwlk  35298  isacycgr  35318  acycgr0v  35321  prclisacycgr  35324  erdszelem10  35373  satf0n0  35551  fmlaomn0  35563  fmlasucdisj  35572  satfv1fvfmla1  35596  satefvfmla1  35598  ismfs  35722  mvtinf  35728  untelirr  35881  untsucf  35883  untangtr  35887  dfon2lem3  35956  dfon2lem4  35957  dfon2lem7  35960  dfon2lem9  35962  distel  35974  funpartfv  36118  dfrdg4  36124  nn0prpwlem  36495  nn0prpw  36496  limsucncmpi  36618  limsucncmp  36619  ordcmp  36620  weiunlem2  36636  weiunfrlem  36637  weiunfr  36640  unblimceq0  36680  unbdqndv1  36681  bj-hbntbi  36878  bj-equsexvwd  36955  bj-cbvexdv  36974  bj-ru1  37117  bj-nuliota  37231  topdifinffinlem  37521  topdifinffin  37522  icorempo  37525  relowlpssretop  37538  finxpreclem2  37564  finxpreclem6  37570  wl-issetft  37756  wl-eujustlem1  37762  leceifl  37779  lindsadd  37783  lindsenlbs  37785  matunitlindflem1  37786  poimirlem16  37806  poimirlem17  37807  poimirlem18  37808  poimirlem19  37809  poimirlem21  37811  poimirlem23  37813  poimirlem26  37816  poimirlem27  37817  poimirlem28  37818  poimirlem31  37821  poimir  37823  mblfinlem2  37828  mblfinlem3  37829  ismblfin  37831  cnambfre  37838  itg2addnclem  37841  itg2addnclem2  37842  iblabsnclem  37853  ftc1anclem1  37863  areacirc  37883  heibor1lem  37979  heiborlem1  37981  heiborlem6  37986  heiborlem8  37988  heiborlem10  37990  smprngopr  38222  ecin0  38522  ax12inda  39243  riotaclbgBAD  39249  lcvfbr  39315  lcvbr  39316  lsatcv0  39326  l1cvpat  39349  opltcon3b  39499  cvrfval  39563  cvrval  39564  cvrnbtwn  39566  cvrval2  39569  cvrnbtwn2  39570  cvrnbtwn3  39571  cvrcon3b  39572  cvrnbtwn4  39574  atnlt  39608  iscvlat  39618  cvlexch1  39623  hlsuprexch  39676  hlrelat5N  39696  hlrelat2  39698  cvrval5  39710  3dimlem1  39753  3dim1lem5  39761  3dim2  39763  3dim3  39764  llnnlt  39818  islpln5  39830  lplni2  39832  lvolex3N  39833  lplnnle2at  39836  islpln2a  39843  lplnribN  39846  lplnexllnN  39859  lplnnlt  39860  lvoli3  39872  islvol5  39874  lvoli2  39876  lvolnle3at  39877  islvol2aN  39887  4atlem11  39904  lvolnltN  39913  dalawlem15  40180  4atexlemex2  40366  4atex  40371  4atex2-0aOLDN  40373  4atex2-0cOLDN  40375  lautcvr  40387  ltrnfset  40412  ltrnset  40413  ltrnu  40416  trlfset  40455  trlset  40456  trlval2  40458  cdlemd6  40498  cdleme0nex  40585  cdleme18d  40590  cdleme25b  40649  cdleme25cv  40653  cdleme29b  40670  cdleme31fv  40685  cdleme31fv2  40688  cdlemefrs29bpre0  40691  cdlemefr32sn2aw  40699  cdlemefr29bpre0N  40701  cdlemefr29clN  40702  cdlemefr32fvaN  40704  cdlemefr32fva1  40705  cdlemefs32sn1aw  40709  cdleme32fva  40732  cdleme32fvaw  40734  cdleme40v  40764  cdleme42b  40773  cdleme46f2g2  40788  cdleme46f2g1  40789  cdleme48gfv  40832  cdlemg1fvawlemN  40868  cdlemg1cex  40883  cdlemg6d  40916  cdlemm10N  41413  dicffval  41469  dicfval  41470  dicval  41471  dicfnN  41478  dicvalrelN  41480  dihffval  41525  dihfval  41526  dihlsscpre  41529  dvh4dimat  41733  dvh3dimatN  41734  dvh4dimlem  41738  dvh3dim  41741  dvh4dimN  41742  dvh3dim2  41743  dvh3dim3N  41744  mapdcv  41955  mapdh9aOLDN  42085  hdmapfval  42122  hdmapval  42123  hdmapval2  42127  hdmap11lem2  42137  dvrelog2b  42355  aks4d1p4  42368  aks4d1p5  42369  aks4d1p7  42372  aks4d1p8d2  42374  aks4d1p8  42376  aks4d1  42378  aks6d1c2p2  42408  hashnexinj  42417  rspcsbnea  42420  aks6d1c5  42428  aks6d1c6lem3  42461  aks6d1c7  42473  supinf  42534  oexpreposd  42614  mullt0b2d  42776  flt4lem7  42939  nna4b4nsq  42940  ellz1  43046  rencldnfilem  43099  jm2.22  43274  jm2.23  43275  wepwsolem  43321  fnwe2lem2  43330  aomclem8  43340  unxpwdom3  43374  onsupmaxb  43518  onexlimgt  43522  onsupeqnmax  43526  onov0suclim  43553  oaordnr  43575  omnord1  43584  oenord1  43595  oaomoencom  43596  oenass  43598  cantnfresb  43603  tfsnfin  43631  ralopabb  43689  nlimsuc  43719  ifpbi12  43766  dfsucon  43801  sqrtcvallem1  43909  ss2iundf  43937  frege124d  44039  clsk3nimkb  44318  clsk1indlem1  44323  clsk1independent  44324  ntrneineine1lem  44362  ntrneicls11  44368  clsneiel1  44386  clsneiel2  44387  neicvgel1  44397  neicvgel2  44398  radcnvrat  44592  rusbcALT  44716  en3lpVD  45122  0elaxnul  45261  omssaxinf2  45266  permaxnul  45286  permaxinf2lem  45290  nregmodel  45295  eliin2f  45385  nssd  45386  wessf1ornlem  45466  rexanuz2nf  45773  limsupre2lem  46005  icccncfext  46168  stoweidlem14  46295  stoweidlem34  46315  stoweidlem59  46340  etransclem24  46539  nnfoctbdjlem  46736  nnfoctbdj  46737  hspmbllem2  46908  nsssmfmbflem  47059  fsetsnprcnex  47338  eu2ndop1stv  47408  afvfv0bi  47435  afvco2  47459  ndmaovg  47467  ndfatafv2nrn  47504  afv2ndefb  47507  afv2fv0  47548  nelbr  47557  otiunsndisjX  47562  fun2dmnopgexmpl  47567  ltnltne  47582  readdcnnred  47586  resubcnnred  47587  recnmulnred  47588  cndivrenred  47589  ichnreuop  47755  fmtnoinf  47819  odz2prm2pw  47846  prmdvdsfmtnof1lem2  47868  lighneallem3  47890  lighneallem4  47893  requad1  47905  isodd3  47935  bits0ALTV  47962  nfermltl8rev  48025  nfermltl2rev  48026  nfermltlrev  48027  upgrimpths  48192  isubgr3stgrlem3  48251  usgrexmpl12ngric  48321  pgnbgreunbgrlem2lem1  48397  pgnbgreunbgrlem2lem2  48398  pgnbgreunbgrlem2lem3  48399  pgnbgreunbgrlem5lem1  48403  pgnbgreunbgrlem5lem2  48404  pgnbgreunbgrlem5lem3  48405  lgricngricex  48412  lidldomnnring  48519  ztprmneprm  48630  lindepsnlininds  48735  islindeps  48736  lindslinindsimp2lem5  48745  lindslinindsimp2  48746  line2ylem  49034  line2xlem  49036  map0cor  49137  nelsubc3lem  49352  fulltermc2  49794  setc1onsubc  49884  cnelsubclem  49885  elsetrecslem  49981