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  835  con3ALT  1085  xorbi12d  1525  equsexvw  2004  cbvexvw  2036  cbvexdvaw  2038  excomimw  2043  hbe1w  2048  19.8aw  2050  exexw  2051  ru0  2127  cbvexv1  2344  cbvex2v  2346  drex1v  2374  cbvex  2404  cbvex2  2417  drex1  2446  eujustALT  2572  necon3abid  2977  neleq12d  3051  rexbiOLD  3105  cbvrexdva  3240  cbvrexfw  3305  rexeqbidvvOLD  3337  cbvrexdva2  3349  cbvrexf  3361  cbvexeqsetf  3495  cgsex4gOLD  3529  ceqsex  3530  ceqsexv  3532  gencbval  3543  spcegf  3592  spc2gv  3600  spc2d  3602  spc3gv  3604  ceqsralbv  3657  cdeqnot  3774  rru  3785  ruOLD  3787  sbcng  3836  sbcrext  3873  cbvrexcsf  3942  difjust  3953  eldif  3961  dfpss3  4089  dfdif3OLD  4118  difeq2  4120  disjne  4455  pssdifcom1  4490  eldifpr  4658  rexsng  4676  elpwunsn  4684  eldiftp  4687  rexprg  4697  preqsnd  4859  disjxun  5141  nalset  5313  dtruALT2  5370  dtruALT  5388  rexxfrd  5409  rexxfr2d  5411  rexxfrd2  5413  rexxfr  5416  dtruOLD  5446  opthneg  5486  snopeqop  5511  otiunsndisj  5525  poeq1  5595  pocl  5600  swopo  5603  sotric  5622  sotrieq  5623  isso2i  5629  somo  5631  freq1  5652  frirr  5661  fr2nr  5662  frminex  5664  tz7.2  5668  wereu2  5682  poinxp  5766  frinxp  5768  posn  5771  frsn  5773  rexiunxp  5851  rexxpf  5858  intirr  6138  poirr2  6144  cnvpo  6307  dfpo2  6316  predpoirr  6354  predfrirr  6355  frpomin  6361  nordeq  6403  ordtri1  6417  ordtri3  6420  fvmpti  7015  fndmdif  7062  rexrnmptw  7115  rexrnmpt  7117  rexima  7258  2f1fvneq  7280  f1imapss  7286  f1ounsn  7292  cbvexfo  7310  nf1const  7324  soisoi  7348  isopolem  7365  weniso  7374  imaeqsalvOLD  7384  canth  7385  riotaclb  7429  rexrnmpo  7573  ndmovg  7616  sorpssuni  7752  sorpssint  7753  fr3nr  7792  dfwe2  7794  ordsucsssuc  7843  nlimsucg  7863  orduninsuc  7864  dfom2  7889  ssnlim  7907  resf1extb  7956  f1oweALT  7997  frxp  8151  poxp  8153  frxp2  8169  frxp3  8176  xpord3inddlem  8179  soseq  8184  suppofssd  8228  suppcoss  8232  wfrlem10OLD  8358  smoword  8406  tz7.48lem  8481  oacan  8586  oaword  8587  omlimcl  8616  omeulem1  8620  nnaword  8665  nnmword  8671  nneob  8694  naddss1  8727  brdifun  8775  swoer  8776  undifixp  8974  boxcutc  8981  2dom  9070  php  9247  phpeqd  9252  nndomog  9253  phpOLD  9259  nndomogOLD  9263  onomeneq  9265  nnsdomo  9270  unxpdomlem2  9287  frfi  9321  unfilem1  9343  supeq3  9489  supeq123d  9490  supmo  9492  eqsup  9496  supub  9499  sup0  9506  suppr  9511  supisolem  9513  supisoex  9514  eqinf  9524  infval  9526  infmo  9535  infpr  9543  infempty  9547  oieq1  9552  ordtypecbv  9557  ordtypelem7  9564  wemapsolem  9590  canthwdom  9619  zfregcl  9634  elirrv  9636  elirr  9637  noinfep  9700  cantnfp1lem3  9720  ttrcltr  9756  rankr1clem  9860  carden2b  10007  domtri2  10029  alephord3  10118  alephdom2  10127  alephval3  10150  dfac9  10177  kmlem2  10192  kmlem4  10194  isfin4  10337  isfin7  10341  fin23lem11  10357  isf32lem5  10397  isf34lem4  10417  fin1a2lem6  10445  fin1a2lem7  10446  fin1a2lem12  10451  itunisuc  10459  ac6n  10525  zorn2g  10543  zornn0g  10545  ttukeylem7  10555  axpowndlem3  10639  axpowndlem4  10640  axregnd  10644  elgch  10662  engch  10668  fpwwe2lem12  10682  fpwwe2  10683  pwfseqlem1  10698  pwfseqlem3  10700  hargch  10713  addnidpi  10941  pinq  10967  nqereu  10969  ltsonq  11009  prlem934  11073  ltexprlem7  11082  addcanpr  11086  prlem936  11087  reclem2pr  11088  reclem3pr  11089  supexpr  11094  ltsosr  11134  supsrlem  11151  axpre-lttri  11205  axpre-sup  11209  xrlenlt  11326  axlttri  11332  axsup  11336  ltne  11358  dedekind  11424  readdcan  11435  leadd1  11731  ltsub1  11759  ltsub2  11760  leord1  11790  lediv1  12133  lemuldiv  12148  lerec  12151  le2msq  12168  infm3  12227  suprnub  12233  infregelb  12252  avgle1  12506  avgle2  12507  znnnlt1  12644  indstr  12958  zsupss  12979  uzsupss  12982  rpneg  13067  xralrple  13247  xleneg  13260  xltadd1  13298  xposdif  13304  xmulneg1  13311  xltmul1  13334  xrsupexmnf  13347  xrinfmexpnf  13348  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  supxrleub  13368  infxrgelb  13377  difreicc  13524  nn0disj  13684  nelfzo  13704  elfznelfzo  13811  fvinim0ffz  13825  injresinjlem  13826  ssnn0fi  14026  leexp2  14211  exp11nnd  14300  hashbnd  14375  hasheni  14387  hashfundm  14481  hashbc  14492  wrdsymb0  14587  swrdnd  14692  swrdnd2  14693  pfxnd0  14726  repswswrd  14822  repswccat  14824  cshwidxmod  14841  cnpart  15279  sqrtlt  15300  limsuplt  15515  rlimrege0  15615  isercoll  15704  efle  16154  odd2np1  16378  sumodd  16425  divalglem7  16436  ndvdsadd  16447  fldivndvdslt  16453  bitsfval  16460  bitsval  16461  bits0  16465  bitsp1  16468  bitsmod  16473  bitscmp  16475  bitsinv1lem  16478  sadadd2lem2  16487  saddisjlem  16501  bitsshft  16512  gcdneg  16559  algcvgblem  16614  lcmneg  16640  isprm3  16720  dvdsnprmd  16727  isprm5  16744  rpexp  16759  phiprmpw  16813  m1dvdsndvds  16836  pythagtrip  16872  pcgcd1  16915  prmpwdvds  16942  prmreclem2  16955  prmreclem3  16956  prmreclem5  16958  prmreclem6  16959  vdwlem6  17024  vdwnnlem2  17034  vdwnnlem3  17035  vdwnn  17036  prmlem0  17143  prmlem1a  17144  divsfval  17592  mrisval  17673  ismri  17674  ismri2dad  17680  cidpropd  17753  cat1lem  18141  plttr  18387  joinval  18422  meetval  18436  acsfiindd  18598  isnsgrp  18736  smndex1n0mnd  18925  mgm2nsgrplem2  18932  sgrp2nmndlem3  18938  symgpssefmnd  19413  symgfix2  19434  pmtrdifellem4  19497  psgnunilem1  19511  psgnunilem5  19512  psgnunilem2  19513  psgnunilem3  19514  pmtrsn  19537  sylow1lem3  19618  sylow2alem2  19636  efgsfo  19757  ablfac1eulem  20092  ablfac1eu  20093  pgpfac1lem1  20094  pgpfac1lem5  20099  nzrunit  20524  zrninitoringc  20676  islbs  21075  lbsind  21079  lbspss  21081  lbspropd  21098  lspsnne1  21119  islbs2  21156  lbsacsbs  21158  lbsextlem1  21160  lbsextlem3  21162  lbsextlem4  21163  lbsextg  21164  frlmlbs  21817  islindf  21832  islinds2  21833  islindf2  21834  lindfind  21836  lindsind  21837  lindfrn  21841  lindfmm  21847  lsslindf  21850  islindf4  21858  opsrtoslem2  22080  psdmul  22170  cply1coe0  22305  cply1coe0bi  22306  mdetunilem7  22624  mdetunilem8  22625  mdetunilem9  22626  maducoeval2  22646  pmatcollpw3fi1lem1  22792  fvmptnn04ifa  22856  fvmptnn04ifc  22858  fvmptnn04ifd  22859  chfacffsupp  22862  chfacfscmul0  22864  chfacfpmmul0  22868  elcls  23081  maxlp  23155  perfi  23163  ordtbaslem  23196  ordtval  23197  ordtbas2  23199  ordtopn1  23202  ordtopn2  23203  ordtcnv  23209  ordtrest  23210  ordtrest2lem  23211  ordtrest2  23212  pnfnei  23228  mnfnei  23229  isreg2  23385  ordthauslem  23391  cmpfi  23416  cmpfii  23417  bwth  23418  nconnsubb  23431  hausdiag  23653  txkgen  23660  kqdisj  23740  ordthmeolem  23809  fbfinnfr  23849  trfbas  23852  fbunfip  23877  fbasrn  23892  trfil3  23896  ufileu  23927  fin1aufil  23940  hausflim  23989  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  ptcmplem2  24061  ptcmplem3  24062  stdbdbl  24530  iccntr  24843  reconnlem2  24849  iccpnfcnv  24975  xrhmeo  24977  lebnumlem1  24993  lebnumlem2  24994  lebnumlem3  24995  bcthlem4  25361  minveclem3b  25462  ivthlem2  25487  ivthlem3  25488  mbfmax  25684  mbfposr  25687  i1fd  25716  mbfi1fseqlem4  25753  itg2splitlem  25783  itg2monolem1  25785  itg2cnlem1  25796  dvne0  26050  lhop1lem  26052  deg1nn0clb  26129  dgrle  26282  coemulhi  26293  aaliou3lem9  26392  cos11  26575  logleb  26645  argrege0  26653  logdivle  26664  ellogdm  26681  cxple  26737  cxplt2  26740  cxple3  26743  isosctrlem1  26861  atandm  26919  atans2  26974  atantayl2  26981  eldmgm  27065  ftalem7  27122  isppw2  27158  musum  27234  dchrsum2  27312  bposlem1  27328  lgsmod  27367  lgsdir2lem2  27370  lgsdir2  27374  lgsne0  27379  lgsprme0  27383  gausslemma2dlem4  27413  lgsquadlem1  27424  2lgslem3  27448  2lgsoddprm  27460  2sq2  27477  addsqrexnreu  27486  rpvmasumlem  27531  padicabv  27674  ostth3  27682  ostth  27683  noextenddif  27713  nodenselem4  27732  nodenselem5  27733  nodenselem7  27735  nolt02o  27740  nogt01o  27741  noresle  27742  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupdm  27749  nosupfv  27751  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd1  27759  nosupbnd2lem1  27760  nosupbnd2  27761  noinfcbv  27762  noinfdm  27764  noinffv  27766  noinfres  27767  noinfbnd1lem1  27768  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd1  27774  noinfbnd2lem1  27775  noinfbnd2  27776  slenlt  27797  sltne  27815  nocvxminlem  27822  slerec  27864  cuteq1  27878  newbday  27940  sltlpss  27945  cofcutr  27958  lrrecfr  27976  addsval  27995  sltadd2  28024  sleneg  28078  slesubsubbd  28116  slesubsub2bd  28117  slesubsub3bd  28118  slesubaddd  28123  sltmul2  28197  slemul2d  28200  slemul1d  28201  istrkgld  28467  axtgupdim2  28479  tglowdim2l  28658  axlowdimlem16  28972  axlowdim2  28975  axlowdim  28976  numedglnl  29161  usgredg2v  29244  lfuhgr1v0e  29271  cusgrfi  29476  vtxd0nedgb  29506  vtxduhgr0edgnel  29512  1loopgrnb0  29520  1hevtxdg0  29523  vtxdgoddnumeven  29571  wlkp1lem1  29691  wlkp1lem2  29692  wlkp1lem5  29695  dfpth2  29749  crctcsh  29844  clwlkclwwlklem2a4  30016  eupth2eucrct  30236  eupth2lem3lem3  30249  eupth2lem3lem4  30250  eupth2lem3lem6  30252  eupth2lem3lem7  30253  eupth2lems  30257  eupth2  30258  konigsberglem4  30274  nfrgr2v  30291  frgrwopreglem3  30333  fusgr2wsp2nb  30353  frgrreggt1  30412  friendshipgt3  30417  lpni  30499  nmobndseqi  30798  minvecolem5  30900  chpsscon3  31522  chnle  31533  nonbooli  31670  pjnel  31745  specval  31917  nmcfnlbi  32071  stri  32276  hstri  32284  cvbr  32301  cvcon3  32303  chcv1  32374  cvexchlem  32387  chrelat2  32389  nelun  32532  elpreq  32548  nelpr  32549  ifeqeqx  32555  nfpconfp  32642  suppiniseg  32695  isoun  32711  suppss3  32735  xrge0infss  32764  infxrge0gelb  32770  eliccelico  32779  elicoelioo  32780  nndiffz1  32788  hashgt1  32812  expgt0b  32818  nn0min  32822  ccatws1f1o  32936  toslublem  32962  tosglblem  32964  pmtrcnel  33109  cycpmco2  33153  isarchi2  33192  archiabl  33205  elrgspnlem2  33247  elrgspnlem3  33248  0nellinds  33398  lindssn  33406  lindfpropd  33410  ssdifidlprm  33486  mxidlirred  33500  ssmxidl  33502  lbslsat  33667  lindsunlem  33675  rtelextdg2lem  33767  ordtcnvNEW  33919  ordtrestNEW  33920  ordtrest2NEWlem  33921  ordtrest2NEW  33922  ordtconnlem1  33923  xrge0iifcnv  33932  esumpcvgval  34079  esum2d  34094  ddemeas  34237  omssubadd  34302  oddpwdc  34356  eulerpartlems  34362  eulerpartlemf  34372  eulerpartlemt  34373  eulerpartlemr  34376  eulerpartlemgvv  34378  eulerpartlemn  34383  ballotlemfc0  34495  ballotlemfcc  34496  ballotlem4  34501  ballotlemimin  34508  ballotlem7  34538  plymulx  34563  signsply0  34566  reprinfz1  34637  reprpmtf1o  34641  reprdifc  34642  hgt750lema  34672  hgt750leme  34673  istrkg2d  34681  bnj23  34732  bnj1185  34807  bnj1228  35025  bnj1388  35047  bnj1417  35055  nummin  35105  axnulg  35106  revwlk  35130  isacycgr  35150  acycgr0v  35153  prclisacycgr  35156  erdszelem10  35205  satf0n0  35383  fmlaomn0  35395  fmlasucdisj  35404  satfv1fvfmla1  35428  satefvfmla1  35430  ismfs  35554  mvtinf  35560  untelirr  35708  untsucf  35710  untangtr  35714  dfon2lem3  35786  dfon2lem4  35787  dfon2lem7  35790  dfon2lem9  35792  distel  35804  funpartfv  35946  dfrdg4  35952  nn0prpwlem  36323  nn0prpw  36324  limsucncmpi  36446  limsucncmp  36447  ordcmp  36448  weiunlem2  36464  weiunfrlem  36465  weiunfr  36468  unblimceq0  36508  unbdqndv1  36509  bj-hbntbi  36705  bj-equsexvwd  36782  bj-cbvexdv  36801  bj-ru1  36944  bj-nuliota  37058  topdifinffinlem  37348  topdifinffin  37349  icorempo  37352  relowlpssretop  37365  finxpreclem2  37391  finxpreclem6  37397  wl-issetft  37583  wl-ax11-lem8  37593  leceifl  37616  lindsadd  37620  lindsenlbs  37622  matunitlindflem1  37623  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem21  37648  poimirlem23  37650  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem31  37658  poimir  37660  mblfinlem2  37665  mblfinlem3  37666  ismblfin  37668  cnambfre  37675  itg2addnclem  37678  itg2addnclem2  37679  iblabsnclem  37690  ftc1anclem1  37700  areacirc  37720  heibor1lem  37816  heiborlem1  37818  heiborlem6  37823  heiborlem8  37825  heiborlem10  37827  smprngopr  38059  ecin0  38353  ax12inda  38949  riotaclbgBAD  38955  lcvfbr  39021  lcvbr  39022  lsatcv0  39032  l1cvpat  39055  opltcon3b  39205  cvrfval  39269  cvrval  39270  cvrnbtwn  39272  cvrval2  39275  cvrnbtwn2  39276  cvrnbtwn3  39277  cvrcon3b  39278  cvrnbtwn4  39280  atnlt  39314  iscvlat  39324  cvlexch1  39329  hlsuprexch  39383  hlrelat5N  39403  hlrelat2  39405  cvrval5  39417  3dimlem1  39460  3dim1lem5  39468  3dim2  39470  3dim3  39471  llnnlt  39525  islpln5  39537  lplni2  39539  lvolex3N  39540  lplnnle2at  39543  islpln2a  39550  lplnribN  39553  lplnexllnN  39566  lplnnlt  39567  lvoli3  39579  islvol5  39581  lvoli2  39583  lvolnle3at  39584  islvol2aN  39594  4atlem11  39611  lvolnltN  39620  dalawlem15  39887  4atexlemex2  40073  4atex  40078  4atex2-0aOLDN  40080  4atex2-0cOLDN  40082  lautcvr  40094  ltrnfset  40119  ltrnset  40120  ltrnu  40123  trlfset  40162  trlset  40163  trlval2  40165  cdlemd6  40205  cdleme0nex  40292  cdleme18d  40297  cdleme25b  40356  cdleme25cv  40360  cdleme29b  40377  cdleme31fv  40392  cdleme31fv2  40395  cdlemefrs29bpre0  40398  cdlemefr32sn2aw  40406  cdlemefr29bpre0N  40408  cdlemefr29clN  40409  cdlemefr32fvaN  40411  cdlemefr32fva1  40412  cdlemefs32sn1aw  40416  cdleme32fva  40439  cdleme32fvaw  40441  cdleme40v  40471  cdleme42b  40480  cdleme46f2g2  40495  cdleme46f2g1  40496  cdleme48gfv  40539  cdlemg1fvawlemN  40575  cdlemg1cex  40590  cdlemg6d  40623  cdlemm10N  41120  dicffval  41176  dicfval  41177  dicval  41178  dicfnN  41185  dicvalrelN  41187  dihffval  41232  dihfval  41233  dihlsscpre  41236  dvh4dimat  41440  dvh3dimatN  41441  dvh4dimlem  41445  dvh3dim  41448  dvh4dimN  41449  dvh3dim2  41450  dvh3dim3N  41451  mapdcv  41662  mapdh9aOLDN  41792  hdmapfval  41829  hdmapval  41830  hdmapval2  41834  hdmap11lem2  41844  dvrelog2b  42067  aks4d1p4  42080  aks4d1p5  42081  aks4d1p7  42084  aks4d1p8d2  42086  aks4d1p8  42088  aks4d1  42090  aks6d1c2p2  42120  hashnexinj  42129  rspcsbnea  42132  aks6d1c5  42140  aks6d1c6lem3  42173  aks6d1c7  42185  metakunt27  42232  metakunt28  42233  metakunt29  42234  supinf  42283  oexpreposd  42357  flt4lem7  42669  nna4b4nsq  42670  ellz1  42778  rencldnfilem  42831  jm2.22  43007  jm2.23  43008  wepwsolem  43054  fnwe2lem2  43063  aomclem8  43073  unxpwdom3  43107  onsupmaxb  43251  onexlimgt  43255  onsupeqnmax  43259  onov0suclim  43287  oaordnr  43309  omnord1  43318  oenord1  43329  oaomoencom  43330  oenass  43332  cantnfresb  43337  tfsnfin  43365  ralopabb  43424  nlimsuc  43454  ifpbi12  43501  dfsucon  43536  sqrtcvallem1  43644  ss2iundf  43672  frege124d  43774  clsk3nimkb  44053  clsk1indlem1  44058  clsk1independent  44059  ntrneineine1lem  44097  ntrneicls11  44103  clsneiel1  44121  clsneiel2  44122  neicvgel1  44132  neicvgel2  44133  radcnvrat  44333  rusbcALT  44458  en3lpVD  44865  0elaxnul  45000  omssaxinf2  45005  eliin2f  45109  nssd  45110  wessf1ornlem  45190  rexanuz2nf  45503  limsupre2lem  45739  icccncfext  45902  stoweidlem14  46029  stoweidlem34  46049  stoweidlem59  46074  etransclem24  46273  nnfoctbdjlem  46470  nnfoctbdj  46471  hspmbllem2  46642  nsssmfmbflem  46793  fsetsnprcnex  47067  eu2ndop1stv  47137  afvfv0bi  47164  afvco2  47188  ndmaovg  47196  ndfatafv2nrn  47233  afv2ndefb  47236  afv2fv0  47277  nelbr  47286  otiunsndisjX  47291  fun2dmnopgexmpl  47296  ltnltne  47311  readdcnnred  47315  resubcnnred  47316  recnmulnred  47317  cndivrenred  47318  ichnreuop  47459  fmtnoinf  47523  odz2prm2pw  47550  prmdvdsfmtnof1lem2  47572  lighneallem3  47594  lighneallem4  47597  requad1  47609  isodd3  47639  bits0ALTV  47666  nfermltl8rev  47729  nfermltl2rev  47730  nfermltlrev  47731  isubgr3stgrlem3  47935  usgrexmpl12ngric  47997  lidldomnnring  48152  ztprmneprm  48263  lindepsnlininds  48369  islindeps  48370  lindslinindsimp2lem5  48379  lindslinindsimp2  48380  difmodm1lt  48443  line2ylem  48672  line2xlem  48674  map0cor  48764  fulltermc2  49144  elsetrecslem  49218