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  1526  equsexvw  2006  cbvexvw  2038  cbvexdvaw  2040  excomimw  2045  hbe1w  2051  19.8aw  2053  exexw  2054  ru0  2130  cbvexv1  2342  cbvex2v  2344  drex1v  2370  cbvex  2399  cbvex2  2412  drex1  2441  eujustALT  2567  necon3abid  2964  neleq12d  3037  cbvrexdva  3213  cbvrexfw  3273  rexeqbidvvOLD  3303  cbvrexdva2  3315  cbvrexf  3327  cbvexeqsetf  3451  cgsex4gOLD  3484  ceqsex  3485  ceqsexv  3486  gencbval  3497  spcegf  3542  spc2gv  3550  spc2d  3552  spc3gv  3554  ceqsralbv  3607  cdeqnot  3722  rru  3733  ruOLD  3735  sbcng  3784  sbcrext  3819  cbvrexcsf  3888  difjust  3899  eldif  3907  dfpss3  4036  dfdif3OLD  4065  difeq2  4067  disjne  4402  pssdifcom1  4437  eldifpr  4608  rexsng  4626  elpwunsn  4634  eldiftp  4637  rexprg  4647  preqsnd  4808  disjxun  5087  nalset  5249  dtruALT2  5306  dtruALT  5324  rexxfrd  5345  rexxfr2d  5347  rexxfrd2  5349  rexxfr  5352  opthneg  5419  snopeqop  5444  otiunsndisj  5458  poeq1  5525  pocl  5530  swopo  5533  sotric  5552  sotrieq  5553  isso2i  5559  somo  5561  freq1  5581  frirr  5590  fr2nr  5591  frminex  5593  tz7.2  5597  wereu2  5611  poinxp  5695  frinxp  5697  posn  5700  frsn  5702  rexiunxp  5779  rexxpf  5786  intirr  6064  poirr2  6070  cnvpo  6234  dfpo2  6243  predpoirr  6280  predfrirr  6281  frpomin  6287  nordeq  6325  ordtri1  6339  ordtri3  6342  fvmpti  6928  fndmdif  6975  rexrnmptw  7028  rexrnmpt  7030  rexima  7172  f1imapss  7200  f1ounsn  7206  cbvexfo  7224  nf1const  7238  soisoi  7262  isopolem  7279  weniso  7288  imaeqsalvOLD  7298  canth  7300  riotaclb  7344  rexrnmpo  7486  ndmovg  7529  sorpssuni  7665  sorpssint  7666  fr3nr  7705  dfwe2  7707  ordsucsssuc  7753  nlimsucg  7772  orduninsuc  7773  dfom2  7798  ssnlim  7816  resf1extb  7864  f1oweALT  7904  frxp  8056  poxp  8058  frxp2  8074  frxp3  8081  xpord3inddlem  8084  soseq  8089  suppofssd  8133  suppcoss  8137  smoword  8286  tz7.48lem  8360  oacan  8463  oaword  8464  omlimcl  8493  omeulem1  8497  nnaword  8542  nnmword  8548  nneob  8571  naddss1  8604  brdifun  8652  swoer  8653  undifixp  8858  boxcutc  8865  2dom  8952  php  9116  phpeqd  9121  nndomog  9122  onomeneq  9123  nnsdomo  9127  unxpdomlem2  9141  frfi  9169  unfilem1  9189  supeq3  9333  supeq123d  9334  supmo  9336  eqsup  9340  supub  9343  sup0  9351  suppr  9356  supisolem  9358  supisoex  9359  eqinf  9369  infval  9371  infmo  9381  infpr  9389  infempty  9393  oieq1  9398  ordtypecbv  9403  ordtypelem7  9410  wemapsolem  9436  canthwdom  9465  zfregcl  9480  zfregclOLD  9481  elirrv  9483  elirrvOLD  9484  elirr  9485  noinfep  9550  cantnfp1lem3  9570  ttrcltr  9606  rankr1clem  9713  carden2b  9860  domtri2  9882  alephord3  9969  alephdom2  9978  alephval3  10001  dfac9  10028  kmlem2  10043  kmlem4  10045  isfin4  10188  isfin7  10192  fin23lem11  10208  isf32lem5  10248  isf34lem4  10268  fin1a2lem6  10296  fin1a2lem7  10297  fin1a2lem12  10302  itunisuc  10310  ac6n  10376  zorn2g  10394  zornn0g  10396  ttukeylem7  10406  axpowndlem3  10490  axpowndlem4  10491  axregnd  10495  elgch  10513  engch  10519  fpwwe2lem12  10533  fpwwe2  10534  pwfseqlem1  10549  pwfseqlem3  10551  hargch  10564  addnidpi  10792  pinq  10818  nqereu  10820  ltsonq  10860  prlem934  10924  ltexprlem7  10933  addcanpr  10937  prlem936  10938  reclem2pr  10939  reclem3pr  10940  supexpr  10945  ltsosr  10985  supsrlem  11002  axpre-lttri  11056  axpre-sup  11060  xrlenlt  11177  axlttri  11184  axsup  11188  ltne  11210  dedekind  11276  readdcan  11287  leadd1  11585  ltsub1  11613  ltsub2  11614  leord1  11644  lediv1  11987  lemuldiv  12002  lerec  12005  le2msq  12022  infm3  12081  suprnub  12087  infregelb  12106  avgle1  12361  avgle2  12362  znnnlt1  12499  indstr  12814  zsupss  12835  uzsupss  12838  rpneg  12924  xralrple  13104  xleneg  13117  xltadd1  13155  xposdif  13161  xmulneg1  13168  xltmul1  13191  xrsupexmnf  13204  xrinfmexpnf  13205  xrsupsslem  13206  xrinfmsslem  13207  xrub  13211  supxrleub  13225  infxrgelb  13235  difreicc  13384  nn0disj  13544  nelfzo  13564  elfznelfzo  13673  fvinim0ffz  13689  injresinjlem  13690  ssnn0fi  13892  leexp2  14078  exp11nnd  14168  hashbnd  14243  hasheni  14255  hashfundm  14349  hashbc  14360  wrdsymb0  14456  swrdnd  14562  swrdnd2  14563  pfxnd0  14596  repswswrd  14691  repswccat  14693  cshwidxmod  14710  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  18631  smndex1n0mnd  18820  mgm2nsgrplem2  18827  sgrp2nmndlem3  18833  symgpssefmnd  19308  symgfix2  19328  pmtrdifellem4  19391  psgnunilem1  19405  psgnunilem5  19406  psgnunilem2  19407  psgnunilem3  19408  pmtrsn  19431  sylow1lem3  19512  sylow2alem2  19530  efgsfo  19651  ablfac1eulem  19986  ablfac1eu  19987  pgpfac1lem1  19988  pgpfac1lem5  19993  nzrunit  20439  zrninitoringc  20591  islbs  21010  lbsind  21014  lbspss  21016  lbspropd  21033  lspsnne1  21054  islbs2  21091  lbsacsbs  21093  lbsextlem1  21095  lbsextlem3  21097  lbsextlem4  21098  lbsextg  21099  frlmlbs  21734  islindf  21749  islinds2  21750  islindf2  21751  lindfind  21753  lindsind  21754  lindfrn  21758  lindfmm  21764  lsslindf  21767  islindf4  21775  opsrtoslem2  21991  psdmul  22081  cply1coe0  22216  cply1coe0bi  22217  mdetunilem7  22533  mdetunilem8  22534  mdetunilem9  22535  maducoeval2  22555  pmatcollpw3fi1lem1  22701  fvmptnn04ifa  22765  fvmptnn04ifc  22767  fvmptnn04ifd  22768  chfacffsupp  22771  chfacfscmul0  22773  chfacfpmmul0  22777  elcls  22988  maxlp  23062  perfi  23070  ordtbaslem  23103  ordtval  23104  ordtbas2  23106  ordtopn1  23109  ordtopn2  23110  ordtcnv  23116  ordtrest  23117  ordtrest2lem  23118  ordtrest2  23119  pnfnei  23135  mnfnei  23136  isreg2  23292  ordthauslem  23298  cmpfi  23323  cmpfii  23324  bwth  23325  nconnsubb  23338  hausdiag  23560  txkgen  23567  kqdisj  23647  ordthmeolem  23716  fbfinnfr  23756  trfbas  23759  fbunfip  23784  fbasrn  23799  trfil3  23803  ufileu  23834  fin1aufil  23847  hausflim  23896  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  ptcmplem2  23968  ptcmplem3  23969  stdbdbl  24432  iccntr  24737  reconnlem2  24743  iccpnfcnv  24869  xrhmeo  24871  lebnumlem1  24887  lebnumlem2  24888  lebnumlem3  24889  bcthlem4  25254  minveclem3b  25355  ivthlem2  25380  ivthlem3  25381  mbfmax  25577  mbfposr  25580  i1fd  25609  mbfi1fseqlem4  25646  itg2splitlem  25676  itg2monolem1  25678  itg2cnlem1  25689  dvne0  25943  lhop1lem  25945  deg1nn0clb  26022  dgrle  26175  coemulhi  26186  aaliou3lem9  26285  cos11  26469  logleb  26539  argrege0  26547  logdivle  26558  ellogdm  26575  cxple  26631  cxplt2  26634  cxple3  26637  isosctrlem1  26755  atandm  26813  atans2  26868  atantayl2  26875  eldmgm  26959  ftalem7  27016  isppw2  27052  musum  27128  dchrsum2  27206  bposlem1  27222  lgsmod  27261  lgsdir2lem2  27264  lgsdir2  27268  lgsne0  27273  lgsprme0  27277  gausslemma2dlem4  27307  lgsquadlem1  27318  2lgslem3  27342  2lgsoddprm  27354  2sq2  27371  addsqrexnreu  27380  rpvmasumlem  27425  padicabv  27568  ostth3  27576  ostth  27577  noextenddif  27607  nodenselem4  27626  nodenselem5  27627  nodenselem7  27629  nolt02o  27634  nogt01o  27635  noresle  27636  nosupprefixmo  27639  noinfprefixmo  27640  nosupcbv  27641  nosupdm  27643  nosupfv  27645  nosupres  27646  nosupbnd1lem1  27647  nosupbnd1lem3  27649  nosupbnd1lem5  27651  nosupbnd1  27653  nosupbnd2lem1  27654  nosupbnd2  27655  noinfcbv  27656  noinfdm  27658  noinffv  27660  noinfres  27661  noinfbnd1lem1  27662  noinfbnd1lem3  27664  noinfbnd1lem5  27666  noinfbnd1  27668  noinfbnd2lem1  27669  noinfbnd2  27670  slenlt  27691  sltne  27709  nocvxminlem  27717  slerec  27760  eqscut3  27765  cuteq1  27778  newbday  27847  sltlpss  27853  cofcutr  27868  lrrecfr  27886  addsval  27905  sltadd2  27934  sleneg  27988  slesubsubbd  28026  slesubsub2bd  28027  slesubsub3bd  28028  slesubaddd  28033  sltmul2  28110  slemul2d  28113  slemul1d  28114  onscutlt  28201  pw2cut2  28382  istrkgld  28437  axtgupdim2  28449  tglowdim2l  28628  axlowdimlem16  28935  axlowdim2  28938  axlowdim  28939  numedglnl  29122  usgredg2v  29205  lfuhgr1v0e  29232  cusgrfi  29437  vtxd0nedgb  29467  vtxduhgr0edgnel  29473  1loopgrnb0  29481  1hevtxdg0  29484  vtxdgoddnumeven  29532  wlkp1lem1  29650  wlkp1lem2  29651  wlkp1lem5  29654  dfpth2  29707  crctcsh  29802  clwlkclwwlklem2a4  29977  eupth2eucrct  30197  eupth2lem3lem3  30210  eupth2lem3lem4  30211  eupth2lem3lem6  30213  eupth2lem3lem7  30214  eupth2lems  30218  eupth2  30219  konigsberglem4  30235  nfrgr2v  30252  frgrwopreglem3  30294  fusgr2wsp2nb  30314  frgrreggt1  30373  friendshipgt3  30378  lpni  30460  nmobndseqi  30759  minvecolem5  30861  chpsscon3  31483  chnle  31494  nonbooli  31631  pjnel  31706  specval  31878  nmcfnlbi  32032  stri  32237  hstri  32245  cvbr  32262  cvcon3  32264  chcv1  32335  cvexchlem  32348  chrelat2  32350  nelun  32493  elpreq  32508  nelpr  32511  ifeqeqx  32522  nfpconfp  32614  suppiniseg  32667  isoun  32683  suppss3  32706  xrge0infss  32743  infxrge0gelb  32749  eliccelico  32760  elicoelioo  32761  nndiffz1  32769  hashgt1  32790  expgt0b  32799  nn0min  32803  ccatws1f1o  32932  toslublem  32953  tosglblem  32955  pmtrcnel  33058  cycpmco2  33102  isarchi2  33154  archiabl  33167  elrgspnlem2  33210  elrgspnlem3  33211  0nellinds  33335  lindssn  33343  lindfpropd  33347  ssdifidlprm  33423  mxidlirred  33437  ssmxidl  33439  lbslsat  33629  lindsunlem  33637  rtelextdg2lem  33739  constrsqrtcl  33792  ordtcnvNEW  33933  ordtrestNEW  33934  ordtrest2NEWlem  33935  ordtrest2NEW  33936  ordtconnlem1  33937  xrge0iifcnv  33946  esumpcvgval  34091  esum2d  34106  ddemeas  34249  omssubadd  34313  oddpwdc  34367  eulerpartlems  34373  eulerpartlemf  34383  eulerpartlemt  34384  eulerpartlemr  34387  eulerpartlemgvv  34389  eulerpartlemn  34394  ballotlemfc0  34506  ballotlemfcc  34507  ballotlem4  34512  ballotlemimin  34519  ballotlem7  34549  plymulx  34561  signsply0  34564  reprinfz1  34635  reprpmtf1o  34639  reprdifc  34640  hgt750lema  34670  hgt750leme  34671  istrkg2d  34679  bnj23  34730  bnj1185  34805  bnj1228  35023  bnj1388  35045  bnj1417  35053  nummin  35104  axnulg  35119  fineqvnttrclselem1  35141  onvf1odlem2  35148  onvf1odlem3  35149  revwlk  35169  isacycgr  35189  acycgr0v  35192  prclisacycgr  35195  erdszelem10  35244  satf0n0  35422  fmlaomn0  35434  fmlasucdisj  35443  satfv1fvfmla1  35467  satefvfmla1  35469  ismfs  35593  mvtinf  35599  untelirr  35752  untsucf  35754  untangtr  35758  dfon2lem3  35827  dfon2lem4  35828  dfon2lem7  35831  dfon2lem9  35833  distel  35845  funpartfv  35989  dfrdg4  35995  nn0prpwlem  36366  nn0prpw  36367  limsucncmpi  36489  limsucncmp  36490  ordcmp  36491  weiunlem2  36507  weiunfrlem  36508  weiunfr  36511  unblimceq0  36551  unbdqndv1  36552  bj-hbntbi  36748  bj-equsexvwd  36825  bj-cbvexdv  36844  bj-ru1  36987  bj-nuliota  37101  topdifinffinlem  37391  topdifinffin  37392  icorempo  37395  relowlpssretop  37408  finxpreclem2  37434  finxpreclem6  37440  wl-issetft  37626  leceifl  37648  lindsadd  37652  lindsenlbs  37654  matunitlindflem1  37655  poimirlem16  37675  poimirlem17  37676  poimirlem18  37677  poimirlem19  37678  poimirlem21  37680  poimirlem23  37682  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  poimirlem31  37690  poimir  37692  mblfinlem2  37697  mblfinlem3  37698  ismblfin  37700  cnambfre  37707  itg2addnclem  37710  itg2addnclem2  37711  iblabsnclem  37722  ftc1anclem1  37732  areacirc  37752  heibor1lem  37848  heiborlem1  37850  heiborlem6  37855  heiborlem8  37857  heiborlem10  37859  smprngopr  38091  ecin0  38383  ax12inda  39046  riotaclbgBAD  39052  lcvfbr  39118  lcvbr  39119  lsatcv0  39129  l1cvpat  39152  opltcon3b  39302  cvrfval  39366  cvrval  39367  cvrnbtwn  39369  cvrval2  39372  cvrnbtwn2  39373  cvrnbtwn3  39374  cvrcon3b  39375  cvrnbtwn4  39377  atnlt  39411  iscvlat  39421  cvlexch1  39426  hlsuprexch  39479  hlrelat5N  39499  hlrelat2  39501  cvrval5  39513  3dimlem1  39556  3dim1lem5  39564  3dim2  39566  3dim3  39567  llnnlt  39621  islpln5  39633  lplni2  39635  lvolex3N  39636  lplnnle2at  39639  islpln2a  39646  lplnribN  39649  lplnexllnN  39662  lplnnlt  39663  lvoli3  39675  islvol5  39677  lvoli2  39679  lvolnle3at  39680  islvol2aN  39690  4atlem11  39707  lvolnltN  39716  dalawlem15  39983  4atexlemex2  40169  4atex  40174  4atex2-0aOLDN  40176  4atex2-0cOLDN  40178  lautcvr  40190  ltrnfset  40215  ltrnset  40216  ltrnu  40219  trlfset  40258  trlset  40259  trlval2  40261  cdlemd6  40301  cdleme0nex  40388  cdleme18d  40393  cdleme25b  40452  cdleme25cv  40456  cdleme29b  40473  cdleme31fv  40488  cdleme31fv2  40491  cdlemefrs29bpre0  40494  cdlemefr32sn2aw  40502  cdlemefr29bpre0N  40504  cdlemefr29clN  40505  cdlemefr32fvaN  40507  cdlemefr32fva1  40508  cdlemefs32sn1aw  40512  cdleme32fva  40535  cdleme32fvaw  40537  cdleme40v  40567  cdleme42b  40576  cdleme46f2g2  40591  cdleme46f2g1  40592  cdleme48gfv  40635  cdlemg1fvawlemN  40671  cdlemg1cex  40686  cdlemg6d  40719  cdlemm10N  41216  dicffval  41272  dicfval  41273  dicval  41274  dicfnN  41281  dicvalrelN  41283  dihffval  41328  dihfval  41329  dihlsscpre  41332  dvh4dimat  41536  dvh3dimatN  41537  dvh4dimlem  41541  dvh3dim  41544  dvh4dimN  41545  dvh3dim2  41546  dvh3dim3N  41547  mapdcv  41758  mapdh9aOLDN  41888  hdmapfval  41925  hdmapval  41926  hdmapval2  41930  hdmap11lem2  41940  dvrelog2b  42158  aks4d1p4  42171  aks4d1p5  42172  aks4d1p7  42175  aks4d1p8d2  42177  aks4d1p8  42179  aks4d1  42181  aks6d1c2p2  42211  hashnexinj  42220  rspcsbnea  42223  aks6d1c5  42231  aks6d1c6lem3  42264  aks6d1c7  42276  supinf  42334  oexpreposd  42414  mullt0b2d  42576  flt4lem7  42751  nna4b4nsq  42752  ellz1  42859  rencldnfilem  42912  jm2.22  43087  jm2.23  43088  wepwsolem  43134  fnwe2lem2  43143  aomclem8  43153  unxpwdom3  43187  onsupmaxb  43331  onexlimgt  43335  onsupeqnmax  43339  onov0suclim  43366  oaordnr  43388  omnord1  43397  oenord1  43408  oaomoencom  43409  oenass  43411  cantnfresb  43416  tfsnfin  43444  ralopabb  43503  nlimsuc  43533  ifpbi12  43580  dfsucon  43615  sqrtcvallem1  43723  ss2iundf  43751  frege124d  43853  clsk3nimkb  44132  clsk1indlem1  44137  clsk1independent  44138  ntrneineine1lem  44176  ntrneicls11  44182  clsneiel1  44200  clsneiel2  44201  neicvgel1  44211  neicvgel2  44212  radcnvrat  44406  rusbcALT  44530  en3lpVD  44936  0elaxnul  45075  omssaxinf2  45080  permaxnul  45100  permaxinf2lem  45104  nregmodel  45109  eliin2f  45200  nssd  45201  wessf1ornlem  45281  rexanuz2nf  45589  limsupre2lem  45821  icccncfext  45984  stoweidlem14  46111  stoweidlem34  46131  stoweidlem59  46156  etransclem24  46355  nnfoctbdjlem  46552  nnfoctbdj  46553  hspmbllem2  46724  nsssmfmbflem  46875  fsetsnprcnex  47154  eu2ndop1stv  47224  afvfv0bi  47251  afvco2  47275  ndmaovg  47283  ndfatafv2nrn  47320  afv2ndefb  47323  afv2fv0  47364  nelbr  47373  otiunsndisjX  47378  fun2dmnopgexmpl  47383  ltnltne  47398  readdcnnred  47402  resubcnnred  47403  recnmulnred  47404  cndivrenred  47405  ichnreuop  47571  fmtnoinf  47635  odz2prm2pw  47662  prmdvdsfmtnof1lem2  47684  lighneallem3  47706  lighneallem4  47709  requad1  47721  isodd3  47751  bits0ALTV  47778  nfermltl8rev  47841  nfermltl2rev  47842  nfermltlrev  47843  upgrimpths  48008  isubgr3stgrlem3  48067  usgrexmpl12ngric  48137  pgnbgreunbgrlem2lem1  48213  pgnbgreunbgrlem2lem2  48214  pgnbgreunbgrlem2lem3  48215  pgnbgreunbgrlem5lem1  48219  pgnbgreunbgrlem5lem2  48220  pgnbgreunbgrlem5lem3  48221  lgricngricex  48228  lidldomnnring  48335  ztprmneprm  48446  lindepsnlininds  48552  islindeps  48553  lindslinindsimp2lem5  48562  lindslinindsimp2  48563  line2ylem  48851  line2xlem  48853  map0cor  48954  nelsubc3lem  49170  fulltermc2  49612  setc1onsubc  49702  cnelsubclem  49703  elsetrecslem  49799