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  3448  cgsex4gOLD  3481  ceqsex  3482  ceqsexv  3484  gencbval  3495  spcegf  3544  spc2gv  3552  spc2d  3554  spc3gv  3556  ceqsralbv  3609  cdeqnot  3724  rru  3735  ruOLD  3737  sbcng  3786  sbcrext  3821  cbvrexcsf  3890  difjust  3901  eldif  3909  dfpss3  4036  dfdif3OLD  4065  difeq2  4067  disjne  4402  pssdifcom1  4437  eldifpr  4608  rexsng  4626  elpwunsn  4634  eldiftp  4637  rexprg  4647  preqsnd  4808  disjxun  5086  nalset  5248  dtruALT2  5305  dtruALT  5323  rexxfrd  5344  rexxfr2d  5346  rexxfrd2  5348  rexxfr  5351  opthneg  5418  snopeqop  5443  otiunsndisj  5457  poeq1  5524  pocl  5529  swopo  5532  sotric  5551  sotrieq  5552  isso2i  5558  somo  5560  freq1  5580  frirr  5589  fr2nr  5590  frminex  5592  tz7.2  5596  wereu2  5610  poinxp  5694  frinxp  5696  posn  5699  frsn  5701  rexiunxp  5777  rexxpf  5784  intirr  6061  poirr2  6067  cnvpo  6229  dfpo2  6238  predpoirr  6275  predfrirr  6276  frpomin  6282  nordeq  6320  ordtri1  6334  ordtri3  6337  fvmpti  6922  fndmdif  6969  rexrnmptw  7022  rexrnmpt  7024  rexima  7166  f1imapss  7194  f1ounsn  7200  cbvexfo  7218  nf1const  7232  soisoi  7256  isopolem  7273  weniso  7282  imaeqsalvOLD  7292  canth  7294  riotaclb  7338  rexrnmpo  7480  ndmovg  7523  sorpssuni  7659  sorpssint  7660  fr3nr  7699  dfwe2  7701  ordsucsssuc  7747  nlimsucg  7766  orduninsuc  7767  dfom2  7792  ssnlim  7810  resf1extb  7858  f1oweALT  7898  frxp  8050  poxp  8052  frxp2  8068  frxp3  8075  xpord3inddlem  8078  soseq  8083  suppofssd  8127  suppcoss  8131  smoword  8280  tz7.48lem  8354  oacan  8457  oaword  8458  omlimcl  8487  omeulem1  8491  nnaword  8536  nnmword  8542  nneob  8565  naddss1  8598  brdifun  8646  swoer  8647  undifixp  8852  boxcutc  8859  2dom  8946  php  9110  phpeqd  9115  nndomog  9116  onomeneq  9117  nnsdomo  9121  unxpdomlem2  9135  frfi  9163  unfilem1  9183  supeq3  9327  supeq123d  9328  supmo  9330  eqsup  9334  supub  9337  sup0  9345  suppr  9350  supisolem  9352  supisoex  9353  eqinf  9363  infval  9365  infmo  9375  infpr  9383  infempty  9387  oieq1  9392  ordtypecbv  9397  ordtypelem7  9404  wemapsolem  9430  canthwdom  9459  zfregcl  9474  zfregclOLD  9475  elirrv  9477  elirrvOLD  9478  elirr  9479  noinfep  9544  cantnfp1lem3  9564  ttrcltr  9600  rankr1clem  9704  carden2b  9851  domtri2  9873  alephord3  9960  alephdom2  9969  alephval3  9992  dfac9  10019  kmlem2  10034  kmlem4  10036  isfin4  10179  isfin7  10183  fin23lem11  10199  isf32lem5  10239  isf34lem4  10259  fin1a2lem6  10287  fin1a2lem7  10288  fin1a2lem12  10293  itunisuc  10301  ac6n  10367  zorn2g  10385  zornn0g  10387  ttukeylem7  10397  axpowndlem3  10481  axpowndlem4  10482  axregnd  10486  elgch  10504  engch  10510  fpwwe2lem12  10524  fpwwe2  10525  pwfseqlem1  10540  pwfseqlem3  10542  hargch  10555  addnidpi  10783  pinq  10809  nqereu  10811  ltsonq  10851  prlem934  10915  ltexprlem7  10924  addcanpr  10928  prlem936  10929  reclem2pr  10930  reclem3pr  10931  supexpr  10936  ltsosr  10976  supsrlem  10993  axpre-lttri  11047  axpre-sup  11051  xrlenlt  11168  axlttri  11175  axsup  11179  ltne  11201  dedekind  11267  readdcan  11278  leadd1  11576  ltsub1  11604  ltsub2  11605  leord1  11635  lediv1  11978  lemuldiv  11993  lerec  11996  le2msq  12013  infm3  12072  suprnub  12078  infregelb  12097  avgle1  12352  avgle2  12353  znnnlt1  12490  indstr  12805  zsupss  12826  uzsupss  12829  rpneg  12915  xralrple  13095  xleneg  13108  xltadd1  13146  xposdif  13152  xmulneg1  13159  xltmul1  13182  xrsupexmnf  13195  xrinfmexpnf  13196  xrsupsslem  13197  xrinfmsslem  13198  xrub  13202  supxrleub  13216  infxrgelb  13226  difreicc  13375  nn0disj  13535  nelfzo  13555  elfznelfzo  13663  fvinim0ffz  13677  injresinjlem  13678  ssnn0fi  13880  leexp2  14066  exp11nnd  14156  hashbnd  14231  hasheni  14243  hashfundm  14337  hashbc  14348  wrdsymb0  14444  swrdnd  14549  swrdnd2  14550  pfxnd0  14583  repswswrd  14678  repswccat  14680  cshwidxmod  14697  cnpart  15134  sqrtlt  15155  limsuplt  15373  rlimrege0  15473  isercoll  15562  efle  16014  odd2np1  16239  sumodd  16286  divalglem7  16297  ndvdsadd  16308  fldivndvdslt  16314  bitsfval  16321  bitsval  16322  bits0  16326  bitsp1  16329  bitsmod  16334  bitscmp  16336  bitsinv1lem  16339  sadadd2lem2  16348  saddisjlem  16362  bitsshft  16373  gcdneg  16420  algcvgblem  16475  lcmneg  16501  isprm3  16581  dvdsnprmd  16588  isprm5  16605  rpexp  16620  phiprmpw  16674  m1dvdsndvds  16697  pythagtrip  16733  pcgcd1  16776  prmpwdvds  16803  prmreclem2  16816  prmreclem3  16817  prmreclem5  16819  prmreclem6  16820  vdwlem6  16885  vdwnnlem2  16895  vdwnnlem3  16896  vdwnn  16897  prmlem0  17004  prmlem1a  17005  divsfval  17438  mrisval  17523  ismri  17524  ismri2dad  17530  cidpropd  17603  cat1lem  17990  plttr  18233  joinval  18268  meetval  18282  acsfiindd  18446  isnsgrp  18584  smndex1n0mnd  18773  mgm2nsgrplem2  18780  sgrp2nmndlem3  18786  symgpssefmnd  19262  symgfix2  19282  pmtrdifellem4  19345  psgnunilem1  19359  psgnunilem5  19360  psgnunilem2  19361  psgnunilem3  19362  pmtrsn  19385  sylow1lem3  19466  sylow2alem2  19484  efgsfo  19605  ablfac1eulem  19940  ablfac1eu  19941  pgpfac1lem1  19942  pgpfac1lem5  19947  nzrunit  20393  zrninitoringc  20545  islbs  20964  lbsind  20968  lbspss  20970  lbspropd  20987  lspsnne1  21008  islbs2  21045  lbsacsbs  21047  lbsextlem1  21049  lbsextlem3  21051  lbsextlem4  21052  lbsextg  21053  frlmlbs  21688  islindf  21703  islinds2  21704  islindf2  21705  lindfind  21707  lindsind  21708  lindfrn  21712  lindfmm  21718  lsslindf  21721  islindf4  21729  opsrtoslem2  21945  psdmul  22035  cply1coe0  22170  cply1coe0bi  22171  mdetunilem7  22487  mdetunilem8  22488  mdetunilem9  22489  maducoeval2  22509  pmatcollpw3fi1lem1  22655  fvmptnn04ifa  22719  fvmptnn04ifc  22721  fvmptnn04ifd  22722  chfacffsupp  22725  chfacfscmul0  22727  chfacfpmmul0  22731  elcls  22942  maxlp  23016  perfi  23024  ordtbaslem  23057  ordtval  23058  ordtbas2  23060  ordtopn1  23063  ordtopn2  23064  ordtcnv  23070  ordtrest  23071  ordtrest2lem  23072  ordtrest2  23073  pnfnei  23089  mnfnei  23090  isreg2  23246  ordthauslem  23252  cmpfi  23277  cmpfii  23278  bwth  23279  nconnsubb  23292  hausdiag  23514  txkgen  23521  kqdisj  23601  ordthmeolem  23670  fbfinnfr  23710  trfbas  23713  fbunfip  23738  fbasrn  23753  trfil3  23757  ufileu  23788  fin1aufil  23801  hausflim  23850  alexsubALTlem2  23917  alexsubALTlem3  23918  alexsubALTlem4  23919  ptcmplem2  23922  ptcmplem3  23923  stdbdbl  24386  iccntr  24691  reconnlem2  24697  iccpnfcnv  24823  xrhmeo  24825  lebnumlem1  24841  lebnumlem2  24842  lebnumlem3  24843  bcthlem4  25208  minveclem3b  25309  ivthlem2  25334  ivthlem3  25335  mbfmax  25531  mbfposr  25534  i1fd  25563  mbfi1fseqlem4  25600  itg2splitlem  25630  itg2monolem1  25632  itg2cnlem1  25643  dvne0  25897  lhop1lem  25899  deg1nn0clb  25976  dgrle  26129  coemulhi  26140  aaliou3lem9  26239  cos11  26423  logleb  26493  argrege0  26501  logdivle  26512  ellogdm  26529  cxple  26585  cxplt2  26588  cxple3  26591  isosctrlem1  26709  atandm  26767  atans2  26822  atantayl2  26829  eldmgm  26913  ftalem7  26970  isppw2  27006  musum  27082  dchrsum2  27160  bposlem1  27176  lgsmod  27215  lgsdir2lem2  27218  lgsdir2  27222  lgsne0  27227  lgsprme0  27231  gausslemma2dlem4  27261  lgsquadlem1  27272  2lgslem3  27296  2lgsoddprm  27308  2sq2  27325  addsqrexnreu  27334  rpvmasumlem  27379  padicabv  27522  ostth3  27530  ostth  27531  noextenddif  27561  nodenselem4  27580  nodenselem5  27581  nodenselem7  27583  nolt02o  27588  nogt01o  27589  noresle  27590  nosupprefixmo  27593  noinfprefixmo  27594  nosupcbv  27595  nosupdm  27597  nosupfv  27599  nosupres  27600  nosupbnd1lem1  27601  nosupbnd1lem3  27603  nosupbnd1lem5  27605  nosupbnd1  27607  nosupbnd2lem1  27608  nosupbnd2  27609  noinfcbv  27610  noinfdm  27612  noinffv  27614  noinfres  27615  noinfbnd1lem1  27616  noinfbnd1lem3  27618  noinfbnd1lem5  27620  noinfbnd1  27622  noinfbnd2lem1  27623  noinfbnd2  27624  slenlt  27645  sltne  27663  nocvxminlem  27671  slerec  27714  eqscut3  27719  cuteq1  27732  newbday  27801  sltlpss  27807  cofcutr  27822  lrrecfr  27840  addsval  27859  sltadd2  27888  sleneg  27942  slesubsubbd  27980  slesubsub2bd  27981  slesubsub3bd  27982  slesubaddd  27987  sltmul2  28064  slemul2d  28067  slemul1d  28068  onscutlt  28155  pw2cut2  28336  istrkgld  28391  axtgupdim2  28403  tglowdim2l  28582  axlowdimlem16  28889  axlowdim2  28892  axlowdim  28893  numedglnl  29076  usgredg2v  29159  lfuhgr1v0e  29186  cusgrfi  29391  vtxd0nedgb  29421  vtxduhgr0edgnel  29427  1loopgrnb0  29435  1hevtxdg0  29438  vtxdgoddnumeven  29486  wlkp1lem1  29604  wlkp1lem2  29605  wlkp1lem5  29608  dfpth2  29661  crctcsh  29756  clwlkclwwlklem2a4  29928  eupth2eucrct  30148  eupth2lem3lem3  30161  eupth2lem3lem4  30162  eupth2lem3lem6  30164  eupth2lem3lem7  30165  eupth2lems  30169  eupth2  30170  konigsberglem4  30186  nfrgr2v  30203  frgrwopreglem3  30245  fusgr2wsp2nb  30265  frgrreggt1  30324  friendshipgt3  30329  lpni  30411  nmobndseqi  30710  minvecolem5  30812  chpsscon3  31434  chnle  31445  nonbooli  31582  pjnel  31657  specval  31829  nmcfnlbi  31983  stri  32188  hstri  32196  cvbr  32213  cvcon3  32215  chcv1  32286  cvexchlem  32299  chrelat2  32301  nelun  32445  elpreq  32460  nelpr  32463  ifeqeqx  32474  nfpconfp  32566  suppiniseg  32619  isoun  32635  suppss3  32658  xrge0infss  32695  infxrge0gelb  32701  eliccelico  32712  elicoelioo  32713  nndiffz1  32721  hashgt1  32745  expgt0b  32754  nn0min  32758  ccatws1f1o  32888  toslublem  32909  tosglblem  32911  pmtrcnel  33026  cycpmco2  33070  isarchi2  33122  archiabl  33135  elrgspnlem2  33178  elrgspnlem3  33179  0nellinds  33303  lindssn  33311  lindfpropd  33315  ssdifidlprm  33391  mxidlirred  33405  ssmxidl  33407  lbslsat  33597  lindsunlem  33605  rtelextdg2lem  33707  constrsqrtcl  33760  ordtcnvNEW  33901  ordtrestNEW  33902  ordtrest2NEWlem  33903  ordtrest2NEW  33904  ordtconnlem1  33905  xrge0iifcnv  33914  esumpcvgval  34059  esum2d  34074  ddemeas  34217  omssubadd  34281  oddpwdc  34335  eulerpartlems  34341  eulerpartlemf  34351  eulerpartlemt  34352  eulerpartlemr  34355  eulerpartlemgvv  34357  eulerpartlemn  34362  ballotlemfc0  34474  ballotlemfcc  34475  ballotlem4  34480  ballotlemimin  34487  ballotlem7  34517  plymulx  34529  signsply0  34532  reprinfz1  34603  reprpmtf1o  34607  reprdifc  34608  hgt750lema  34638  hgt750leme  34639  istrkg2d  34647  bnj23  34698  bnj1185  34773  bnj1228  34991  bnj1388  35013  bnj1417  35021  nummin  35071  axnulg  35072  fineqvnttrclselem1  35087  onvf1odlem2  35094  onvf1odlem3  35095  revwlk  35115  isacycgr  35135  acycgr0v  35138  prclisacycgr  35141  erdszelem10  35190  satf0n0  35368  fmlaomn0  35380  fmlasucdisj  35389  satfv1fvfmla1  35413  satefvfmla1  35415  ismfs  35539  mvtinf  35545  untelirr  35698  untsucf  35700  untangtr  35704  dfon2lem3  35776  dfon2lem4  35777  dfon2lem7  35780  dfon2lem9  35782  distel  35794  funpartfv  35936  dfrdg4  35942  nn0prpwlem  36313  nn0prpw  36314  limsucncmpi  36436  limsucncmp  36437  ordcmp  36438  weiunlem2  36454  weiunfrlem  36455  weiunfr  36458  unblimceq0  36498  unbdqndv1  36499  bj-hbntbi  36695  bj-equsexvwd  36772  bj-cbvexdv  36791  bj-ru1  36934  bj-nuliota  37048  topdifinffinlem  37338  topdifinffin  37339  icorempo  37342  relowlpssretop  37355  finxpreclem2  37381  finxpreclem6  37387  wl-issetft  37573  wl-ax11-lem8  37583  leceifl  37606  lindsadd  37610  lindsenlbs  37612  matunitlindflem1  37613  poimirlem16  37633  poimirlem17  37634  poimirlem18  37635  poimirlem19  37636  poimirlem21  37638  poimirlem23  37640  poimirlem26  37643  poimirlem27  37644  poimirlem28  37645  poimirlem31  37648  poimir  37650  mblfinlem2  37655  mblfinlem3  37656  ismblfin  37658  cnambfre  37665  itg2addnclem  37668  itg2addnclem2  37669  iblabsnclem  37680  ftc1anclem1  37690  areacirc  37710  heibor1lem  37806  heiborlem1  37808  heiborlem6  37813  heiborlem8  37815  heiborlem10  37817  smprngopr  38049  ecin0  38337  ax12inda  38944  riotaclbgBAD  38950  lcvfbr  39016  lcvbr  39017  lsatcv0  39027  l1cvpat  39050  opltcon3b  39200  cvrfval  39264  cvrval  39265  cvrnbtwn  39267  cvrval2  39270  cvrnbtwn2  39271  cvrnbtwn3  39272  cvrcon3b  39273  cvrnbtwn4  39275  atnlt  39309  iscvlat  39319  cvlexch1  39324  hlsuprexch  39377  hlrelat5N  39397  hlrelat2  39399  cvrval5  39411  3dimlem1  39454  3dim1lem5  39462  3dim2  39464  3dim3  39465  llnnlt  39519  islpln5  39531  lplni2  39533  lvolex3N  39534  lplnnle2at  39537  islpln2a  39544  lplnribN  39547  lplnexllnN  39560  lplnnlt  39561  lvoli3  39573  islvol5  39575  lvoli2  39577  lvolnle3at  39578  islvol2aN  39588  4atlem11  39605  lvolnltN  39614  dalawlem15  39881  4atexlemex2  40067  4atex  40072  4atex2-0aOLDN  40074  4atex2-0cOLDN  40076  lautcvr  40088  ltrnfset  40113  ltrnset  40114  ltrnu  40117  trlfset  40156  trlset  40157  trlval2  40159  cdlemd6  40199  cdleme0nex  40286  cdleme18d  40291  cdleme25b  40350  cdleme25cv  40354  cdleme29b  40371  cdleme31fv  40386  cdleme31fv2  40389  cdlemefrs29bpre0  40392  cdlemefr32sn2aw  40400  cdlemefr29bpre0N  40402  cdlemefr29clN  40403  cdlemefr32fvaN  40405  cdlemefr32fva1  40406  cdlemefs32sn1aw  40410  cdleme32fva  40433  cdleme32fvaw  40435  cdleme40v  40465  cdleme42b  40474  cdleme46f2g2  40489  cdleme46f2g1  40490  cdleme48gfv  40533  cdlemg1fvawlemN  40569  cdlemg1cex  40584  cdlemg6d  40617  cdlemm10N  41114  dicffval  41170  dicfval  41171  dicval  41172  dicfnN  41179  dicvalrelN  41181  dihffval  41226  dihfval  41227  dihlsscpre  41230  dvh4dimat  41434  dvh3dimatN  41435  dvh4dimlem  41439  dvh3dim  41442  dvh4dimN  41443  dvh3dim2  41444  dvh3dim3N  41445  mapdcv  41656  mapdh9aOLDN  41786  hdmapfval  41823  hdmapval  41824  hdmapval2  41828  hdmap11lem2  41838  dvrelog2b  42056  aks4d1p4  42069  aks4d1p5  42070  aks4d1p7  42073  aks4d1p8d2  42075  aks4d1p8  42077  aks4d1  42079  aks6d1c2p2  42109  hashnexinj  42118  rspcsbnea  42121  aks6d1c5  42129  aks6d1c6lem3  42162  aks6d1c7  42174  supinf  42232  oexpreposd  42312  mullt0b2d  42474  flt4lem7  42649  nna4b4nsq  42650  ellz1  42757  rencldnfilem  42810  jm2.22  42985  jm2.23  42986  wepwsolem  43032  fnwe2lem2  43041  aomclem8  43051  unxpwdom3  43085  onsupmaxb  43229  onexlimgt  43233  onsupeqnmax  43237  onov0suclim  43264  oaordnr  43286  omnord1  43295  oenord1  43306  oaomoencom  43307  oenass  43309  cantnfresb  43314  tfsnfin  43342  ralopabb  43401  nlimsuc  43431  ifpbi12  43478  dfsucon  43513  sqrtcvallem1  43621  ss2iundf  43649  frege124d  43751  clsk3nimkb  44030  clsk1indlem1  44035  clsk1independent  44036  ntrneineine1lem  44074  ntrneicls11  44080  clsneiel1  44098  clsneiel2  44099  neicvgel1  44109  neicvgel2  44110  radcnvrat  44304  rusbcALT  44428  en3lpVD  44834  0elaxnul  44973  omssaxinf2  44978  permaxnul  44998  permaxinf2lem  45002  nregmodel  45007  eliin2f  45098  nssd  45099  wessf1ornlem  45179  rexanuz2nf  45487  limsupre2lem  45719  icccncfext  45882  stoweidlem14  46009  stoweidlem34  46029  stoweidlem59  46054  etransclem24  46253  nnfoctbdjlem  46450  nnfoctbdj  46451  hspmbllem2  46622  nsssmfmbflem  46773  fsetsnprcnex  47053  eu2ndop1stv  47123  afvfv0bi  47150  afvco2  47174  ndmaovg  47182  ndfatafv2nrn  47219  afv2ndefb  47222  afv2fv0  47263  nelbr  47272  otiunsndisjX  47277  fun2dmnopgexmpl  47282  ltnltne  47297  readdcnnred  47301  resubcnnred  47302  recnmulnred  47303  cndivrenred  47304  ichnreuop  47470  fmtnoinf  47534  odz2prm2pw  47561  prmdvdsfmtnof1lem2  47583  lighneallem3  47605  lighneallem4  47608  requad1  47620  isodd3  47650  bits0ALTV  47677  nfermltl8rev  47740  nfermltl2rev  47741  nfermltlrev  47742  upgrimpths  47907  isubgr3stgrlem3  47966  usgrexmpl12ngric  48036  pgnbgreunbgrlem2lem1  48112  pgnbgreunbgrlem2lem2  48113  pgnbgreunbgrlem2lem3  48114  pgnbgreunbgrlem5lem1  48118  pgnbgreunbgrlem5lem2  48119  pgnbgreunbgrlem5lem3  48120  lgricngricex  48127  lidldomnnring  48234  ztprmneprm  48345  lindepsnlininds  48451  islindeps  48452  lindslinindsimp2lem5  48461  lindslinindsimp2  48462  line2ylem  48750  line2xlem  48752  map0cor  48853  nelsubc3lem  49069  fulltermc2  49511  setc1onsubc  49601  cnelsubclem  49602  elsetrecslem  49698