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  2369  cbvex  2398  cbvex2  2411  drex1  2440  eujustALT  2566  necon3abid  2962  neleq12d  3035  cbvrexdva  3219  cbvrexfw  3281  rexeqbidvvOLD  3312  cbvrexdva2  3324  cbvrexf  3337  cbvexeqsetf  3465  cgsex4gOLD  3498  ceqsex  3499  ceqsexv  3501  gencbval  3512  spcegf  3561  spc2gv  3569  spc2d  3571  spc3gv  3573  ceqsralbv  3626  cdeqnot  3742  rru  3753  ruOLD  3755  sbcng  3804  sbcrext  3839  cbvrexcsf  3908  difjust  3919  eldif  3927  dfpss3  4055  dfdif3OLD  4084  difeq2  4086  disjne  4421  pssdifcom1  4456  eldifpr  4625  rexsng  4643  elpwunsn  4651  eldiftp  4654  rexprg  4664  preqsnd  4826  disjxun  5108  nalset  5271  dtruALT2  5328  dtruALT  5346  rexxfrd  5367  rexxfr2d  5369  rexxfrd2  5371  rexxfr  5374  dtruOLD  5404  opthneg  5444  snopeqop  5469  otiunsndisj  5483  poeq1  5552  pocl  5557  swopo  5560  sotric  5579  sotrieq  5580  isso2i  5586  somo  5588  freq1  5608  frirr  5617  fr2nr  5618  frminex  5620  tz7.2  5624  wereu2  5638  poinxp  5722  frinxp  5724  posn  5727  frsn  5729  rexiunxp  5807  rexxpf  5814  intirr  6094  poirr2  6100  cnvpo  6263  dfpo2  6272  predpoirr  6309  predfrirr  6310  frpomin  6316  nordeq  6354  ordtri1  6368  ordtri3  6371  fvmpti  6970  fndmdif  7017  rexrnmptw  7070  rexrnmpt  7072  rexima  7215  f1imapss  7244  f1ounsn  7250  cbvexfo  7268  nf1const  7282  soisoi  7306  isopolem  7323  weniso  7332  imaeqsalvOLD  7342  canth  7344  riotaclb  7388  rexrnmpo  7532  ndmovg  7575  sorpssuni  7711  sorpssint  7712  fr3nr  7751  dfwe2  7753  ordsucsssuc  7801  nlimsucg  7821  orduninsuc  7822  dfom2  7847  ssnlim  7865  resf1extb  7913  f1oweALT  7954  frxp  8108  poxp  8110  frxp2  8126  frxp3  8133  xpord3inddlem  8136  soseq  8141  suppofssd  8185  suppcoss  8189  smoword  8338  tz7.48lem  8412  oacan  8515  oaword  8516  omlimcl  8545  omeulem1  8549  nnaword  8594  nnmword  8600  nneob  8623  naddss1  8656  brdifun  8704  swoer  8705  undifixp  8910  boxcutc  8917  2dom  9004  php  9177  phpeqd  9182  nndomog  9183  onomeneq  9184  nnsdomo  9188  unxpdomlem2  9205  frfi  9239  unfilem1  9261  supeq3  9407  supeq123d  9408  supmo  9410  eqsup  9414  supub  9417  sup0  9425  suppr  9430  supisolem  9432  supisoex  9433  eqinf  9443  infval  9445  infmo  9455  infpr  9463  infempty  9467  oieq1  9472  ordtypecbv  9477  ordtypelem7  9484  wemapsolem  9510  canthwdom  9539  zfregcl  9554  elirrv  9556  elirr  9557  noinfep  9620  cantnfp1lem3  9640  ttrcltr  9676  rankr1clem  9780  carden2b  9927  domtri2  9949  alephord3  10038  alephdom2  10047  alephval3  10070  dfac9  10097  kmlem2  10112  kmlem4  10114  isfin4  10257  isfin7  10261  fin23lem11  10277  isf32lem5  10317  isf34lem4  10337  fin1a2lem6  10365  fin1a2lem7  10366  fin1a2lem12  10371  itunisuc  10379  ac6n  10445  zorn2g  10463  zornn0g  10465  ttukeylem7  10475  axpowndlem3  10559  axpowndlem4  10560  axregnd  10564  elgch  10582  engch  10588  fpwwe2lem12  10602  fpwwe2  10603  pwfseqlem1  10618  pwfseqlem3  10620  hargch  10633  addnidpi  10861  pinq  10887  nqereu  10889  ltsonq  10929  prlem934  10993  ltexprlem7  11002  addcanpr  11006  prlem936  11007  reclem2pr  11008  reclem3pr  11009  supexpr  11014  ltsosr  11054  supsrlem  11071  axpre-lttri  11125  axpre-sup  11129  xrlenlt  11246  axlttri  11252  axsup  11256  ltne  11278  dedekind  11344  readdcan  11355  leadd1  11653  ltsub1  11681  ltsub2  11682  leord1  11712  lediv1  12055  lemuldiv  12070  lerec  12073  le2msq  12090  infm3  12149  suprnub  12155  infregelb  12174  avgle1  12429  avgle2  12430  znnnlt1  12567  indstr  12882  zsupss  12903  uzsupss  12906  rpneg  12992  xralrple  13172  xleneg  13185  xltadd1  13223  xposdif  13229  xmulneg1  13236  xltmul1  13259  xrsupexmnf  13272  xrinfmexpnf  13273  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  supxrleub  13293  infxrgelb  13303  difreicc  13452  nn0disj  13612  nelfzo  13632  elfznelfzo  13740  fvinim0ffz  13754  injresinjlem  13755  ssnn0fi  13957  leexp2  14143  exp11nnd  14233  hashbnd  14308  hasheni  14320  hashfundm  14414  hashbc  14425  wrdsymb0  14521  swrdnd  14626  swrdnd2  14627  pfxnd0  14660  repswswrd  14756  repswccat  14758  cshwidxmod  14775  cnpart  15213  sqrtlt  15234  limsuplt  15452  rlimrege0  15552  isercoll  15641  efle  16093  odd2np1  16318  sumodd  16365  divalglem7  16376  ndvdsadd  16387  fldivndvdslt  16393  bitsfval  16400  bitsval  16401  bits0  16405  bitsp1  16408  bitsmod  16413  bitscmp  16415  bitsinv1lem  16418  sadadd2lem2  16427  saddisjlem  16441  bitsshft  16452  gcdneg  16499  algcvgblem  16554  lcmneg  16580  isprm3  16660  dvdsnprmd  16667  isprm5  16684  rpexp  16699  phiprmpw  16753  m1dvdsndvds  16776  pythagtrip  16812  pcgcd1  16855  prmpwdvds  16882  prmreclem2  16895  prmreclem3  16896  prmreclem5  16898  prmreclem6  16899  vdwlem6  16964  vdwnnlem2  16974  vdwnnlem3  16975  vdwnn  16976  prmlem0  17083  prmlem1a  17084  divsfval  17517  mrisval  17598  ismri  17599  ismri2dad  17605  cidpropd  17678  cat1lem  18065  plttr  18308  joinval  18343  meetval  18357  acsfiindd  18519  isnsgrp  18657  smndex1n0mnd  18846  mgm2nsgrplem2  18853  sgrp2nmndlem3  18859  symgpssefmnd  19333  symgfix2  19353  pmtrdifellem4  19416  psgnunilem1  19430  psgnunilem5  19431  psgnunilem2  19432  psgnunilem3  19433  pmtrsn  19456  sylow1lem3  19537  sylow2alem2  19555  efgsfo  19676  ablfac1eulem  20011  ablfac1eu  20012  pgpfac1lem1  20013  pgpfac1lem5  20018  nzrunit  20440  zrninitoringc  20592  islbs  20990  lbsind  20994  lbspss  20996  lbspropd  21013  lspsnne1  21034  islbs2  21071  lbsacsbs  21073  lbsextlem1  21075  lbsextlem3  21077  lbsextlem4  21078  lbsextg  21079  frlmlbs  21713  islindf  21728  islinds2  21729  islindf2  21730  lindfind  21732  lindsind  21733  lindfrn  21737  lindfmm  21743  lsslindf  21746  islindf4  21754  opsrtoslem2  21970  psdmul  22060  cply1coe0  22195  cply1coe0bi  22196  mdetunilem7  22512  mdetunilem8  22513  mdetunilem9  22514  maducoeval2  22534  pmatcollpw3fi1lem1  22680  fvmptnn04ifa  22744  fvmptnn04ifc  22746  fvmptnn04ifd  22747  chfacffsupp  22750  chfacfscmul0  22752  chfacfpmmul0  22756  elcls  22967  maxlp  23041  perfi  23049  ordtbaslem  23082  ordtval  23083  ordtbas2  23085  ordtopn1  23088  ordtopn2  23089  ordtcnv  23095  ordtrest  23096  ordtrest2lem  23097  ordtrest2  23098  pnfnei  23114  mnfnei  23115  isreg2  23271  ordthauslem  23277  cmpfi  23302  cmpfii  23303  bwth  23304  nconnsubb  23317  hausdiag  23539  txkgen  23546  kqdisj  23626  ordthmeolem  23695  fbfinnfr  23735  trfbas  23738  fbunfip  23763  fbasrn  23778  trfil3  23782  ufileu  23813  fin1aufil  23826  hausflim  23875  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem2  23947  ptcmplem3  23948  stdbdbl  24412  iccntr  24717  reconnlem2  24723  iccpnfcnv  24849  xrhmeo  24851  lebnumlem1  24867  lebnumlem2  24868  lebnumlem3  24869  bcthlem4  25234  minveclem3b  25335  ivthlem2  25360  ivthlem3  25361  mbfmax  25557  mbfposr  25560  i1fd  25589  mbfi1fseqlem4  25626  itg2splitlem  25656  itg2monolem1  25658  itg2cnlem1  25669  dvne0  25923  lhop1lem  25925  deg1nn0clb  26002  dgrle  26155  coemulhi  26166  aaliou3lem9  26265  cos11  26449  logleb  26519  argrege0  26527  logdivle  26538  ellogdm  26555  cxple  26611  cxplt2  26614  cxple3  26617  isosctrlem1  26735  atandm  26793  atans2  26848  atantayl2  26855  eldmgm  26939  ftalem7  26996  isppw2  27032  musum  27108  dchrsum2  27186  bposlem1  27202  lgsmod  27241  lgsdir2lem2  27244  lgsdir2  27248  lgsne0  27253  lgsprme0  27257  gausslemma2dlem4  27287  lgsquadlem1  27298  2lgslem3  27322  2lgsoddprm  27334  2sq2  27351  addsqrexnreu  27360  rpvmasumlem  27405  padicabv  27548  ostth3  27556  ostth  27557  noextenddif  27587  nodenselem4  27606  nodenselem5  27607  nodenselem7  27609  nolt02o  27614  nogt01o  27615  noresle  27616  nosupprefixmo  27619  noinfprefixmo  27620  nosupcbv  27621  nosupdm  27623  nosupfv  27625  nosupres  27626  nosupbnd1lem1  27627  nosupbnd1lem3  27629  nosupbnd1lem5  27631  nosupbnd1  27633  nosupbnd2lem1  27634  nosupbnd2  27635  noinfcbv  27636  noinfdm  27638  noinffv  27640  noinfres  27641  noinfbnd1lem1  27642  noinfbnd1lem3  27644  noinfbnd1lem5  27646  noinfbnd1  27648  noinfbnd2lem1  27649  noinfbnd2  27650  slenlt  27671  sltne  27689  nocvxminlem  27696  slerec  27738  cuteq1  27753  newbday  27820  sltlpss  27826  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  istrkgld  28393  axtgupdim2  28405  tglowdim2l  28584  axlowdimlem16  28891  axlowdim2  28894  axlowdim  28895  numedglnl  29078  usgredg2v  29161  lfuhgr1v0e  29188  cusgrfi  29393  vtxd0nedgb  29423  vtxduhgr0edgnel  29429  1loopgrnb0  29437  1hevtxdg0  29440  vtxdgoddnumeven  29488  wlkp1lem1  29608  wlkp1lem2  29609  wlkp1lem5  29612  dfpth2  29666  crctcsh  29761  clwlkclwwlklem2a4  29933  eupth2eucrct  30153  eupth2lem3lem3  30166  eupth2lem3lem4  30167  eupth2lem3lem6  30169  eupth2lem3lem7  30170  eupth2lems  30174  eupth2  30175  konigsberglem4  30191  nfrgr2v  30208  frgrwopreglem3  30250  fusgr2wsp2nb  30270  frgrreggt1  30329  friendshipgt3  30334  lpni  30416  nmobndseqi  30715  minvecolem5  30817  chpsscon3  31439  chnle  31450  nonbooli  31587  pjnel  31662  specval  31834  nmcfnlbi  31988  stri  32193  hstri  32201  cvbr  32218  cvcon3  32220  chcv1  32291  cvexchlem  32304  chrelat2  32306  nelun  32449  elpreq  32464  nelpr  32467  ifeqeqx  32478  nfpconfp  32563  suppiniseg  32616  isoun  32632  suppss3  32654  xrge0infss  32690  infxrge0gelb  32696  eliccelico  32707  elicoelioo  32708  nndiffz1  32716  hashgt1  32740  expgt0b  32748  nn0min  32752  ccatws1f1o  32880  toslublem  32905  tosglblem  32907  pmtrcnel  33053  cycpmco2  33097  isarchi2  33146  archiabl  33159  elrgspnlem2  33201  elrgspnlem3  33202  0nellinds  33348  lindssn  33356  lindfpropd  33360  ssdifidlprm  33436  mxidlirred  33450  ssmxidl  33452  lbslsat  33619  lindsunlem  33627  rtelextdg2lem  33723  constrsqrtcl  33776  ordtcnvNEW  33917  ordtrestNEW  33918  ordtrest2NEWlem  33919  ordtrest2NEW  33920  ordtconnlem1  33921  xrge0iifcnv  33930  esumpcvgval  34075  esum2d  34090  ddemeas  34233  omssubadd  34298  oddpwdc  34352  eulerpartlems  34358  eulerpartlemf  34368  eulerpartlemt  34369  eulerpartlemr  34372  eulerpartlemgvv  34374  eulerpartlemn  34379  ballotlemfc0  34491  ballotlemfcc  34492  ballotlem4  34497  ballotlemimin  34504  ballotlem7  34534  plymulx  34546  signsply0  34549  reprinfz1  34620  reprpmtf1o  34624  reprdifc  34625  hgt750lema  34655  hgt750leme  34656  istrkg2d  34664  bnj23  34715  bnj1185  34790  bnj1228  35008  bnj1388  35030  bnj1417  35038  nummin  35088  axnulg  35089  onvf1odlem2  35098  onvf1odlem3  35099  revwlk  35119  isacycgr  35139  acycgr0v  35142  prclisacycgr  35145  erdszelem10  35194  satf0n0  35372  fmlaomn0  35384  fmlasucdisj  35393  satfv1fvfmla1  35417  satefvfmla1  35419  ismfs  35543  mvtinf  35549  untelirr  35702  untsucf  35704  untangtr  35708  dfon2lem3  35780  dfon2lem4  35781  dfon2lem7  35784  dfon2lem9  35786  distel  35798  funpartfv  35940  dfrdg4  35946  nn0prpwlem  36317  nn0prpw  36318  limsucncmpi  36440  limsucncmp  36441  ordcmp  36442  weiunlem2  36458  weiunfrlem  36459  weiunfr  36462  unblimceq0  36502  unbdqndv1  36503  bj-hbntbi  36699  bj-equsexvwd  36776  bj-cbvexdv  36795  bj-ru1  36938  bj-nuliota  37052  topdifinffinlem  37342  topdifinffin  37343  icorempo  37346  relowlpssretop  37359  finxpreclem2  37385  finxpreclem6  37391  wl-issetft  37577  wl-ax11-lem8  37587  leceifl  37610  lindsadd  37614  lindsenlbs  37616  matunitlindflem1  37617  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem21  37642  poimirlem23  37644  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem31  37652  poimir  37654  mblfinlem2  37659  mblfinlem3  37660  ismblfin  37662  cnambfre  37669  itg2addnclem  37672  itg2addnclem2  37673  iblabsnclem  37684  ftc1anclem1  37694  areacirc  37714  heibor1lem  37810  heiborlem1  37812  heiborlem6  37817  heiborlem8  37819  heiborlem10  37821  smprngopr  38053  ecin0  38341  ax12inda  38948  riotaclbgBAD  38954  lcvfbr  39020  lcvbr  39021  lsatcv0  39031  l1cvpat  39054  opltcon3b  39204  cvrfval  39268  cvrval  39269  cvrnbtwn  39271  cvrval2  39274  cvrnbtwn2  39275  cvrnbtwn3  39276  cvrcon3b  39277  cvrnbtwn4  39279  atnlt  39313  iscvlat  39323  cvlexch1  39328  hlsuprexch  39382  hlrelat5N  39402  hlrelat2  39404  cvrval5  39416  3dimlem1  39459  3dim1lem5  39467  3dim2  39469  3dim3  39470  llnnlt  39524  islpln5  39536  lplni2  39538  lvolex3N  39539  lplnnle2at  39542  islpln2a  39549  lplnribN  39552  lplnexllnN  39565  lplnnlt  39566  lvoli3  39578  islvol5  39580  lvoli2  39582  lvolnle3at  39583  islvol2aN  39593  4atlem11  39610  lvolnltN  39619  dalawlem15  39886  4atexlemex2  40072  4atex  40077  4atex2-0aOLDN  40079  4atex2-0cOLDN  40081  lautcvr  40093  ltrnfset  40118  ltrnset  40119  ltrnu  40122  trlfset  40161  trlset  40162  trlval2  40164  cdlemd6  40204  cdleme0nex  40291  cdleme18d  40296  cdleme25b  40355  cdleme25cv  40359  cdleme29b  40376  cdleme31fv  40391  cdleme31fv2  40394  cdlemefrs29bpre0  40397  cdlemefr32sn2aw  40405  cdlemefr29bpre0N  40407  cdlemefr29clN  40408  cdlemefr32fvaN  40410  cdlemefr32fva1  40411  cdlemefs32sn1aw  40415  cdleme32fva  40438  cdleme32fvaw  40440  cdleme40v  40470  cdleme42b  40479  cdleme46f2g2  40494  cdleme46f2g1  40495  cdleme48gfv  40538  cdlemg1fvawlemN  40574  cdlemg1cex  40589  cdlemg6d  40622  cdlemm10N  41119  dicffval  41175  dicfval  41176  dicval  41177  dicfnN  41184  dicvalrelN  41186  dihffval  41231  dihfval  41232  dihlsscpre  41235  dvh4dimat  41439  dvh3dimatN  41440  dvh4dimlem  41444  dvh3dim  41447  dvh4dimN  41448  dvh3dim2  41449  dvh3dim3N  41450  mapdcv  41661  mapdh9aOLDN  41791  hdmapfval  41828  hdmapval  41829  hdmapval2  41833  hdmap11lem2  41843  dvrelog2b  42061  aks4d1p4  42074  aks4d1p5  42075  aks4d1p7  42078  aks4d1p8d2  42080  aks4d1p8  42082  aks4d1  42084  aks6d1c2p2  42114  hashnexinj  42123  rspcsbnea  42126  aks6d1c5  42134  aks6d1c6lem3  42167  aks6d1c7  42179  supinf  42237  oexpreposd  42317  mullt0b2d  42479  flt4lem7  42654  nna4b4nsq  42655  ellz1  42762  rencldnfilem  42815  jm2.22  42991  jm2.23  42992  wepwsolem  43038  fnwe2lem2  43047  aomclem8  43057  unxpwdom3  43091  onsupmaxb  43235  onexlimgt  43239  onsupeqnmax  43243  onov0suclim  43270  oaordnr  43292  omnord1  43301  oenord1  43312  oaomoencom  43313  oenass  43315  cantnfresb  43320  tfsnfin  43348  ralopabb  43407  nlimsuc  43437  ifpbi12  43484  dfsucon  43519  sqrtcvallem1  43627  ss2iundf  43655  frege124d  43757  clsk3nimkb  44036  clsk1indlem1  44041  clsk1independent  44042  ntrneineine1lem  44080  ntrneicls11  44086  clsneiel1  44104  clsneiel2  44105  neicvgel1  44115  neicvgel2  44116  radcnvrat  44310  rusbcALT  44435  en3lpVD  44841  0elaxnul  44980  omssaxinf2  44985  permaxnul  45005  permaxinf2lem  45009  nregmodel  45014  eliin2f  45105  nssd  45106  wessf1ornlem  45186  rexanuz2nf  45495  limsupre2lem  45729  icccncfext  45892  stoweidlem14  46019  stoweidlem34  46039  stoweidlem59  46064  etransclem24  46263  nnfoctbdjlem  46460  nnfoctbdj  46461  hspmbllem2  46632  nsssmfmbflem  46783  fsetsnprcnex  47060  eu2ndop1stv  47130  afvfv0bi  47157  afvco2  47181  ndmaovg  47189  ndfatafv2nrn  47226  afv2ndefb  47229  afv2fv0  47270  nelbr  47279  otiunsndisjX  47284  fun2dmnopgexmpl  47289  ltnltne  47304  readdcnnred  47308  resubcnnred  47309  recnmulnred  47310  cndivrenred  47311  ichnreuop  47477  fmtnoinf  47541  odz2prm2pw  47568  prmdvdsfmtnof1lem2  47590  lighneallem3  47612  lighneallem4  47615  requad1  47627  isodd3  47657  bits0ALTV  47684  nfermltl8rev  47747  nfermltl2rev  47748  nfermltlrev  47749  upgrimpths  47913  isubgr3stgrlem3  47971  usgrexmpl12ngric  48033  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  lgricngricex  48123  lidldomnnring  48228  ztprmneprm  48339  lindepsnlininds  48445  islindeps  48446  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  line2ylem  48744  line2xlem  48746  map0cor  48847  nelsubc3lem  49063  fulltermc2  49505  setc1onsubc  49595  cnelsubclem  49596  elsetrecslem  49692