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  1085  xorbi12d  1522  equsexvw  2004  cbvexvw  2036  cbvexdvaw  2038  excomimw  2043  hbe1w  2048  19.8aw  2050  exexw  2051  ru0  2127  cbvexv1  2348  cbvex2v  2350  drex1v  2377  cbvex  2407  cbvex2  2420  drex1  2449  eujustALT  2575  necon3abid  2983  neleq12d  3057  rexbiOLD  3111  cbvrexdva  3246  cbvrexfw  3311  rexeqbidvvOLD  3345  cbvrexdva2  3357  cbvrexf  3369  cbvexeqsetf  3503  cgsex4gOLD  3539  ceqsex  3540  ceqsexv  3542  gencbval  3555  spcegf  3605  spc2gv  3613  spc2d  3615  spc3gv  3617  ceqsralbv  3670  cdeqnot  3790  rru  3801  ruOLD  3803  sbcng  3855  sbcrext  3895  cbvrexcsf  3967  difjust  3978  eldif  3986  dfpss3  4112  dfdif3OLD  4141  difeq2  4143  ab0OLD  4403  disjne  4478  pssdifcom1  4513  eldifpr  4680  rexsng  4698  elpwunsn  4707  eldiftp  4710  rexprg  4721  preqsnd  4883  disjxun  5164  nalset  5331  dtruALT2  5388  dtruALT  5406  rexxfrd  5427  rexxfr2d  5429  rexxfrd2  5431  rexxfr  5434  dtruOLD  5461  opthneg  5501  snopeqop  5525  otiunsndisj  5539  poeq1  5610  pocl  5615  poclOLD  5616  swopo  5619  sotric  5637  sotrieq  5638  isso2i  5644  somo  5646  freq1  5667  frirr  5676  fr2nr  5677  frminex  5679  tz7.2  5683  wereu2  5697  poinxp  5780  frinxp  5782  posn  5785  frsn  5787  rexiunxp  5865  rexxpf  5872  intirr  6150  poirr2  6156  cnvpo  6318  dfpo2  6327  predpoirr  6365  predfrirr  6366  frpomin  6372  nordeq  6414  ordtri1  6428  ordtri3  6431  fvmpti  7028  fndmdif  7075  rexrnmptw  7129  rexrnmpt  7131  rexima  7275  2f1fvneq  7297  f1imapss  7303  cbvexfo  7326  nf1const  7340  soisoi  7364  isopolem  7381  weniso  7390  imaeqsalvOLD  7400  canth  7401  riotaclb  7446  rexrnmpo  7590  ndmovg  7633  sorpssuni  7767  sorpssint  7768  fr3nr  7807  dfwe2  7809  ordsucsssuc  7859  nlimsucg  7879  orduninsuc  7880  dfom2  7905  ssnlim  7923  f1oweALT  8013  frxp  8167  poxp  8169  frxp2  8185  frxp3  8192  xpord3inddlem  8195  soseq  8200  suppofssd  8244  suppcoss  8248  wfrlem10OLD  8374  smoword  8422  tz7.48lem  8497  oacan  8604  oaword  8605  omlimcl  8634  omeulem1  8638  nnaword  8683  nnmword  8689  nneob  8712  naddss1  8745  brdifun  8793  swoer  8794  undifixp  8992  boxcutc  8999  2dom  9095  php  9273  phpeqd  9278  nndomog  9279  phpOLD  9285  nndomogOLD  9289  onomeneq  9291  nnsdomo  9297  unxpdomlem2  9314  frfi  9349  unfilem1  9371  supeq3  9518  supeq123d  9519  supmo  9521  eqsup  9525  supub  9528  sup0  9535  suppr  9540  supisolem  9542  supisoex  9543  eqinf  9553  infval  9555  infmo  9564  infpr  9572  infempty  9576  oieq1  9581  ordtypecbv  9586  ordtypelem7  9593  wemapsolem  9619  canthwdom  9648  zfregcl  9663  elirrv  9665  elirr  9666  noinfep  9729  cantnfp1lem3  9749  ttrcltr  9785  rankr1clem  9889  carden2b  10036  domtri2  10058  alephord3  10147  alephdom2  10156  alephval3  10179  dfac9  10206  kmlem2  10221  kmlem4  10223  isfin4  10366  isfin7  10370  fin23lem11  10386  isf32lem5  10426  isf34lem4  10446  fin1a2lem6  10474  fin1a2lem7  10475  fin1a2lem12  10480  itunisuc  10488  ac6n  10554  zorn2g  10572  zornn0g  10574  ttukeylem7  10584  axpowndlem3  10668  axpowndlem4  10669  axregnd  10673  elgch  10691  engch  10697  fpwwe2lem12  10711  fpwwe2  10712  pwfseqlem1  10727  pwfseqlem3  10729  hargch  10742  addnidpi  10970  pinq  10996  nqereu  10998  ltsonq  11038  prlem934  11102  ltexprlem7  11111  addcanpr  11115  prlem936  11116  reclem2pr  11117  reclem3pr  11118  supexpr  11123  ltsosr  11163  supsrlem  11180  axpre-lttri  11234  axpre-sup  11238  xrlenlt  11355  axlttri  11361  axsup  11365  ltne  11387  dedekind  11453  readdcan  11464  leadd1  11758  ltsub1  11786  ltsub2  11787  leord1  11817  lediv1  12160  lemuldiv  12175  lerec  12178  le2msq  12195  infm3  12254  suprnub  12260  infregelb  12279  avgle1  12533  avgle2  12534  znnnlt1  12670  indstr  12981  zsupss  13002  uzsupss  13005  rpneg  13089  xralrple  13267  xleneg  13280  xltadd1  13318  xposdif  13324  xmulneg1  13331  xltmul1  13354  xrsupexmnf  13367  xrinfmexpnf  13368  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  supxrleub  13388  infxrgelb  13397  difreicc  13544  nn0disj  13701  nelfzo  13721  elfznelfzo  13822  fvinim0ffz  13836  injresinjlem  13837  ssnn0fi  14036  leexp2  14221  exp11nnd  14310  hashbnd  14385  hasheni  14397  hashfundm  14491  hashbc  14502  wrdsymb0  14597  swrdnd  14702  swrdnd2  14703  pfxnd0  14736  repswswrd  14832  repswccat  14834  cshwidxmod  14851  cnpart  15289  sqrtlt  15310  limsuplt  15525  rlimrege0  15625  isercoll  15716  efle  16166  odd2np1  16389  sumodd  16436  divalglem7  16447  ndvdsadd  16458  fldivndvdslt  16462  bitsfval  16469  bitsval  16470  bits0  16474  bitsp1  16477  bitsmod  16482  bitscmp  16484  bitsinv1lem  16487  sadadd2lem2  16496  saddisjlem  16510  bitsshft  16521  gcdneg  16568  algcvgblem  16624  lcmneg  16650  isprm3  16730  dvdsnprmd  16737  isprm5  16754  rpexp  16769  phiprmpw  16823  m1dvdsndvds  16845  pythagtrip  16881  pcgcd1  16924  prmpwdvds  16951  prmreclem2  16964  prmreclem3  16965  prmreclem5  16967  prmreclem6  16968  vdwlem6  17033  vdwnnlem2  17043  vdwnnlem3  17044  vdwnn  17045  prmlem0  17153  prmlem1a  17154  divsfval  17607  mrisval  17688  ismri  17689  ismri2dad  17695  cidpropd  17768  cat1lem  18163  plttr  18412  joinval  18447  meetval  18461  acsfiindd  18623  isnsgrp  18761  smndex1n0mnd  18947  mgm2nsgrplem2  18954  sgrp2nmndlem3  18960  symgpssefmnd  19437  symgfix2  19458  pmtrdifellem4  19521  psgnunilem1  19535  psgnunilem5  19536  psgnunilem2  19537  psgnunilem3  19538  pmtrsn  19561  sylow1lem3  19642  sylow2alem2  19660  efgsfo  19781  ablfac1eulem  20116  ablfac1eu  20117  pgpfac1lem1  20118  pgpfac1lem5  20123  nzrunit  20550  zrninitoringc  20698  islbs  21098  lbsind  21102  lbspss  21104  lbspropd  21121  lspsnne1  21142  islbs2  21179  lbsacsbs  21181  lbsextlem1  21183  lbsextlem3  21185  lbsextlem4  21186  lbsextg  21187  frlmlbs  21840  islindf  21855  islinds2  21856  islindf2  21857  lindfind  21859  lindsind  21860  lindfrn  21864  lindfmm  21870  lsslindf  21873  islindf4  21881  opsrtoslem2  22103  psdmul  22193  cply1coe0  22326  cply1coe0bi  22327  mdetunilem7  22645  mdetunilem8  22646  mdetunilem9  22647  maducoeval2  22667  pmatcollpw3fi1lem1  22813  fvmptnn04ifa  22877  fvmptnn04ifc  22879  fvmptnn04ifd  22880  chfacffsupp  22883  chfacfscmul0  22885  chfacfpmmul0  22889  elcls  23102  maxlp  23176  perfi  23184  ordtbaslem  23217  ordtval  23218  ordtbas2  23220  ordtopn1  23223  ordtopn2  23224  ordtcnv  23230  ordtrest  23231  ordtrest2lem  23232  ordtrest2  23233  pnfnei  23249  mnfnei  23250  isreg2  23406  ordthauslem  23412  cmpfi  23437  cmpfii  23438  bwth  23439  nconnsubb  23452  hausdiag  23674  txkgen  23681  kqdisj  23761  ordthmeolem  23830  fbfinnfr  23870  trfbas  23873  fbunfip  23898  fbasrn  23913  trfil3  23917  ufileu  23948  fin1aufil  23961  hausflim  24010  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem2  24082  ptcmplem3  24083  stdbdbl  24551  iccntr  24862  reconnlem2  24868  iccpnfcnv  24994  xrhmeo  24996  lebnumlem1  25012  lebnumlem2  25013  lebnumlem3  25014  bcthlem4  25380  minveclem3b  25481  ivthlem2  25506  ivthlem3  25507  mbfmax  25703  mbfposr  25706  i1fd  25735  mbfi1fseqlem4  25773  itg2splitlem  25803  itg2monolem1  25805  itg2cnlem1  25816  dvne0  26070  lhop1lem  26072  deg1nn0clb  26149  dgrle  26302  coemulhi  26313  aaliou3lem9  26410  cos11  26593  logleb  26663  argrege0  26671  logdivle  26682  ellogdm  26699  cxple  26755  cxplt2  26758  cxple3  26761  isosctrlem1  26879  atandm  26937  atans2  26992  atantayl2  26999  eldmgm  27083  ftalem7  27140  isppw2  27176  musum  27252  dchrsum2  27330  bposlem1  27346  lgsmod  27385  lgsdir2lem2  27388  lgsdir2  27392  lgsne0  27397  lgsprme0  27401  gausslemma2dlem4  27431  lgsquadlem1  27442  2lgslem3  27466  2lgsoddprm  27478  2sq2  27495  addsqrexnreu  27504  rpvmasumlem  27549  padicabv  27692  ostth3  27700  ostth  27701  noextenddif  27731  nodenselem4  27750  nodenselem5  27751  nodenselem7  27753  nolt02o  27758  nogt01o  27759  noresle  27760  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd1  27777  nosupbnd2lem1  27778  nosupbnd2  27779  noinfcbv  27780  noinfdm  27782  noinffv  27784  noinfres  27785  noinfbnd1lem1  27786  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd1  27792  noinfbnd2lem1  27793  noinfbnd2  27794  slenlt  27815  sltne  27833  nocvxminlem  27840  slerec  27882  cuteq1  27896  newbday  27958  sltlpss  27963  cofcutr  27976  lrrecfr  27994  addsval  28013  sltadd2  28042  sleneg  28096  slesubsubbd  28134  slesubsub2bd  28135  slesubsub3bd  28136  slesubaddd  28141  sltmul2  28215  slemul2d  28218  slemul1d  28219  istrkgld  28485  axtgupdim2  28497  tglowdim2l  28676  axlowdimlem16  28990  axlowdim2  28993  axlowdim  28994  numedglnl  29179  usgredg2v  29262  lfuhgr1v0e  29289  cusgrfi  29494  vtxd0nedgb  29524  vtxduhgr0edgnel  29530  1loopgrnb0  29538  1hevtxdg0  29541  vtxdgoddnumeven  29589  wlkp1lem1  29709  wlkp1lem2  29710  wlkp1lem5  29713  crctcsh  29857  clwlkclwwlklem2a4  30029  eupth2eucrct  30249  eupth2lem3lem3  30262  eupth2lem3lem4  30263  eupth2lem3lem6  30265  eupth2lem3lem7  30266  eupth2lems  30270  eupth2  30271  konigsberglem4  30287  nfrgr2v  30304  frgrwopreglem3  30346  fusgr2wsp2nb  30366  frgrreggt1  30425  friendshipgt3  30430  lpni  30512  nmobndseqi  30811  minvecolem5  30913  chpsscon3  31535  chnle  31546  nonbooli  31683  pjnel  31758  specval  31930  nmcfnlbi  32084  stri  32289  hstri  32297  cvbr  32314  cvcon3  32316  chcv1  32387  cvexchlem  32400  chrelat2  32402  nelun  32542  elpreq  32558  nelpr  32559  ifeqeqx  32565  nfpconfp  32651  suppiniseg  32698  isoun  32713  suppss3  32738  xrge0infss  32767  infxrge0gelb  32773  eliccelico  32782  elicoelioo  32783  nndiffz1  32791  hashgt1  32815  expgt0b  32820  nn0min  32824  ccatws1f1o  32918  toslublem  32945  tosglblem  32947  pmtrcnel  33082  cycpmco2  33126  isarchi2  33165  archiabl  33178  0nellinds  33363  lindssn  33371  lindfpropd  33375  ssdifidlprm  33451  mxidlirred  33465  ssmxidl  33467  lbslsat  33629  lindsunlem  33637  rtelextdg2lem  33717  ordtcnvNEW  33866  ordtrestNEW  33867  ordtrest2NEWlem  33868  ordtrest2NEW  33869  ordtconnlem1  33870  xrge0iifcnv  33879  esumpcvgval  34042  esum2d  34057  ddemeas  34200  omssubadd  34265  oddpwdc  34319  eulerpartlems  34325  eulerpartlemf  34335  eulerpartlemt  34336  eulerpartlemr  34339  eulerpartlemgvv  34341  eulerpartlemn  34346  ballotlemfc0  34457  ballotlemfcc  34458  ballotlem4  34463  ballotlemimin  34470  ballotlem7  34500  plymulx  34525  signsply0  34528  reprinfz1  34599  reprpmtf1o  34603  reprdifc  34604  hgt750lema  34634  hgt750leme  34635  istrkg2d  34643  bnj23  34694  bnj1185  34769  bnj1228  34987  bnj1388  35009  bnj1417  35017  nummin  35067  axnulg  35068  revwlk  35092  isacycgr  35113  acycgr0v  35116  prclisacycgr  35119  erdszelem10  35168  satf0n0  35346  fmlaomn0  35358  fmlasucdisj  35367  satfv1fvfmla1  35391  satefvfmla1  35393  ismfs  35517  mvtinf  35523  untelirr  35670  untsucf  35672  untangtr  35676  dfon2lem3  35749  dfon2lem4  35750  dfon2lem7  35753  dfon2lem9  35755  distel  35767  funpartfv  35909  dfrdg4  35915  nn0prpwlem  36288  nn0prpw  36289  limsucncmpi  36411  limsucncmp  36412  ordcmp  36413  weiunlem2  36429  weiunfrlem  36430  weiunfr  36433  unblimceq0  36473  unbdqndv1  36474  bj-hbntbi  36670  bj-equsexvwd  36747  bj-cbvexdv  36766  bj-ru1  36909  bj-nuliota  37023  topdifinffinlem  37313  topdifinffin  37314  icorempo  37317  relowlpssretop  37330  finxpreclem2  37356  finxpreclem6  37362  wl-issetft  37536  wl-ax11-lem8  37546  leceifl  37569  lindsadd  37573  lindsenlbs  37575  matunitlindflem1  37576  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem21  37601  poimirlem23  37603  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem31  37611  poimir  37613  mblfinlem2  37618  mblfinlem3  37619  ismblfin  37621  cnambfre  37628  itg2addnclem  37631  itg2addnclem2  37632  iblabsnclem  37643  ftc1anclem1  37653  areacirc  37673  heibor1lem  37769  heiborlem1  37771  heiborlem6  37776  heiborlem8  37778  heiborlem10  37780  smprngopr  38012  ecin0  38308  ax12inda  38904  riotaclbgBAD  38910  lcvfbr  38976  lcvbr  38977  lsatcv0  38987  l1cvpat  39010  opltcon3b  39160  cvrfval  39224  cvrval  39225  cvrnbtwn  39227  cvrval2  39230  cvrnbtwn2  39231  cvrnbtwn3  39232  cvrcon3b  39233  cvrnbtwn4  39235  atnlt  39269  iscvlat  39279  cvlexch1  39284  hlsuprexch  39338  hlrelat5N  39358  hlrelat2  39360  cvrval5  39372  3dimlem1  39415  3dim1lem5  39423  3dim2  39425  3dim3  39426  llnnlt  39480  islpln5  39492  lplni2  39494  lvolex3N  39495  lplnnle2at  39498  islpln2a  39505  lplnribN  39508  lplnexllnN  39521  lplnnlt  39522  lvoli3  39534  islvol5  39536  lvoli2  39538  lvolnle3at  39539  islvol2aN  39549  4atlem11  39566  lvolnltN  39575  dalawlem15  39842  4atexlemex2  40028  4atex  40033  4atex2-0aOLDN  40035  4atex2-0cOLDN  40037  lautcvr  40049  ltrnfset  40074  ltrnset  40075  ltrnu  40078  trlfset  40117  trlset  40118  trlval2  40120  cdlemd6  40160  cdleme0nex  40247  cdleme18d  40252  cdleme25b  40311  cdleme25cv  40315  cdleme29b  40332  cdleme31fv  40347  cdleme31fv2  40350  cdlemefrs29bpre0  40353  cdlemefr32sn2aw  40361  cdlemefr29bpre0N  40363  cdlemefr29clN  40364  cdlemefr32fvaN  40366  cdlemefr32fva1  40367  cdlemefs32sn1aw  40371  cdleme32fva  40394  cdleme32fvaw  40396  cdleme40v  40426  cdleme42b  40435  cdleme46f2g2  40450  cdleme46f2g1  40451  cdleme48gfv  40494  cdlemg1fvawlemN  40530  cdlemg1cex  40545  cdlemg6d  40578  cdlemm10N  41075  dicffval  41131  dicfval  41132  dicval  41133  dicfnN  41140  dicvalrelN  41142  dihffval  41187  dihfval  41188  dihlsscpre  41191  dvh4dimat  41395  dvh3dimatN  41396  dvh4dimlem  41400  dvh3dim  41403  dvh4dimN  41404  dvh3dim2  41405  dvh3dim3N  41406  mapdcv  41617  mapdh9aOLDN  41747  hdmapfval  41784  hdmapval  41785  hdmapval2  41789  hdmap11lem2  41799  dvrelog2b  42023  aks4d1p4  42036  aks4d1p5  42037  aks4d1p7  42040  aks4d1p8d2  42042  aks4d1p8  42044  aks4d1  42046  aks6d1c2p2  42076  hashnexinj  42085  rspcsbnea  42088  aks6d1c5  42096  aks6d1c6lem3  42129  aks6d1c7  42141  metakunt27  42188  metakunt28  42189  metakunt29  42190  supinf  42237  oexpreposd  42309  flt4lem7  42614  nna4b4nsq  42615  ellz1  42723  rencldnfilem  42776  jm2.22  42952  jm2.23  42953  wepwsolem  42999  fnwe2lem2  43008  aomclem8  43018  unxpwdom3  43052  onsupmaxb  43200  onexlimgt  43204  onsupeqnmax  43208  onov0suclim  43236  oaordnr  43258  omnord1  43267  oenord1  43278  oaomoencom  43279  oenass  43281  cantnfresb  43286  tfsnfin  43314  ralopabb  43373  nlimsuc  43403  ifpbi12  43450  dfsucon  43485  sqrtcvallem1  43593  ss2iundf  43621  frege124d  43723  clsk3nimkb  44002  clsk1indlem1  44007  clsk1independent  44008  ntrneineine1lem  44046  ntrneicls11  44052  clsneiel1  44070  clsneiel2  44071  neicvgel1  44081  neicvgel2  44082  radcnvrat  44283  rusbcALT  44408  en3lpVD  44816  eliin2f  45006  nssd  45007  wessf1ornlem  45092  rexanuz2nf  45408  limsupre2lem  45645  icccncfext  45808  stoweidlem14  45935  stoweidlem34  45955  stoweidlem59  45980  etransclem24  46179  nnfoctbdjlem  46376  nnfoctbdj  46377  hspmbllem2  46548  nsssmfmbflem  46699  fsetsnprcnex  46970  eu2ndop1stv  47040  afvfv0bi  47067  afvco2  47091  ndmaovg  47099  ndfatafv2nrn  47136  afv2ndefb  47139  afv2fv0  47180  nelbr  47189  otiunsndisjX  47194  fun2dmnopgexmpl  47199  ltnltne  47214  readdcnnred  47218  resubcnnred  47219  recnmulnred  47220  cndivrenred  47221  ichnreuop  47346  fmtnoinf  47410  odz2prm2pw  47437  prmdvdsfmtnof1lem2  47459  lighneallem3  47481  lighneallem4  47484  requad1  47496  isodd3  47526  bits0ALTV  47553  nfermltl8rev  47616  nfermltl2rev  47617  nfermltlrev  47618  usgrexmpl12ngric  47853  lidldomnnring  47959  ztprmneprm  48072  lindepsnlininds  48181  islindeps  48182  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  difmodm1lt  48256  line2ylem  48485  line2xlem  48487  map0cor  48568  elsetrecslem  48791