Theorem notbid 317

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

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

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 206

This theorem is referenced by:  notbi  318  annotanannot  831  ifpbi123dOLD  1077  con3ALT  1083  xorbi12d  1519  norassOLD  1536  equsexvw  2009  cbvexvw  2041  cbvexdvaw  2043  hbe1w  2052  19.8aw  2054  exexw  2055  cbvexv1  2341  cbvex2v  2344  drex1v  2369  cbvex  2399  cbvex2  2412  drex1  2441  eujustALT  2572  necon3abid  2979  neleq12d  3052  rexbiOLD  3170  rexeqbidvv  3330  cbvrexfw  3360  cbvrexf  3362  cgsex4g  3466  gencbval  3480  spcegf  3521  spc2gv  3529  spc2d  3531  spc3gv  3533  cdeqnot  3698  rru  3709  ru  3710  sbcng  3761  sbcrext  3802  cbvrexcsf  3874  difjust  3885  eldif  3893  dfpss3  4017  dfdif3  4045  difeq2  4047  ab0OLD  4306  disjne  4385  pssdifcom1  4417  eldifpr  4590  rexsng  4607  elpwunsn  4616  eldiftp  4619  rexprg  4629  preqsnd  4786  disjxun  5068  nalset  5232  dtru  5288  dtruALT  5306  rexxfrd  5327  rexxfr2d  5329  rexxfrd2  5331  rexxfr  5334  dtruALT2  5353  opthneg  5390  snopeqop  5414  otiunsndisj  5428  poeq1  5497  pocl  5501  poclOLD  5502  swopo  5505  sotric  5522  sotrieq  5523  isso2i  5529  somo  5531  freq1  5550  frirr  5557  fr2nr  5558  frminex  5560  tz7.2  5564  wereu2  5577  poinxp  5658  frinxp  5660  posn  5663  frsn  5665  rexiunxp  5738  rexxpf  5745  intirr  6012  poirr2  6018  cnvpo  6179  dfpo2  6188  predpoirr  6225  predfrirr  6226  frpomin  6228  nordeq  6270  ordtri1  6284  ordtri3  6287  fvmpti  6856  fndmdif  6901  rexrnmptw  6953  rexrnmpt  6955  2f1fvneq  7114  f1imapss  7120  cbvexfo  7142  nf1const  7156  soisoi  7179  isopolem  7196  weniso  7205  canth  7209  riotaclb  7254  rexrnmpo  7391  ndmovg  7433  sorpssuni  7563  sorpssint  7564  fr3nr  7600  dfwe2  7602  ordsucsssuc  7645  nlimsucg  7664  orduninsuc  7665  dfom2  7689  ssnlim  7707  f1oweALT  7788  frxp  7938  poxp  7940  suppofssd  7990  suppcoss  7994  wfrlem10OLD  8120  smoword  8168  tz7.48lem  8242  oacan  8341  oaword  8342  omlimcl  8371  omeulem1  8375  nnaword  8420  nnmword  8426  nneob  8446  brdifun  8485  swoer  8486  undifixp  8680  boxcutc  8687  2dom  8774  php  8897  nndomog  8904  nnsdomo  8948  unxpdomlem2  8957  frfi  8989  unfilem1  9008  supeq3  9138  supeq123d  9139  supmo  9141  eqsup  9145  supub  9148  sup0  9155  suppr  9160  supisolem  9162  supisoex  9163  eqinf  9173  infval  9175  infmo  9184  infpr  9192  infempty  9196  oieq1  9201  ordtypecbv  9206  ordtypelem7  9213  wemapsolem  9239  canthwdom  9268  zfregcl  9283  elirrv  9285  elirr  9286  noinfep  9348  cantnfp1lem3  9368  rankr1clem  9509  carden2b  9656  domtri2  9678  alephord3  9765  alephdom2  9774  alephval3  9797  dfac9  9823  kmlem2  9838  kmlem4  9840  isfin4  9984  isfin7  9988  fin23lem11  10004  isf32lem5  10044  isf34lem4  10064  fin1a2lem6  10092  fin1a2lem7  10093  fin1a2lem12  10098  itunisuc  10106  ac6n  10172  zorn2g  10190  zornn0g  10192  ttukeylem7  10202  axpowndlem3  10286  axpowndlem4  10287  axregnd  10291  elgch  10309  engch  10315  fpwwe2lem12  10329  fpwwe2  10330  pwfseqlem1  10345  pwfseqlem3  10347  hargch  10360  addnidpi  10588  pinq  10614  nqereu  10616  ltsonq  10656  prlem934  10720  ltexprlem7  10729  addcanpr  10733  prlem936  10734  reclem2pr  10735  reclem3pr  10736  supexpr  10741  ltsosr  10781  supsrlem  10798  axpre-lttri  10852  axpre-sup  10856  xrlenlt  10971  axlttri  10977  axsup  10981  ltne  11002  dedekind  11068  readdcan  11079  leadd1  11373  ltsub1  11401  ltsub2  11402  leord1  11432  lediv1  11770  lemuldiv  11785  lerec  11788  le2msq  11805  infm3  11864  suprnub  11870  infregelb  11889  avgle1  12143  avgle2  12144  znnnlt1  12277  indstr  12585  zsupss  12606  uzsupss  12609  rpneg  12691  xralrple  12868  xleneg  12881  xltadd1  12919  xposdif  12925  xmulneg1  12932  xltmul1  12955  xrsupexmnf  12968  xrinfmexpnf  12969  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  supxrleub  12989  infxrgelb  12998  difreicc  13145  nn0disj  13301  nelfzo  13321  elfznelfzo  13420  fvinim0ffz  13434  injresinjlem  13435  ssnn0fi  13633  leexp2  13817  hashbnd  13978  hasheni  13990  hashbc  14093  wrdsymb0  14180  swrdnd  14295  swrdnd2  14296  pfxnd0  14329  repswswrd  14425  repswccat  14427  cshwidxmod  14444  cnpart  14879  sqrtlt  14901  limsuplt  15116  rlimrege0  15216  isercoll  15307  efle  15755  odd2np1  15978  sumodd  16025  divalglem7  16036  ndvdsadd  16047  fldivndvdslt  16051  bitsfval  16058  bitsval  16059  bits0  16063  bitsp1  16066  bitsmod  16071  bitscmp  16073  bitsinv1lem  16076  sadadd2lem2  16085  saddisjlem  16099  bitsshft  16110  gcdneg  16157  algcvgblem  16210  lcmneg  16236  isprm3  16316  dvdsnprmd  16323  isprm5  16340  rpexp  16355  phiprmpw  16405  m1dvdsndvds  16427  pythagtrip  16463  pcgcd1  16506  prmpwdvds  16533  prmreclem2  16546  prmreclem3  16547  prmreclem5  16549  prmreclem6  16550  vdwlem6  16615  vdwnnlem2  16625  vdwnnlem3  16626  vdwnn  16627  prmlem0  16735  prmlem1a  16736  divsfval  17175  mrisval  17256  ismri  17257  ismri2dad  17263  cidpropd  17336  cat1lem  17727  plttr  17975  joinval  18010  meetval  18024  acsfiindd  18186  isnsgrp  18294  smndex1n0mnd  18466  mgm2nsgrplem2  18473  sgrp2nmndlem3  18479  symgpssefmnd  18918  symgfix2  18939  pmtrdifellem4  19002  psgnunilem1  19016  psgnunilem5  19017  psgnunilem2  19018  psgnunilem3  19019  pmtrsn  19042  sylow1lem3  19120  sylow2alem2  19138  efgsfo  19260  ablfac1eulem  19590  ablfac1eu  19591  pgpfac1lem1  19592  pgpfac1lem5  19597  islbs  20253  lbsind  20257  lbspss  20259  lbspropd  20276  lspsnne1  20294  islbs2  20331  lbsacsbs  20333  lbsextlem1  20335  lbsextlem3  20337  lbsextlem4  20338  lbsextg  20339  nzrunit  20451  frlmlbs  20914  islindf  20929  islinds2  20930  islindf2  20931  lindfind  20933  lindsind  20934  lindfrn  20938  lindfmm  20944  lsslindf  20947  islindf4  20955  opsrtoslem2  21173  cply1coe0  21380  cply1coe0bi  21381  mdetunilem7  21675  mdetunilem8  21676  mdetunilem9  21677  maducoeval2  21697  pmatcollpw3fi1lem1  21843  fvmptnn04ifa  21907  fvmptnn04ifc  21909  fvmptnn04ifd  21910  chfacffsupp  21913  chfacfscmul0  21915  chfacfpmmul0  21919  elcls  22132  maxlp  22206  perfi  22214  ordtbaslem  22247  ordtval  22248  ordtbas2  22250  ordtopn1  22253  ordtopn2  22254  ordtcnv  22260  ordtrest  22261  ordtrest2lem  22262  ordtrest2  22263  pnfnei  22279  mnfnei  22280  isreg2  22436  ordthauslem  22442  cmpfi  22467  cmpfii  22468  bwth  22469  nconnsubb  22482  hausdiag  22704  txkgen  22711  kqdisj  22791  ordthmeolem  22860  fbfinnfr  22900  trfbas  22903  fbunfip  22928  fbasrn  22943  trfil3  22947  ufileu  22978  fin1aufil  22991  hausflim  23040  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem2  23112  ptcmplem3  23113  stdbdbl  23579  iccntr  23890  reconnlem2  23896  iccpnfcnv  24013  xrhmeo  24015  lebnumlem1  24030  lebnumlem2  24031  lebnumlem3  24032  bcthlem4  24396  minveclem3b  24497  ivthlem2  24521  ivthlem3  24522  mbfmax  24718  mbfposr  24721  i1fd  24750  mbfi1fseqlem4  24788  itg2splitlem  24818  itg2monolem1  24820  itg2cnlem1  24831  dvne0  25080  lhop1lem  25082  deg1nn0clb  25160  dgrle  25309  coemulhi  25320  aaliou3lem9  25415  cos11  25594  logleb  25663  argrege0  25671  logdivle  25682  ellogdm  25699  cxple  25755  cxplt2  25758  cxple3  25761  isosctrlem1  25873  atandm  25931  atans2  25986  atantayl2  25993  eldmgm  26076  ftalem7  26133  isppw2  26169  musum  26245  dchrsum2  26321  bposlem1  26337  lgsmod  26376  lgsdir2lem2  26379  lgsdir2  26383  lgsne0  26388  lgsprme0  26392  gausslemma2dlem4  26422  lgsquadlem1  26433  2lgslem3  26457  2lgsoddprm  26469  2sq2  26486  addsqrexnreu  26495  rpvmasumlem  26540  padicabv  26683  ostth3  26691  ostth  26692  istrkgld  26724  axtgupdim2  26736  tglowdim2l  26915  axlowdimlem16  27228  axlowdim2  27231  axlowdim  27232  numedglnl  27417  usgredg2v  27497  lfuhgr1v0e  27524  cusgrfi  27728  vtxd0nedgb  27758  vtxduhgr0edgnel  27764  1loopgrnb0  27772  1hevtxdg0  27775  vtxdgoddnumeven  27823  wlkp1lem1  27943  wlkp1lem2  27944  wlkp1lem5  27947  crctcsh  28090  clwlkclwwlklem2a4  28262  eupth2eucrct  28482  eupth2lem3lem3  28495  eupth2lem3lem4  28496  eupth2lem3lem6  28498  eupth2lem3lem7  28499  eupth2lems  28503  eupth2  28504  konigsberglem4  28520  nfrgr2v  28537  frgrwopreglem3  28579  fusgr2wsp2nb  28599  frgrreggt1  28658  friendshipgt3  28663  lpni  28743  nmobndseqi  29042  minvecolem5  29144  chpsscon3  29766  chnle  29777  nonbooli  29914  pjnel  29989  specval  30161  nmcfnlbi  30315  stri  30520  hstri  30528  cvbr  30545  cvcon3  30547  chcv1  30618  cvexchlem  30631  chrelat2  30633  nelun  30760  elpreq  30779  nelpr  30780  ifeqeqx  30786  nfpconfp  30868  suppiniseg  30922  isoun  30936  suppss3  30961  xrge0infss  30985  infxrge0gelb  30991  eliccelico  31000  elicoelioo  31001  nndiffz1  31009  hashgt1  31030  nn0min  31036  toslublem  31152  tosglblem  31154  pmtrcnel  31260  cycpmco2  31302  isarchi2  31341  archiabl  31354  0nellinds  31468  lindssn  31475  lindfpropd  31478  ssmxidl  31544  lbslsat  31601  lindsunlem  31607  ordtcnvNEW  31772  ordtrestNEW  31773  ordtrest2NEWlem  31774  ordtrest2NEW  31775  ordtconnlem1  31776  xrge0iifcnv  31785  esumpcvgval  31946  esum2d  31961  ddemeas  32104  omssubadd  32167  oddpwdc  32221  eulerpartlems  32227  eulerpartlemf  32237  eulerpartlemt  32238  eulerpartlemr  32241  eulerpartlemgvv  32243  eulerpartlemn  32248  ballotlemfc0  32359  ballotlemfcc  32360  ballotlem4  32365  ballotlemimin  32372  ballotlem7  32402  plymulx  32427  signsply0  32430  reprinfz1  32502  reprpmtf1o  32506  reprdifc  32507  hgt750lema  32537  hgt750leme  32538  istrkg2d  32546  bnj23  32597  bnj1185  32673  bnj1228  32891  bnj1388  32913  bnj1417  32921  nummin  32963  hashfundm  32974  revwlk  32986  isacycgr  33007  acycgr0v  33010  prclisacycgr  33013  erdszelem10  33062  satf0n0  33240  fmlaomn0  33252  fmlasucdisj  33261  satfv1fvfmla1  33285  satefvfmla1  33287  ismfs  33411  mvtinf  33417  untelirr  33549  untsucf  33551  untangtr  33555  ceqsralv2  33572  imaeqsalv  33594  dfon2lem3  33667  dfon2lem4  33668  dfon2lem7  33671  dfon2lem9  33673  distel  33685  ttrcltr  33702  frxp2  33718  frxp3  33724  soseq  33730  naddss1  33768  noextenddif  33798  nodenselem4  33817  nodenselem5  33818  nodenselem7  33820  nolt02o  33825  nogt01o  33826  noresle  33827  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd1  33844  nosupbnd2lem1  33845  nosupbnd2  33846  noinfcbv  33847  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem1  33853  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd1  33859  noinfbnd2lem1  33860  noinfbnd2  33861  slenlt  33882  nocvxminlem  33899  slerec  33940  newbday  34009  sltlpss  34014  cofcutr  34019  lrrecfr  34027  addsval  34053  funpartfv  34174  dfrdg4  34180  nn0prpwlem  34438  nn0prpw  34439  limsucncmpi  34561  limsucncmp  34562  ordcmp  34563  unblimceq0  34614  unbdqndv1  34615  bj-hbntbi  34813  bj-equsexvwd  34890  bj-cbvexdv  34909  bj-dtru  34926  bj-ru0  35058  bj-nuliota  35155  topdifinffinlem  35445  topdifinffin  35446  icorempo  35449  relowlpssretop  35462  finxpreclem2  35488  finxpreclem6  35494  wl-ax11-lem8  35670  leceifl  35693  lindsadd  35697  lindsenlbs  35699  matunitlindflem1  35700  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem21  35725  poimirlem23  35727  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem31  35735  poimir  35737  mblfinlem2  35742  mblfinlem3  35743  ismblfin  35745  cnambfre  35752  itg2addnclem  35755  itg2addnclem2  35756  iblabsnclem  35767  ftc1anclem1  35777  areacirc  35797  heibor1lem  35894  heiborlem1  35896  heiborlem6  35901  heiborlem8  35903  heiborlem10  35905  smprngopr  36137  ecin0  36411  ax12inda  36889  riotaclbgBAD  36895  lcvfbr  36961  lcvbr  36962  lsatcv0  36972  l1cvpat  36995  opltcon3b  37145  cvrfval  37209  cvrval  37210  cvrnbtwn  37212  cvrval2  37215  cvrnbtwn2  37216  cvrnbtwn3  37217  cvrcon3b  37218  cvrnbtwn4  37220  atnlt  37254  iscvlat  37264  cvlexch1  37269  hlsuprexch  37322  hlrelat5N  37342  hlrelat2  37344  cvrval5  37356  3dimlem1  37399  3dim1lem5  37407  3dim2  37409  3dim3  37410  llnnlt  37464  islpln5  37476  lplni2  37478  lvolex3N  37479  lplnnle2at  37482  islpln2a  37489  lplnribN  37492  lplnexllnN  37505  lplnnlt  37506  lvoli3  37518  islvol5  37520  lvoli2  37522  lvolnle3at  37523  islvol2aN  37533  4atlem11  37550  lvolnltN  37559  dalawlem15  37826  4atexlemex2  38012  4atex  38017  4atex2-0aOLDN  38019  4atex2-0cOLDN  38021  lautcvr  38033  ltrnfset  38058  ltrnset  38059  ltrnu  38062  trlfset  38101  trlset  38102  trlval2  38104  cdlemd6  38144  cdleme0nex  38231  cdleme18d  38236  cdleme25b  38295  cdleme25cv  38299  cdleme29b  38316  cdleme31fv  38331  cdleme31fv2  38334  cdlemefrs29bpre0  38337  cdlemefr32sn2aw  38345  cdlemefr29bpre0N  38347  cdlemefr29clN  38348  cdlemefr32fvaN  38350  cdlemefr32fva1  38351  cdlemefs32sn1aw  38355  cdleme32fva  38378  cdleme32fvaw  38380  cdleme40v  38410  cdleme42b  38419  cdleme46f2g2  38434  cdleme46f2g1  38435  cdleme48gfv  38478  cdlemg1fvawlemN  38514  cdlemg1cex  38529  cdlemg6d  38562  cdlemm10N  39059  dicffval  39115  dicfval  39116  dicval  39117  dicfnN  39124  dicvalrelN  39126  dihffval  39171  dihfval  39172  dihlsscpre  39175  dvh4dimat  39379  dvh3dimatN  39380  dvh4dimlem  39384  dvh3dim  39387  dvh4dimN  39388  dvh3dim2  39389  dvh3dim3N  39390  mapdcv  39601  mapdh9aOLDN  39731  hdmapfval  39768  hdmapval  39769  hdmapval2  39773  hdmap11lem2  39783  dvrelog2b  40002  aks4d1p4  40015  aks4d1p5  40016  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8  40023  aks4d1  40025  metakunt27  40079  metakunt28  40080  metakunt29  40081  oexpreposd  40242  exp11nnd  40245  flt4lem7  40412  nna4b4nsq  40413  ellz1  40505  rencldnfilem  40558  jm2.22  40733  jm2.23  40734  wepwsolem  40783  fnwe2lem2  40792  aomclem8  40802  unxpwdom3  40836  ifpbi12  40993  dfsucon  41028  sqrtcvallem1  41128  ss2iundf  41156  frege124d  41258  clsk3nimkb  41539  clsk1indlem1  41544  clsk1independent  41545  ntrneineine1lem  41583  ntrneicls11  41589  clsneiel1  41607  clsneiel2  41608  neicvgel1  41618  neicvgel2  41619  radcnvrat  41821  rusbcALT  41946  en3lpVD  42354  eliin2f  42543  nssd  42544  wessf1ornlem  42611  limsupre2lem  43155  icccncfext  43318  stoweidlem14  43445  stoweidlem34  43465  stoweidlem59  43490  etransclem24  43689  nnfoctbdjlem  43883  nnfoctbdj  43884  hspmbllem2  44055  nsssmfmbflem  44200  fsetsnprcnex  44436  eu2ndop1stv  44504  afvfv0bi  44531  afvco2  44555  ndmaovg  44563  ndfatafv2nrn  44600  afv2ndefb  44603  afv2fv0  44644  nelbr  44653  otiunsndisjX  44658  fun2dmnopgexmpl  44663  ltnltne  44679  readdcnnred  44683  resubcnnred  44684  recnmulnred  44685  cndivrenred  44686  ichnreuop  44812  fmtnoinf  44876  odz2prm2pw  44903  prmdvdsfmtnof1lem2  44925  lighneallem3  44947  lighneallem4  44950  requad1  44962  isodd3  44992  bits0ALTV  45019  nfermltl8rev  45082  nfermltl2rev  45083  nfermltlrev  45084  lidldomnnring  45376  zrninitoringc  45517  ztprmneprm  45571  lindepsnlininds  45681  islindeps  45682  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  difmodm1lt  45756  line2ylem  45985  line2xlem  45987  map0cor  46070  elsetrecslem  46290