Theorem notbid 321

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

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

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 210

This theorem is referenced by:  notbi  322  annotanannot  833  ifpbi123dOLD  1076  con3ALT  1082  xorbi12d  1518  norassOLD  1535  equsexvw  2011  cbvexvw  2044  cbvexdvaw  2046  hbe1w  2055  cbvexv1  2351  cbvex2v  2354  drex1v  2377  cbvex  2406  cbvexvOLD  2410  cbvex2  2423  drex1  2452  eujustALT  2632  necon3abid  3023  neleq12d  3095  cbvrexfw  3384  cbvrexf  3386  cbvrexdva2OLD  3405  cgsex4g  3486  gencbval  3499  spcegf  3539  spc2gv  3549  spc2d  3551  spc3gv  3553  cdeqnot  3707  rru  3718  ru  3719  sbcng  3766  sbcrext  3802  cbvrexcsf  3871  difjust  3883  eldif  3891  dfpss3  4014  dfdif3  4042  difeq2  4044  disjne  4362  pssdifcom1  4393  eldifpr  4557  elpwunsn  4581  eldiftp  4584  preqsnd  4749  disjxun  5028  nalset  5181  dtru  5236  dtruALT  5254  rexxfrd  5275  rexxfr2d  5277  rexxfrd2  5279  rexxfr  5282  dtruALT2  5301  opthneg  5338  snopeqop  5361  otiunsndisj  5375  poeq1  5441  pocl  5445  swopo  5448  sotric  5465  sotrieq  5466  isso2i  5472  somo  5474  freq1  5489  frirr  5496  fr2nr  5497  frminex  5499  tz7.2  5503  wereu2  5516  poinxp  5596  frinxp  5598  posn  5601  frsn  5603  rexiunxp  5675  rexxpf  5682  intirr  5945  poirr2  5951  cnvpo  6106  predpoirr  6144  predfrirr  6145  nordeq  6178  ordtri1  6192  ordtri3  6195  fvmpti  6744  fndmdif  6789  rexrnmptw  6838  rexrnmpt  6840  2f1fvneq  6996  f1imapss  7002  cbvexfo  7024  nf1const  7038  soisoi  7060  isopolem  7077  weniso  7086  canth  7090  riotaclb  7134  rexrnmpo  7269  ndmovg  7311  sorpssuni  7438  sorpssint  7439  fr3nr  7474  dfwe2  7476  ordsucsssuc  7518  nlimsucg  7537  orduninsuc  7538  dfom2  7562  ssnlim  7579  f1oweALT  7655  frxp  7803  poxp  7805  suppofssd  7850  suppcoss  7854  wfrlem10  7947  smoword  7986  tz7.48lem  8060  oacan  8157  oaword  8158  omlimcl  8187  omeulem1  8191  nnaword  8236  nnmword  8242  nneob  8262  brdifun  8301  swoer  8302  undifixp  8481  boxcutc  8488  2dom  8565  php  8685  nndomog  8692  nnsdomo  8698  unxpdomlem2  8707  frfi  8747  unfilem1  8766  supeq3  8897  supeq123d  8898  supmo  8900  eqsup  8904  supub  8907  sup0  8914  suppr  8919  supisolem  8921  supisoex  8922  eqinf  8932  infval  8934  infmo  8943  infpr  8951  infempty  8955  oieq1  8960  ordtypecbv  8965  ordtypelem7  8972  wemapsolem  8998  canthwdom  9027  zfregcl  9042  elirrv  9044  elirr  9045  noinfep  9107  cantnfp1lem3  9127  rankr1clem  9233  carden2b  9380  domtri2  9402  alephord3  9489  alephdom2  9498  alephval3  9521  dfac9  9547  kmlem2  9562  kmlem4  9564  isfin4  9708  isfin7  9712  fin23lem11  9728  isf32lem5  9768  isf34lem4  9788  fin1a2lem6  9816  fin1a2lem7  9817  fin1a2lem12  9822  itunisuc  9830  ac6n  9896  zorn2g  9914  zornn0g  9916  ttukeylem7  9926  axpowndlem3  10010  axpowndlem4  10011  axregnd  10015  elgch  10033  engch  10039  fpwwe2lem13  10053  fpwwe2  10054  pwfseqlem1  10069  pwfseqlem3  10071  hargch  10084  addnidpi  10312  pinq  10338  nqereu  10340  ltsonq  10380  prlem934  10444  ltexprlem7  10453  addcanpr  10457  prlem936  10458  reclem2pr  10459  reclem3pr  10460  supexpr  10465  ltsosr  10505  supsrlem  10522  axpre-lttri  10576  axpre-sup  10580  xrlenlt  10695  axlttri  10701  axsup  10705  ltne  10726  dedekind  10792  readdcan  10803  leadd1  11097  ltsub1  11125  ltsub2  11126  leord1  11156  lediv1  11494  lemuldiv  11509  lerec  11512  le2msq  11529  infm3  11587  suprnub  11593  infregelb  11612  avgle1  11865  avgle2  11866  znnnlt1  11997  indstr  12304  zsupss  12325  uzsupss  12328  rpneg  12409  xralrple  12586  xleneg  12599  xltadd1  12637  xposdif  12643  xmulneg1  12650  xltmul1  12673  xrsupexmnf  12686  xrinfmexpnf  12687  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  supxrleub  12707  infxrgelb  12716  difreicc  12862  nn0disj  13018  nelfzo  13038  elfznelfzo  13137  fvinim0ffz  13151  injresinjlem  13152  ssnn0fi  13348  leexp2  13531  hashbnd  13692  hasheni  13704  hashbc  13807  wrdsymb0  13892  swrdnd  14007  swrdnd2  14008  pfxnd0  14041  repswswrd  14137  repswccat  14139  cshwidxmod  14156  cnpart  14591  sqrtlt  14613  limsuplt  14828  rlimrege0  14928  isercoll  15016  efle  15463  odd2np1  15682  sumodd  15729  divalglem7  15740  ndvdsadd  15751  fldivndvdslt  15755  bitsfval  15762  bitsval  15763  bits0  15767  bitsp1  15770  bitsmod  15775  bitscmp  15777  bitsinv1lem  15780  sadadd2lem2  15789  saddisjlem  15803  bitsshft  15814  gcdneg  15860  algcvgblem  15911  lcmneg  15937  isprm3  16017  dvdsnprmd  16024  isprm5  16041  rpexp  16054  phiprmpw  16103  m1dvdsndvds  16125  pythagtrip  16161  pcgcd1  16203  prmpwdvds  16230  prmreclem2  16243  prmreclem3  16244  prmreclem5  16246  prmreclem6  16247  vdwlem6  16312  vdwnnlem2  16322  vdwnnlem3  16323  vdwnn  16324  prmlem0  16431  prmlem1a  16432  divsfval  16812  mrisval  16893  ismri  16894  ismri2dad  16900  cidpropd  16972  plttr  17572  joinval  17607  meetval  17621  acsfiindd  17779  isnsgrp  17897  smndex1n0mnd  18069  mgm2nsgrplem2  18076  sgrp2nmndlem3  18082  symgpssefmnd  18516  symgfix2  18536  pmtrdifellem4  18599  psgnunilem1  18613  psgnunilem5  18614  psgnunilem2  18615  psgnunilem3  18616  pmtrsn  18639  sylow1lem3  18717  sylow2alem2  18735  efgsfo  18857  ablfac1eulem  19187  ablfac1eu  19188  pgpfac1lem1  19189  pgpfac1lem5  19194  islbs  19841  lbsind  19845  lbspss  19847  lbspropd  19864  lspsnne1  19882  islbs2  19919  lbsacsbs  19921  lbsextlem1  19923  lbsextlem3  19925  lbsextlem4  19926  lbsextg  19927  nzrunit  20033  frlmlbs  20486  islindf  20501  islinds2  20502  islindf2  20503  lindfind  20505  lindsind  20506  lindfrn  20510  lindfmm  20516  lsslindf  20519  islindf4  20527  opsrtoslem2  20724  cply1coe0  20928  cply1coe0bi  20929  mdetunilem7  21223  mdetunilem8  21224  mdetunilem9  21225  maducoeval2  21245  pmatcollpw3fi1lem1  21391  fvmptnn04ifa  21455  fvmptnn04ifc  21457  fvmptnn04ifd  21458  chfacffsupp  21461  chfacfscmul0  21463  chfacfpmmul0  21467  elcls  21678  maxlp  21752  perfi  21760  ordtbaslem  21793  ordtval  21794  ordtbas2  21796  ordtopn1  21799  ordtopn2  21800  ordtcnv  21806  ordtrest  21807  ordtrest2lem  21808  ordtrest2  21809  pnfnei  21825  mnfnei  21826  isreg2  21982  ordthauslem  21988  cmpfi  22013  cmpfii  22014  bwth  22015  nconnsubb  22028  hausdiag  22250  txkgen  22257  kqdisj  22337  ordthmeolem  22406  fbfinnfr  22446  trfbas  22449  fbunfip  22474  fbasrn  22489  trfil3  22493  ufileu  22524  fin1aufil  22537  hausflim  22586  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  ptcmplem2  22658  ptcmplem3  22659  stdbdbl  23124  iccntr  23426  reconnlem2  23432  iccpnfcnv  23549  xrhmeo  23551  lebnumlem1  23566  lebnumlem2  23567  lebnumlem3  23568  bcthlem4  23931  minveclem3b  24032  ivthlem2  24056  ivthlem3  24057  mbfmax  24253  mbfposr  24256  i1fd  24285  mbfi1fseqlem4  24322  itg2splitlem  24352  itg2monolem1  24354  itg2cnlem1  24365  dvne0  24614  lhop1lem  24616  deg1nn0clb  24691  dgrle  24840  coemulhi  24851  aaliou3lem9  24946  cos11  25125  logleb  25194  argrege0  25202  logdivle  25213  ellogdm  25230  cxple  25286  cxplt2  25289  cxple3  25292  isosctrlem1  25404  atandm  25462  atans2  25517  atantayl2  25524  eldmgm  25607  ftalem7  25664  isppw2  25700  musum  25776  dchrsum2  25852  bposlem1  25868  lgsmod  25907  lgsdir2lem2  25910  lgsdir2  25914  lgsne0  25919  lgsprme0  25923  gausslemma2dlem4  25953  lgsquadlem1  25964  2lgslem3  25988  2lgsoddprm  26000  2sq2  26017  addsqrexnreu  26026  rpvmasumlem  26071  padicabv  26214  ostth3  26222  ostth  26223  istrkgld  26253  axtgupdim2  26265  tglowdim2l  26444  axlowdimlem16  26751  axlowdim2  26754  axlowdim  26755  numedglnl  26937  usgredg2v  27017  lfuhgr1v0e  27044  cusgrfi  27248  vtxd0nedgb  27278  vtxduhgr0edgnel  27284  1loopgrnb0  27292  1hevtxdg0  27295  vtxdgoddnumeven  27343  wlkp1lem1  27463  wlkp1lem2  27464  wlkp1lem5  27467  crctcsh  27610  clwlkclwwlklem2a4  27782  eupth2eucrct  28002  eupth2lem3lem3  28015  eupth2lem3lem4  28016  eupth2lem3lem6  28018  eupth2lem3lem7  28019  eupth2lems  28023  eupth2  28024  konigsberglem4  28040  nfrgr2v  28057  frgrwopreglem3  28099  fusgr2wsp2nb  28119  frgrreggt1  28178  friendshipgt3  28183  lpni  28263  nmobndseqi  28562  minvecolem5  28664  chpsscon3  29286  chnle  29297  nonbooli  29434  pjnel  29509  specval  29681  nmcfnlbi  29835  stri  30040  hstri  30048  cvbr  30065  cvcon3  30067  chcv1  30138  cvexchlem  30151  chrelat2  30153  nelun  30282  elpreq  30302  nelpr  30303  ifeqeqx  30309  nfpconfp  30391  suppiniseg  30446  isoun  30461  suppss3  30486  xrge0infss  30510  infxrge0gelb  30516  eliccelico  30526  elicoelioo  30527  nndiffz1  30535  hashgt1  30556  nn0min  30562  toslublem  30680  tosglblem  30682  pmtrcnel  30783  cycpmco2  30825  isarchi2  30864  archiabl  30877  0nellinds  30986  lindssn  30993  lindfpropd  30996  ssmxidl  31050  lbslsat  31102  lindsunlem  31108  ordtcnvNEW  31273  ordtrestNEW  31274  ordtrest2NEWlem  31275  ordtrest2NEW  31276  ordtconnlem1  31277  xrge0iifcnv  31286  esumpcvgval  31447  esum2d  31462  ddemeas  31605  omssubadd  31668  oddpwdc  31722  eulerpartlems  31728  eulerpartlemf  31738  eulerpartlemt  31739  eulerpartlemr  31742  eulerpartlemgvv  31744  eulerpartlemn  31749  ballotlemfc0  31860  ballotlemfcc  31861  ballotlem4  31866  ballotlemimin  31873  ballotlem7  31903  plymulx  31928  signsply0  31931  reprinfz1  32003  reprpmtf1o  32007  reprdifc  32008  hgt750lema  32038  hgt750leme  32039  istrkg2d  32047  bnj23  32098  bnj1185  32175  bnj1228  32393  bnj1388  32415  bnj1417  32423  hashfundm  32464  nummin  32474  revwlk  32484  isacycgr  32505  acycgr0v  32508  prclisacycgr  32511  erdszelem10  32560  satf0n0  32738  fmlaomn0  32750  fmlasucdisj  32759  satfv1fvfmla1  32783  satefvfmla1  32785  ismfs  32909  mvtinf  32915  untelirr  33047  untsucf  33049  untangtr  33053  ceqsralv2  33069  dfpo2  33104  dfon2lem3  33143  dfon2lem4  33144  dfon2lem7  33147  dfon2lem9  33149  distel  33161  frpomin  33191  soseq  33209  noextenddif  33288  nodenselem4  33304  nodenselem5  33305  nodenselem7  33307  nolt02o  33312  noresle  33313  noprefixmo  33315  nosupdm  33317  nosupfv  33319  nosupres  33320  nosupbnd1lem1  33321  nosupbnd1lem3  33323  nosupbnd1lem5  33325  nosupbnd1  33327  nosupbnd2lem1  33328  nosupbnd2  33329  slenlt  33344  nocvxminlem  33360  slerec  33390  funpartfv  33519  dfrdg4  33525  nn0prpwlem  33783  nn0prpw  33784  limsucncmpi  33906  limsucncmp  33907  ordcmp  33908  unblimceq0  33959  unbdqndv1  33960  bj-hbntbi  34151  bj-cbvexdv  34237  bj-dtru  34254  bj-ru0  34377  bj-nuliota  34474  topdifinffinlem  34764  topdifinffin  34765  icorempo  34768  relowlpssretop  34781  finxpreclem2  34807  finxpreclem6  34813  wl-ax11-lem8  34989  wl-dfrexf  35012  leceifl  35046  lindsadd  35050  lindsenlbs  35052  matunitlindflem1  35053  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem21  35078  poimirlem23  35080  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem31  35088  poimir  35090  mblfinlem2  35095  mblfinlem3  35096  ismblfin  35098  cnambfre  35105  itg2addnclem  35108  itg2addnclem2  35109  iblabsnclem  35120  ftc1anclem1  35130  areacirc  35150  heibor1lem  35247  heiborlem1  35249  heiborlem6  35254  heiborlem8  35256  heiborlem10  35258  smprngopr  35490  ecin0  35766  ax12inda  36244  riotaclbgBAD  36250  lcvfbr  36316  lcvbr  36317  lsatcv0  36327  l1cvpat  36350  opltcon3b  36500  cvrfval  36564  cvrval  36565  cvrnbtwn  36567  cvrval2  36570  cvrnbtwn2  36571  cvrnbtwn3  36572  cvrcon3b  36573  cvrnbtwn4  36575  atnlt  36609  iscvlat  36619  cvlexch1  36624  hlsuprexch  36677  hlrelat5N  36697  hlrelat2  36699  cvrval5  36711  3dimlem1  36754  3dim1lem5  36762  3dim2  36764  3dim3  36765  llnnlt  36819  islpln5  36831  lplni2  36833  lvolex3N  36834  lplnnle2at  36837  islpln2a  36844  lplnribN  36847  lplnexllnN  36860  lplnnlt  36861  lvoli3  36873  islvol5  36875  lvoli2  36877  lvolnle3at  36878  islvol2aN  36888  4atlem11  36905  lvolnltN  36914  dalawlem15  37181  4atexlemex2  37367  4atex  37372  4atex2-0aOLDN  37374  4atex2-0cOLDN  37376  lautcvr  37388  ltrnfset  37413  ltrnset  37414  ltrnu  37417  trlfset  37456  trlset  37457  trlval2  37459  cdlemd6  37499  cdleme0nex  37586  cdleme18d  37591  cdleme25b  37650  cdleme25cv  37654  cdleme29b  37671  cdleme31fv  37686  cdleme31fv2  37689  cdlemefrs29bpre0  37692  cdlemefr32sn2aw  37700  cdlemefr29bpre0N  37702  cdlemefr29clN  37703  cdlemefr32fvaN  37705  cdlemefr32fva1  37706  cdlemefs32sn1aw  37710  cdleme32fva  37733  cdleme32fvaw  37735  cdleme40v  37765  cdleme42b  37774  cdleme46f2g2  37789  cdleme46f2g1  37790  cdleme48gfv  37833  cdlemg1fvawlemN  37869  cdlemg1cex  37884  cdlemg6d  37917  cdlemm10N  38414  dicffval  38470  dicfval  38471  dicval  38472  dicfnN  38479  dicvalrelN  38481  dihffval  38526  dihfval  38527  dihlsscpre  38530  dvh4dimat  38734  dvh3dimatN  38735  dvh4dimlem  38739  dvh3dim  38742  dvh4dimN  38743  dvh3dim2  38744  dvh3dim3N  38745  mapdcv  38956  mapdh9aOLDN  39086  hdmapfval  39123  hdmapval  39124  hdmapval2  39128  hdmap11lem2  39138  metakunt27  39376  metakunt28  39377  metakunt29  39378  oexpreposd  39487  ellz1  39708  rencldnfilem  39761  jm2.22  39936  jm2.23  39937  wepwsolem  39986  fnwe2lem2  39995  aomclem8  40005  unxpwdom3  40039  ifpbi12  40196  dfsucon  40231  sqrtcvallem1  40331  ss2iundf  40360  frege124d  40462  clsk3nimkb  40743  clsk1indlem1  40748  clsk1independent  40749  ntrneineine1lem  40787  ntrneicls11  40793  clsneiel1  40811  clsneiel2  40812  neicvgel1  40822  neicvgel2  40823  radcnvrat  41018  rusbcALT  41143  en3lpVD  41551  eliin2f  41740  nssd  41741  wessf1ornlem  41811  limsupre2lem  42366  icccncfext  42529  stoweidlem14  42656  stoweidlem34  42676  stoweidlem59  42701  etransclem24  42900  nnfoctbdjlem  43094  nnfoctbdj  43095  hspmbllem2  43266  nsssmfmbflem  43411  eu2ndop1stv  43681  afvfv0bi  43708  afvco2  43732  ndmaovg  43740  ndfatafv2nrn  43777  afv2ndefb  43780  afv2fv0  43821  nelbr  43830  otiunsndisjX  43835  fun2dmnopgexmpl  43840  ltnltne  43856  readdcnnred  43860  resubcnnred  43861  recnmulnred  43862  cndivrenred  43863  ichnreuop  43989  fmtnoinf  44053  odz2prm2pw  44080  prmdvdsfmtnof1lem2  44102  lighneallem3  44125  lighneallem4  44128  requad1  44140  isodd3  44170  bits0ALTV  44197  nfermltl8rev  44260  nfermltl2rev  44261  nfermltlrev  44262  lidldomnnring  44554  zrninitoringc  44695  ztprmneprm  44749  lindepsnlininds  44861  islindeps  44862  lindslinindsimp2lem5  44871  lindslinindsimp2  44872  difmodm1lt  44936  line2ylem  45165  line2xlem  45167  elsetrecslem  45228