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  834  con3ALT  1084  xorbi12d  1525  equsexvw  2005  cbvexvw  2037  cbvexdvaw  2039  excomimw  2044  hbe1w  2049  19.8aw  2051  exexw  2052  ru0  2128  cbvexv1  2340  cbvex2v  2342  drex1v  2368  cbvex  2397  cbvex2  2410  drex1  2439  eujustALT  2565  necon3abid  2961  neleq12d  3034  cbvrexdva  3210  cbvrexfw  3270  rexeqbidvvOLD  3300  cbvrexdva2  3312  cbvrexf  3324  cbvexeqsetf  3451  cgsex4gOLD  3484  ceqsex  3485  ceqsexv  3487  gencbval  3498  spcegf  3547  spc2gv  3555  spc2d  3557  spc3gv  3559  ceqsralbv  3612  cdeqnot  3728  rru  3739  ruOLD  3741  sbcng  3790  sbcrext  3825  cbvrexcsf  3894  difjust  3905  eldif  3913  dfpss3  4040  dfdif3OLD  4069  difeq2  4071  disjne  4406  pssdifcom1  4441  eldifpr  4610  rexsng  4628  elpwunsn  4636  eldiftp  4639  rexprg  4649  preqsnd  4810  disjxun  5090  nalset  5252  dtruALT2  5309  dtruALT  5327  rexxfrd  5348  rexxfr2d  5350  rexxfrd2  5352  rexxfr  5355  opthneg  5424  snopeqop  5449  otiunsndisj  5463  poeq1  5530  pocl  5535  swopo  5538  sotric  5557  sotrieq  5558  isso2i  5564  somo  5566  freq1  5586  frirr  5595  fr2nr  5596  frminex  5598  tz7.2  5602  wereu2  5616  poinxp  5700  frinxp  5702  posn  5705  frsn  5707  rexiunxp  5783  rexxpf  5790  intirr  6067  poirr2  6073  cnvpo  6235  dfpo2  6244  predpoirr  6281  predfrirr  6282  frpomin  6288  nordeq  6326  ordtri1  6340  ordtri3  6343  fvmpti  6929  fndmdif  6976  rexrnmptw  7029  rexrnmpt  7031  rexima  7174  f1imapss  7203  f1ounsn  7209  cbvexfo  7227  nf1const  7241  soisoi  7265  isopolem  7282  weniso  7291  imaeqsalvOLD  7301  canth  7303  riotaclb  7347  rexrnmpo  7489  ndmovg  7532  sorpssuni  7668  sorpssint  7669  fr3nr  7708  dfwe2  7710  ordsucsssuc  7756  nlimsucg  7775  orduninsuc  7776  dfom2  7801  ssnlim  7819  resf1extb  7867  f1oweALT  7907  frxp  8059  poxp  8061  frxp2  8077  frxp3  8084  xpord3inddlem  8087  soseq  8092  suppofssd  8136  suppcoss  8140  smoword  8289  tz7.48lem  8363  oacan  8466  oaword  8467  omlimcl  8496  omeulem1  8500  nnaword  8545  nnmword  8551  nneob  8574  naddss1  8607  brdifun  8655  swoer  8656  undifixp  8861  boxcutc  8868  2dom  8955  php  9121  phpeqd  9126  nndomog  9127  onomeneq  9128  nnsdomo  9132  unxpdomlem2  9146  frfi  9174  unfilem1  9194  supeq3  9339  supeq123d  9340  supmo  9342  eqsup  9346  supub  9349  sup0  9357  suppr  9362  supisolem  9364  supisoex  9365  eqinf  9375  infval  9377  infmo  9387  infpr  9395  infempty  9399  oieq1  9404  ordtypecbv  9409  ordtypelem7  9416  wemapsolem  9442  canthwdom  9471  zfregcl  9486  zfregclOLD  9487  elirrv  9489  elirrvOLD  9490  elirr  9491  noinfep  9556  cantnfp1lem3  9576  ttrcltr  9612  rankr1clem  9716  carden2b  9863  domtri2  9885  alephord3  9972  alephdom2  9981  alephval3  10004  dfac9  10031  kmlem2  10046  kmlem4  10048  isfin4  10191  isfin7  10195  fin23lem11  10211  isf32lem5  10251  isf34lem4  10271  fin1a2lem6  10299  fin1a2lem7  10300  fin1a2lem12  10305  itunisuc  10313  ac6n  10379  zorn2g  10397  zornn0g  10399  ttukeylem7  10409  axpowndlem3  10493  axpowndlem4  10494  axregnd  10498  elgch  10516  engch  10522  fpwwe2lem12  10536  fpwwe2  10537  pwfseqlem1  10552  pwfseqlem3  10554  hargch  10567  addnidpi  10795  pinq  10821  nqereu  10823  ltsonq  10863  prlem934  10927  ltexprlem7  10936  addcanpr  10940  prlem936  10941  reclem2pr  10942  reclem3pr  10943  supexpr  10948  ltsosr  10988  supsrlem  11005  axpre-lttri  11059  axpre-sup  11063  xrlenlt  11180  axlttri  11187  axsup  11191  ltne  11213  dedekind  11279  readdcan  11290  leadd1  11588  ltsub1  11616  ltsub2  11617  leord1  11647  lediv1  11990  lemuldiv  12005  lerec  12008  le2msq  12025  infm3  12084  suprnub  12090  infregelb  12109  avgle1  12364  avgle2  12365  znnnlt1  12502  indstr  12817  zsupss  12838  uzsupss  12841  rpneg  12927  xralrple  13107  xleneg  13120  xltadd1  13158  xposdif  13164  xmulneg1  13171  xltmul1  13194  xrsupexmnf  13207  xrinfmexpnf  13208  xrsupsslem  13209  xrinfmsslem  13210  xrub  13214  supxrleub  13228  infxrgelb  13238  difreicc  13387  nn0disj  13547  nelfzo  13567  elfznelfzo  13675  fvinim0ffz  13689  injresinjlem  13690  ssnn0fi  13892  leexp2  14078  exp11nnd  14168  hashbnd  14243  hasheni  14255  hashfundm  14349  hashbc  14360  wrdsymb0  14456  swrdnd  14561  swrdnd2  14562  pfxnd0  14595  repswswrd  14690  repswccat  14692  cshwidxmod  14709  cnpart  15147  sqrtlt  15168  limsuplt  15386  rlimrege0  15486  isercoll  15575  efle  16027  odd2np1  16252  sumodd  16299  divalglem7  16310  ndvdsadd  16321  fldivndvdslt  16327  bitsfval  16334  bitsval  16335  bits0  16339  bitsp1  16342  bitsmod  16347  bitscmp  16349  bitsinv1lem  16352  sadadd2lem2  16361  saddisjlem  16375  bitsshft  16386  gcdneg  16433  algcvgblem  16488  lcmneg  16514  isprm3  16594  dvdsnprmd  16601  isprm5  16618  rpexp  16633  phiprmpw  16687  m1dvdsndvds  16710  pythagtrip  16746  pcgcd1  16789  prmpwdvds  16816  prmreclem2  16829  prmreclem3  16830  prmreclem5  16832  prmreclem6  16833  vdwlem6  16898  vdwnnlem2  16908  vdwnnlem3  16909  vdwnn  16910  prmlem0  17017  prmlem1a  17018  divsfval  17451  mrisval  17536  ismri  17537  ismri2dad  17543  cidpropd  17616  cat1lem  18003  plttr  18246  joinval  18281  meetval  18295  acsfiindd  18459  isnsgrp  18597  smndex1n0mnd  18786  mgm2nsgrplem2  18793  sgrp2nmndlem3  18799  symgpssefmnd  19275  symgfix2  19295  pmtrdifellem4  19358  psgnunilem1  19372  psgnunilem5  19373  psgnunilem2  19374  psgnunilem3  19375  pmtrsn  19398  sylow1lem3  19479  sylow2alem2  19497  efgsfo  19618  ablfac1eulem  19953  ablfac1eu  19954  pgpfac1lem1  19955  pgpfac1lem5  19960  nzrunit  20409  zrninitoringc  20561  islbs  20980  lbsind  20984  lbspss  20986  lbspropd  21003  lspsnne1  21024  islbs2  21061  lbsacsbs  21063  lbsextlem1  21065  lbsextlem3  21067  lbsextlem4  21068  lbsextg  21069  frlmlbs  21704  islindf  21719  islinds2  21720  islindf2  21721  lindfind  21723  lindsind  21724  lindfrn  21728  lindfmm  21734  lsslindf  21737  islindf4  21745  opsrtoslem2  21961  psdmul  22051  cply1coe0  22186  cply1coe0bi  22187  mdetunilem7  22503  mdetunilem8  22504  mdetunilem9  22505  maducoeval2  22525  pmatcollpw3fi1lem1  22671  fvmptnn04ifa  22735  fvmptnn04ifc  22737  fvmptnn04ifd  22738  chfacffsupp  22741  chfacfscmul0  22743  chfacfpmmul0  22747  elcls  22958  maxlp  23032  perfi  23040  ordtbaslem  23073  ordtval  23074  ordtbas2  23076  ordtopn1  23079  ordtopn2  23080  ordtcnv  23086  ordtrest  23087  ordtrest2lem  23088  ordtrest2  23089  pnfnei  23105  mnfnei  23106  isreg2  23262  ordthauslem  23268  cmpfi  23293  cmpfii  23294  bwth  23295  nconnsubb  23308  hausdiag  23530  txkgen  23537  kqdisj  23617  ordthmeolem  23686  fbfinnfr  23726  trfbas  23729  fbunfip  23754  fbasrn  23769  trfil3  23773  ufileu  23804  fin1aufil  23817  hausflim  23866  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALTlem4  23935  ptcmplem2  23938  ptcmplem3  23939  stdbdbl  24403  iccntr  24708  reconnlem2  24714  iccpnfcnv  24840  xrhmeo  24842  lebnumlem1  24858  lebnumlem2  24859  lebnumlem3  24860  bcthlem4  25225  minveclem3b  25326  ivthlem2  25351  ivthlem3  25352  mbfmax  25548  mbfposr  25551  i1fd  25580  mbfi1fseqlem4  25617  itg2splitlem  25647  itg2monolem1  25649  itg2cnlem1  25660  dvne0  25914  lhop1lem  25916  deg1nn0clb  25993  dgrle  26146  coemulhi  26157  aaliou3lem9  26256  cos11  26440  logleb  26510  argrege0  26518  logdivle  26529  ellogdm  26546  cxple  26602  cxplt2  26605  cxple3  26608  isosctrlem1  26726  atandm  26784  atans2  26839  atantayl2  26846  eldmgm  26930  ftalem7  26987  isppw2  27023  musum  27099  dchrsum2  27177  bposlem1  27193  lgsmod  27232  lgsdir2lem2  27235  lgsdir2  27239  lgsne0  27244  lgsprme0  27248  gausslemma2dlem4  27278  lgsquadlem1  27289  2lgslem3  27313  2lgsoddprm  27325  2sq2  27342  addsqrexnreu  27351  rpvmasumlem  27396  padicabv  27539  ostth3  27547  ostth  27548  noextenddif  27578  nodenselem4  27597  nodenselem5  27598  nodenselem7  27600  nolt02o  27605  nogt01o  27606  noresle  27607  nosupprefixmo  27610  noinfprefixmo  27611  nosupcbv  27612  nosupdm  27614  nosupfv  27616  nosupres  27617  nosupbnd1lem1  27618  nosupbnd1lem3  27620  nosupbnd1lem5  27622  nosupbnd1  27624  nosupbnd2lem1  27625  nosupbnd2  27626  noinfcbv  27627  noinfdm  27629  noinffv  27631  noinfres  27632  noinfbnd1lem1  27633  noinfbnd1lem3  27635  noinfbnd1lem5  27637  noinfbnd1  27639  noinfbnd2lem1  27640  noinfbnd2  27641  slenlt  27662  sltne  27680  nocvxminlem  27688  slerec  27731  eqscut3  27736  cuteq1  27749  newbday  27818  sltlpss  27824  cofcutr  27839  lrrecfr  27857  addsval  27876  sltadd2  27905  sleneg  27959  slesubsubbd  27997  slesubsub2bd  27998  slesubsub3bd  27999  slesubaddd  28004  sltmul2  28081  slemul2d  28084  slemul1d  28085  onscutlt  28172  pw2cut2  28353  istrkgld  28408  axtgupdim2  28420  tglowdim2l  28599  axlowdimlem16  28906  axlowdim2  28909  axlowdim  28910  numedglnl  29093  usgredg2v  29176  lfuhgr1v0e  29203  cusgrfi  29408  vtxd0nedgb  29438  vtxduhgr0edgnel  29444  1loopgrnb0  29452  1hevtxdg0  29455  vtxdgoddnumeven  29503  wlkp1lem1  29621  wlkp1lem2  29622  wlkp1lem5  29625  dfpth2  29678  crctcsh  29773  clwlkclwwlklem2a4  29945  eupth2eucrct  30165  eupth2lem3lem3  30178  eupth2lem3lem4  30179  eupth2lem3lem6  30181  eupth2lem3lem7  30182  eupth2lems  30186  eupth2  30187  konigsberglem4  30203  nfrgr2v  30220  frgrwopreglem3  30262  fusgr2wsp2nb  30282  frgrreggt1  30341  friendshipgt3  30346  lpni  30428  nmobndseqi  30727  minvecolem5  30829  chpsscon3  31451  chnle  31462  nonbooli  31599  pjnel  31674  specval  31846  nmcfnlbi  32000  stri  32205  hstri  32213  cvbr  32230  cvcon3  32232  chcv1  32303  cvexchlem  32316  chrelat2  32318  nelun  32462  elpreq  32477  nelpr  32480  ifeqeqx  32491  nfpconfp  32583  suppiniseg  32636  isoun  32652  suppss3  32675  xrge0infss  32712  infxrge0gelb  32718  eliccelico  32729  elicoelioo  32730  nndiffz1  32738  hashgt1  32762  expgt0b  32770  nn0min  32774  ccatws1f1o  32902  toslublem  32923  tosglblem  32925  pmtrcnel  33040  cycpmco2  33084  isarchi2  33136  archiabl  33149  elrgspnlem2  33192  elrgspnlem3  33193  0nellinds  33316  lindssn  33324  lindfpropd  33328  ssdifidlprm  33404  mxidlirred  33418  ssmxidl  33420  lbslsat  33599  lindsunlem  33607  rtelextdg2lem  33709  constrsqrtcl  33762  ordtcnvNEW  33903  ordtrestNEW  33904  ordtrest2NEWlem  33905  ordtrest2NEW  33906  ordtconnlem1  33907  xrge0iifcnv  33916  esumpcvgval  34061  esum2d  34076  ddemeas  34219  omssubadd  34284  oddpwdc  34338  eulerpartlems  34344  eulerpartlemf  34354  eulerpartlemt  34355  eulerpartlemr  34358  eulerpartlemgvv  34360  eulerpartlemn  34365  ballotlemfc0  34477  ballotlemfcc  34478  ballotlem4  34483  ballotlemimin  34490  ballotlem7  34520  plymulx  34532  signsply0  34535  reprinfz1  34606  reprpmtf1o  34610  reprdifc  34611  hgt750lema  34641  hgt750leme  34642  istrkg2d  34650  bnj23  34701  bnj1185  34776  bnj1228  34994  bnj1388  35016  bnj1417  35024  nummin  35074  axnulg  35075  fineqvnttrclselem1  35090  onvf1odlem2  35097  onvf1odlem3  35098  revwlk  35118  isacycgr  35138  acycgr0v  35141  prclisacycgr  35144  erdszelem10  35193  satf0n0  35371  fmlaomn0  35383  fmlasucdisj  35392  satfv1fvfmla1  35416  satefvfmla1  35418  ismfs  35542  mvtinf  35548  untelirr  35701  untsucf  35703  untangtr  35707  dfon2lem3  35779  dfon2lem4  35780  dfon2lem7  35783  dfon2lem9  35785  distel  35797  funpartfv  35939  dfrdg4  35945  nn0prpwlem  36316  nn0prpw  36317  limsucncmpi  36439  limsucncmp  36440  ordcmp  36441  weiunlem2  36457  weiunfrlem  36458  weiunfr  36461  unblimceq0  36501  unbdqndv1  36502  bj-hbntbi  36698  bj-equsexvwd  36775  bj-cbvexdv  36794  bj-ru1  36937  bj-nuliota  37051  topdifinffinlem  37341  topdifinffin  37342  icorempo  37345  relowlpssretop  37358  finxpreclem2  37384  finxpreclem6  37390  wl-issetft  37576  wl-ax11-lem8  37586  leceifl  37609  lindsadd  37613  lindsenlbs  37615  matunitlindflem1  37616  poimirlem16  37636  poimirlem17  37637  poimirlem18  37638  poimirlem19  37639  poimirlem21  37641  poimirlem23  37643  poimirlem26  37646  poimirlem27  37647  poimirlem28  37648  poimirlem31  37651  poimir  37653  mblfinlem2  37658  mblfinlem3  37659  ismblfin  37661  cnambfre  37668  itg2addnclem  37671  itg2addnclem2  37672  iblabsnclem  37683  ftc1anclem1  37693  areacirc  37713  heibor1lem  37809  heiborlem1  37811  heiborlem6  37816  heiborlem8  37818  heiborlem10  37820  smprngopr  38052  ecin0  38340  ax12inda  38947  riotaclbgBAD  38953  lcvfbr  39019  lcvbr  39020  lsatcv0  39030  l1cvpat  39053  opltcon3b  39203  cvrfval  39267  cvrval  39268  cvrnbtwn  39270  cvrval2  39273  cvrnbtwn2  39274  cvrnbtwn3  39275  cvrcon3b  39276  cvrnbtwn4  39278  atnlt  39312  iscvlat  39322  cvlexch1  39327  hlsuprexch  39380  hlrelat5N  39400  hlrelat2  39402  cvrval5  39414  3dimlem1  39457  3dim1lem5  39465  3dim2  39467  3dim3  39468  llnnlt  39522  islpln5  39534  lplni2  39536  lvolex3N  39537  lplnnle2at  39540  islpln2a  39547  lplnribN  39550  lplnexllnN  39563  lplnnlt  39564  lvoli3  39576  islvol5  39578  lvoli2  39580  lvolnle3at  39581  islvol2aN  39591  4atlem11  39608  lvolnltN  39617  dalawlem15  39884  4atexlemex2  40070  4atex  40075  4atex2-0aOLDN  40077  4atex2-0cOLDN  40079  lautcvr  40091  ltrnfset  40116  ltrnset  40117  ltrnu  40120  trlfset  40159  trlset  40160  trlval2  40162  cdlemd6  40202  cdleme0nex  40289  cdleme18d  40294  cdleme25b  40353  cdleme25cv  40357  cdleme29b  40374  cdleme31fv  40389  cdleme31fv2  40392  cdlemefrs29bpre0  40395  cdlemefr32sn2aw  40403  cdlemefr29bpre0N  40405  cdlemefr29clN  40406  cdlemefr32fvaN  40408  cdlemefr32fva1  40409  cdlemefs32sn1aw  40413  cdleme32fva  40436  cdleme32fvaw  40438  cdleme40v  40468  cdleme42b  40477  cdleme46f2g2  40492  cdleme46f2g1  40493  cdleme48gfv  40536  cdlemg1fvawlemN  40572  cdlemg1cex  40587  cdlemg6d  40620  cdlemm10N  41117  dicffval  41173  dicfval  41174  dicval  41175  dicfnN  41182  dicvalrelN  41184  dihffval  41229  dihfval  41230  dihlsscpre  41233  dvh4dimat  41437  dvh3dimatN  41438  dvh4dimlem  41442  dvh3dim  41445  dvh4dimN  41446  dvh3dim2  41447  dvh3dim3N  41448  mapdcv  41659  mapdh9aOLDN  41789  hdmapfval  41826  hdmapval  41827  hdmapval2  41831  hdmap11lem2  41841  dvrelog2b  42059  aks4d1p4  42072  aks4d1p5  42073  aks4d1p7  42076  aks4d1p8d2  42078  aks4d1p8  42080  aks4d1  42082  aks6d1c2p2  42112  hashnexinj  42121  rspcsbnea  42124  aks6d1c5  42132  aks6d1c6lem3  42165  aks6d1c7  42177  supinf  42235  oexpreposd  42315  mullt0b2d  42477  flt4lem7  42652  nna4b4nsq  42653  ellz1  42760  rencldnfilem  42813  jm2.22  42988  jm2.23  42989  wepwsolem  43035  fnwe2lem2  43044  aomclem8  43054  unxpwdom3  43088  onsupmaxb  43232  onexlimgt  43236  onsupeqnmax  43240  onov0suclim  43267  oaordnr  43289  omnord1  43298  oenord1  43309  oaomoencom  43310  oenass  43312  cantnfresb  43317  tfsnfin  43345  ralopabb  43404  nlimsuc  43434  ifpbi12  43481  dfsucon  43516  sqrtcvallem1  43624  ss2iundf  43652  frege124d  43754  clsk3nimkb  44033  clsk1indlem1  44038  clsk1independent  44039  ntrneineine1lem  44077  ntrneicls11  44083  clsneiel1  44101  clsneiel2  44102  neicvgel1  44112  neicvgel2  44113  radcnvrat  44307  rusbcALT  44432  en3lpVD  44838  0elaxnul  44977  omssaxinf2  44982  permaxnul  45002  permaxinf2lem  45006  nregmodel  45011  eliin2f  45102  nssd  45103  wessf1ornlem  45183  rexanuz2nf  45491  limsupre2lem  45725  icccncfext  45888  stoweidlem14  46015  stoweidlem34  46035  stoweidlem59  46060  etransclem24  46259  nnfoctbdjlem  46456  nnfoctbdj  46457  hspmbllem2  46628  nsssmfmbflem  46779  fsetsnprcnex  47059  eu2ndop1stv  47129  afvfv0bi  47156  afvco2  47180  ndmaovg  47188  ndfatafv2nrn  47225  afv2ndefb  47228  afv2fv0  47269  nelbr  47278  otiunsndisjX  47283  fun2dmnopgexmpl  47288  ltnltne  47303  readdcnnred  47307  resubcnnred  47308  recnmulnred  47309  cndivrenred  47310  ichnreuop  47476  fmtnoinf  47540  odz2prm2pw  47567  prmdvdsfmtnof1lem2  47589  lighneallem3  47611  lighneallem4  47614  requad1  47626  isodd3  47656  bits0ALTV  47683  nfermltl8rev  47746  nfermltl2rev  47747  nfermltlrev  47748  upgrimpths  47913  isubgr3stgrlem3  47972  usgrexmpl12ngric  48042  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  pgnbgreunbgrlem2lem3  48120  pgnbgreunbgrlem5lem1  48124  pgnbgreunbgrlem5lem2  48125  pgnbgreunbgrlem5lem3  48126  lgricngricex  48133  lidldomnnring  48240  ztprmneprm  48351  lindepsnlininds  48457  islindeps  48458  lindslinindsimp2lem5  48467  lindslinindsimp2  48468  line2ylem  48756  line2xlem  48758  map0cor  48859  nelsubc3lem  49075  fulltermc2  49517  setc1onsubc  49607  cnelsubclem  49608  elsetrecslem  49704