Theorem notbid 320

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 317	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
3		notnotb 317	. . 3 ⊢ (𝜒 ↔ ¬ ¬ 𝜒)
4	1, 2, 3	3bitr3g 315	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
5	4	con4bid 319	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

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

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 209

This theorem is referenced by:  notbi  321  annotanannot  832  ifpbi123dOLD  1073  con3ALT  1080  con3ALTOLD  1081  xorbi12d  1517  norassOLD  1534  equsexvw  2011  cbvexvw  2044  cbvexdvaw  2046  hbe1w  2055  cbvexv1  2362  cbvex2v  2365  drex1v  2388  cbvex  2417  cbvexvOLD  2421  cbvex2  2434  drex1  2463  eujustALT  2657  necon3abid  3052  neleq12d  3127  cbvrexfw  3438  cbvrexf  3440  cbvrexdva2OLD  3458  gencbval  3551  spcegf  3591  spc2gv  3601  spc2d  3603  spc3gv  3605  cdeqnot  3759  rru  3770  ru  3771  sbcng  3819  sbcrext  3856  cbvrexcsf  3926  difjust  3938  eldif  3946  dfpss3  4063  dfdif3  4091  difeq2  4093  disjne  4404  pssdifcom1  4435  eldifpr  4597  elpwunsn  4621  eldiftp  4624  preqsnd  4789  disjxun  5064  nalset  5217  dtru  5271  dtruALT  5289  rexxfrd  5310  rexxfr2d  5312  rexxfrd2  5314  rexxfr  5317  dtruALT2  5336  opthneg  5373  snopeqop  5396  otiunsndisj  5410  poeq1  5477  pocl  5481  swopo  5484  sotric  5501  sotrieq  5502  isso2i  5508  somo  5510  freq1  5525  frirr  5532  fr2nr  5533  frminex  5535  tz7.2  5539  wereu2  5552  poinxp  5632  frinxp  5634  posn  5637  frsn  5639  rexiunxp  5711  rexxpf  5718  intirr  5978  poirr2  5984  cnvpo  6138  predpoirr  6176  predfrirr  6177  nordeq  6210  ordtri1  6224  ordtri3  6227  fvmpti  6767  fndmdif  6812  rexrnmptw  6861  rexrnmpt  6863  2f1fvneq  7018  f1imapss  7024  cbvexfo  7046  nf1const  7059  soisoi  7081  isopolem  7098  weniso  7107  canth  7111  riotaclb  7155  rexrnmpo  7290  ndmovg  7331  sorpssuni  7458  sorpssint  7459  fr3nr  7494  dfwe2  7496  ordsucsssuc  7538  nlimsucg  7557  orduninsuc  7558  dfom2  7582  ssnlim  7599  f1oweALT  7673  frxp  7820  poxp  7822  suppofssd  7867  wfrlem10  7964  smoword  8003  tz7.48lem  8077  oacan  8174  oaword  8175  omlimcl  8204  omeulem1  8208  nnaword  8253  nnmword  8259  nneob  8279  brdifun  8318  swoer  8319  undifixp  8498  boxcutc  8505  2dom  8582  php  8701  nndomo  8712  nnsdomo  8713  unxpdomlem2  8723  frfi  8763  unfilem1  8782  supeq3  8913  supeq123d  8914  supmo  8916  eqsup  8920  supub  8923  sup0  8930  suppr  8935  supisolem  8937  supisoex  8938  eqinf  8948  infval  8950  infmo  8959  infpr  8967  infempty  8971  oieq1  8976  ordtypecbv  8981  ordtypelem7  8988  wemapsolem  9014  canthwdom  9043  zfregcl  9058  elirrv  9060  elirr  9061  noinfep  9123  cantnfp1lem3  9143  rankr1clem  9249  carden2b  9396  domtri2  9418  alephord3  9504  alephdom2  9513  alephval3  9536  dfac9  9562  kmlem2  9577  kmlem4  9579  isfin4  9719  isfin7  9723  fin23lem11  9739  isf32lem5  9779  isf34lem4  9799  fin1a2lem6  9827  fin1a2lem7  9828  fin1a2lem12  9833  itunisuc  9841  ac6n  9907  zorn2g  9925  zornn0g  9927  ttukeylem7  9937  axpowndlem3  10021  axpowndlem4  10022  axregnd  10026  elgch  10044  engch  10050  fpwwe2lem13  10064  fpwwe2  10065  pwfseqlem1  10080  pwfseqlem3  10082  hargch  10095  addnidpi  10323  pinq  10349  nqereu  10351  ltsonq  10391  prlem934  10455  ltexprlem7  10464  addcanpr  10468  prlem936  10469  reclem2pr  10470  reclem3pr  10471  supexpr  10476  ltsosr  10516  supsrlem  10533  axpre-lttri  10587  axpre-sup  10591  xrlenlt  10706  axlttri  10712  axsup  10716  ltne  10737  dedekind  10803  readdcan  10814  leadd1  11108  ltsub1  11136  ltsub2  11137  leord1  11167  lediv1  11505  lemuldiv  11520  lerec  11523  le2msq  11540  infm3  11600  suprnub  11606  infregelb  11625  avgle1  11878  avgle2  11879  znnnlt1  12010  indstr  12317  zsupss  12338  uzsupss  12341  rpneg  12422  xralrple  12599  xleneg  12612  xltadd1  12650  xposdif  12656  xmulneg1  12663  xltmul1  12686  xrsupexmnf  12699  xrinfmexpnf  12700  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  supxrleub  12720  infxrgelb  12729  difreicc  12871  nn0disj  13024  nelfzo  13044  elfznelfzo  13143  fvinim0ffz  13157  injresinjlem  13158  ssnn0fi  13354  leexp2  13536  hashbnd  13697  hasheni  13709  hashbc  13812  wrdsymb0  13901  swrdnd  14016  swrdnd2  14017  pfxnd0  14050  repswswrd  14146  repswccat  14148  cshwidxmod  14165  cnpart  14599  sqrtlt  14621  limsuplt  14836  rlimrege0  14936  isercoll  15024  efle  15471  odd2np1  15690  sumodd  15739  divalglem7  15750  ndvdsadd  15761  fldivndvdslt  15765  bitsfval  15772  bitsval  15773  bits0  15777  bitsp1  15780  bitsmod  15785  bitscmp  15787  bitsinv1lem  15790  sadadd2lem2  15799  saddisjlem  15813  bitsshft  15824  gcdneg  15870  algcvgblem  15921  lcmneg  15947  isprm3  16027  dvdsnprmd  16034  isprm5  16051  rpexp  16064  phiprmpw  16113  m1dvdsndvds  16135  pythagtrip  16171  pcgcd1  16213  prmpwdvds  16240  prmreclem2  16253  prmreclem3  16254  prmreclem5  16256  prmreclem6  16257  vdwlem6  16322  vdwnnlem2  16332  vdwnnlem3  16333  vdwnn  16334  prmlem0  16439  prmlem1a  16440  divsfval  16820  mrisval  16901  ismri  16902  ismri2dad  16908  cidpropd  16980  plttr  17580  joinval  17615  meetval  17629  acsfiindd  17787  isnsgrp  17905  smndex1n0mnd  18077  mgm2nsgrplem2  18084  sgrp2nmndlem3  18090  symgpssefmnd  18524  symgfix2  18544  pmtrdifellem4  18607  psgnunilem1  18621  psgnunilem5  18622  psgnunilem2  18623  psgnunilem3  18624  pmtrsn  18647  sylow1lem3  18725  sylow2alem2  18743  efgsfo  18865  ablfac1eulem  19194  ablfac1eu  19195  pgpfac1lem1  19196  pgpfac1lem5  19201  islbs  19848  lbsind  19852  lbspss  19854  lbspropd  19871  lspsnne1  19889  islbs2  19926  lbsacsbs  19928  lbsextlem1  19930  lbsextlem3  19932  lbsextlem4  19933  lbsextg  19934  nzrunit  20040  opsrtoslem2  20265  cply1coe0  20467  cply1coe0bi  20468  frlmlbs  20941  islindf  20956  islinds2  20957  islindf2  20958  lindfind  20960  lindsind  20961  lindfrn  20965  lindfmm  20971  lsslindf  20974  islindf4  20982  mdetunilem7  21227  mdetunilem8  21228  mdetunilem9  21229  maducoeval2  21249  pmatcollpw3fi1lem1  21394  fvmptnn04ifa  21458  fvmptnn04ifc  21460  fvmptnn04ifd  21461  chfacffsupp  21464  chfacfscmul0  21466  chfacfpmmul0  21470  elcls  21681  maxlp  21755  perfi  21763  ordtbaslem  21796  ordtval  21797  ordtbas2  21799  ordtopn1  21802  ordtopn2  21803  ordtcnv  21809  ordtrest  21810  ordtrest2lem  21811  ordtrest2  21812  pnfnei  21828  mnfnei  21829  isreg2  21985  ordthauslem  21991  cmpfi  22016  cmpfii  22017  bwth  22018  nconnsubb  22031  hausdiag  22253  txkgen  22260  kqdisj  22340  ordthmeolem  22409  fbfinnfr  22449  trfbas  22452  fbunfip  22477  fbasrn  22492  trfil3  22496  ufileu  22527  fin1aufil  22540  hausflim  22589  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem2  22661  ptcmplem3  22662  stdbdbl  23127  iccntr  23429  reconnlem2  23435  iccpnfcnv  23548  xrhmeo  23550  lebnumlem1  23565  lebnumlem2  23566  lebnumlem3  23567  bcthlem4  23930  minveclem3b  24031  ivthlem2  24053  ivthlem3  24054  mbfmax  24250  mbfposr  24253  i1fd  24282  mbfi1fseqlem4  24319  itg2splitlem  24349  itg2monolem1  24351  itg2cnlem1  24362  dvne0  24608  lhop1lem  24610  deg1nn0clb  24684  dgrle  24833  coemulhi  24844  aaliou3lem9  24939  cos11  25117  logleb  25186  argrege0  25194  logdivle  25205  ellogdm  25222  cxple  25278  cxplt2  25281  cxple3  25284  isosctrlem1  25396  atandm  25454  atans2  25509  atantayl2  25516  eldmgm  25599  ftalem7  25656  isppw2  25692  musum  25768  dchrsum2  25844  bposlem1  25860  lgsmod  25899  lgsdir2lem2  25902  lgsdir2  25906  lgsne0  25911  lgsprme0  25915  gausslemma2dlem4  25945  lgsquadlem1  25956  2lgslem3  25980  2lgsoddprm  25992  2sq2  26009  addsqrexnreu  26018  rpvmasumlem  26063  padicabv  26206  ostth3  26214  ostth  26215  istrkgld  26245  axtgupdim2  26257  tglowdim2l  26436  axlowdimlem16  26743  axlowdim2  26746  axlowdim  26747  numedglnl  26929  usgredg2v  27009  lfuhgr1v0e  27036  cusgrfi  27240  vtxd0nedgb  27270  vtxduhgr0edgnel  27276  1loopgrnb0  27284  1hevtxdg0  27287  vtxdgoddnumeven  27335  wlkp1lem1  27455  wlkp1lem2  27456  wlkp1lem5  27459  crctcsh  27602  clwlkclwwlklem2a4  27775  eupth2eucrct  27996  eupth2lem3lem3  28009  eupth2lem3lem4  28010  eupth2lem3lem6  28012  eupth2lem3lem7  28013  eupth2lems  28017  eupth2  28018  konigsberglem4  28034  nfrgr2v  28051  frgrwopreglem3  28093  fusgr2wsp2nb  28113  frgrreggt1  28172  friendshipgt3  28177  lpni  28257  nmobndseqi  28556  minvecolem5  28658  chpsscon3  29280  chnle  29291  nonbooli  29428  pjnel  29503  specval  29675  nmcfnlbi  29829  stri  30034  hstri  30042  cvbr  30059  cvcon3  30061  chcv1  30132  cvexchlem  30145  chrelat2  30147  nelun  30274  elpreq  30290  nelpr  30291  ifeqeqx  30297  nfpconfp  30377  isoun  30437  suppss3  30460  xrge0infss  30484  infxrge0gelb  30490  eliccelico  30500  elicoelioo  30501  nndiffz1  30509  hashgt1  30530  nn0min  30536  toslublem  30654  tosglblem  30656  pmtrcnel  30733  cycpmco2  30775  isarchi2  30814  archiabl  30827  0nellinds  30935  lindssn  30939  lindfpropd  30942  ssmxidl  30979  lbslsat  31014  lindsunlem  31020  ordtcnvNEW  31163  ordtrestNEW  31164  ordtrest2NEWlem  31165  ordtrest2NEW  31166  ordtconnlem1  31167  xrge0iifcnv  31176  esumpcvgval  31337  esum2d  31352  ddemeas  31495  omssubadd  31558  oddpwdc  31612  eulerpartlems  31618  eulerpartlemf  31628  eulerpartlemt  31629  eulerpartlemr  31632  eulerpartlemgvv  31634  eulerpartlemn  31639  ballotlemfc0  31750  ballotlemfcc  31751  ballotlem4  31756  ballotlemimin  31763  ballotlem7  31793  plymulx  31818  signsply0  31821  reprinfz1  31893  reprpmtf1o  31897  reprdifc  31898  hgt750lema  31928  hgt750leme  31929  istrkg2d  31937  bnj23  31988  bnj1185  32065  bnj1228  32283  bnj1388  32305  bnj1417  32313  hashfundm  32354  revwlk  32371  isacycgr  32392  acycgr0v  32395  prclisacycgr  32398  erdszelem10  32447  satf0n0  32625  fmlaomn0  32637  fmlasucdisj  32646  satfv1fvfmla1  32670  satefvfmla1  32672  ismfs  32796  mvtinf  32802  untelirr  32934  untsucf  32936  untangtr  32940  ceqsralv2  32956  dfpo2  32991  dfon2lem3  33030  dfon2lem4  33031  dfon2lem7  33034  dfon2lem9  33036  distel  33048  frpomin  33078  soseq  33096  noextenddif  33175  nodenselem4  33191  nodenselem5  33192  nodenselem7  33194  nolt02o  33199  noresle  33200  noprefixmo  33202  nosupdm  33204  nosupfv  33206  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd1  33214  nosupbnd2lem1  33215  nosupbnd2  33216  slenlt  33231  nocvxminlem  33247  slerec  33277  funpartfv  33406  dfrdg4  33412  nn0prpwlem  33670  nn0prpw  33671  limsucncmpi  33793  limsucncmp  33794  ordcmp  33795  unblimceq0  33846  unbdqndv1  33847  bj-hbntbi  34038  bj-cbvexdv  34122  bj-dtru  34139  bj-ru0  34256  bj-nuliota  34353  topdifinffinlem  34631  topdifinffin  34632  icorempo  34635  relowlpssretop  34648  finxpreclem2  34674  finxpreclem6  34680  wl-ax11-lem8  34839  wl-dfrexf  34862  leceifl  34896  lindsadd  34900  lindsenlbs  34902  matunitlindflem1  34903  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem21  34928  poimirlem23  34930  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem31  34938  poimir  34940  mblfinlem2  34945  mblfinlem3  34946  ismblfin  34948  cnambfre  34955  itg2addnclem  34958  itg2addnclem2  34959  iblabsnclem  34970  ftc1anclem1  34982  areacirc  35002  heibor1lem  35102  heiborlem1  35104  heiborlem6  35109  heiborlem8  35111  heiborlem10  35113  smprngopr  35345  ecin0  35621  ax12inda  36099  riotaclbgBAD  36105  lcvfbr  36171  lcvbr  36172  lsatcv0  36182  l1cvpat  36205  opltcon3b  36355  cvrfval  36419  cvrval  36420  cvrnbtwn  36422  cvrval2  36425  cvrnbtwn2  36426  cvrnbtwn3  36427  cvrcon3b  36428  cvrnbtwn4  36430  atnlt  36464  iscvlat  36474  cvlexch1  36479  hlsuprexch  36532  hlrelat5N  36552  hlrelat2  36554  cvrval5  36566  3dimlem1  36609  3dim1lem5  36617  3dim2  36619  3dim3  36620  llnnlt  36674  islpln5  36686  lplni2  36688  lvolex3N  36689  lplnnle2at  36692  islpln2a  36699  lplnribN  36702  lplnexllnN  36715  lplnnlt  36716  lvoli3  36728  islvol5  36730  lvoli2  36732  lvolnle3at  36733  islvol2aN  36743  4atlem11  36760  lvolnltN  36769  dalawlem15  37036  4atexlemex2  37222  4atex  37227  4atex2-0aOLDN  37229  4atex2-0cOLDN  37231  lautcvr  37243  ltrnfset  37268  ltrnset  37269  ltrnu  37272  trlfset  37311  trlset  37312  trlval2  37314  cdlemd6  37354  cdleme0nex  37441  cdleme18d  37446  cdleme25b  37505  cdleme25cv  37509  cdleme29b  37526  cdleme31fv  37541  cdleme31fv2  37544  cdlemefrs29bpre0  37547  cdlemefr32sn2aw  37555  cdlemefr29bpre0N  37557  cdlemefr29clN  37558  cdlemefr32fvaN  37560  cdlemefr32fva1  37561  cdlemefs32sn1aw  37565  cdleme32fva  37588  cdleme32fvaw  37590  cdleme40v  37620  cdleme42b  37629  cdleme46f2g2  37644  cdleme46f2g1  37645  cdleme48gfv  37688  cdlemg1fvawlemN  37724  cdlemg1cex  37739  cdlemg6d  37772  cdlemm10N  38269  dicffval  38325  dicfval  38326  dicval  38327  dicfnN  38334  dicvalrelN  38336  dihffval  38381  dihfval  38382  dihlsscpre  38385  dvh4dimat  38589  dvh3dimatN  38590  dvh4dimlem  38594  dvh3dim  38597  dvh4dimN  38598  dvh3dim2  38599  dvh3dim3N  38600  mapdcv  38811  mapdh9aOLDN  38941  hdmapfval  38978  hdmapval  38979  hdmapval2  38983  hdmap11lem2  38993  oexpreposd  39228  ellz1  39413  rencldnfilem  39466  jm2.22  39641  jm2.23  39642  wepwsolem  39691  fnwe2lem2  39700  aomclem8  39710  unxpwdom3  39744  ifpbi12  39903  dfsucon  39938  nndomog  39946  ss2iundf  40053  frege124d  40155  clsk3nimkb  40439  clsk1indlem1  40444  clsk1independent  40445  ntrneineine1lem  40483  ntrneicls11  40489  clsneiel1  40507  clsneiel2  40508  neicvgel1  40518  neicvgel2  40519  radcnvrat  40695  rusbcALT  40820  en3lpVD  41228  eliin2f  41419  nssd  41420  wessf1ornlem  41494  limsupre2lem  42054  icccncfext  42219  stoweidlem14  42348  stoweidlem34  42368  stoweidlem59  42393  etransclem24  42592  nnfoctbdjlem  42786  nnfoctbdj  42787  hspmbllem2  42958  smfmbfcex  43085  nsssmfmbflem  43103  eu2ndop1stv  43373  afvfv0bi  43400  afvco2  43424  ndmaovg  43432  ndfatafv2nrn  43469  afv2ndefb  43472  afv2fv0  43513  nelbr  43522  otiunsndisjX  43527  fun2dmnopgexmpl  43532  ltnltne  43548  readdcnnred  43552  resubcnnred  43553  recnmulnred  43554  cndivrenred  43555  ichnreuop  43683  fmtnoinf  43747  odz2prm2pw  43774  prmdvdsfmtnof1lem2  43796  lighneallem3  43821  lighneallem4  43824  requad1  43836  isodd3  43866  bits0ALTV  43893  nfermltl8rev  43956  nfermltl2rev  43957  nfermltlrev  43958  lidldomnnring  44250  zrninitoringc  44391  ztprmneprm  44444  lindepsnlininds  44556  islindeps  44557  lindslinindsimp2lem5  44566  lindslinindsimp2  44567  difmodm1lt  44631  line2ylem  44787  line2xlem  44789  elsetrecslem  44850