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  1084  xorbi12d  1525  equsexvw  2005  cbvexvw  2037  cbvexdvaw  2039  excomimw  2044  hbe1w  2049  19.8aw  2051  exexw  2052  ru0  2128  cbvexv1  2340  cbvex2v  2342  drex1v  2368  cbvex  2397  cbvex2  2410  drex1  2439  eujustALT  2565  necon3abid  2961  neleq12d  3034  cbvrexdva  3216  cbvrexfw  3277  rexeqbidvvOLD  3307  cbvrexdva2  3319  cbvrexf  3332  cbvexeqsetf  3459  cgsex4gOLD  3492  ceqsex  3493  ceqsexv  3495  gencbval  3506  spcegf  3555  spc2gv  3563  spc2d  3565  spc3gv  3567  ceqsralbv  3620  cdeqnot  3736  rru  3747  ruOLD  3749  sbcng  3798  sbcrext  3833  cbvrexcsf  3902  difjust  3913  eldif  3921  dfpss3  4048  dfdif3OLD  4077  difeq2  4079  disjne  4414  pssdifcom1  4449  eldifpr  4618  rexsng  4636  elpwunsn  4644  eldiftp  4647  rexprg  4657  preqsnd  4819  disjxun  5100  nalset  5263  dtruALT2  5320  dtruALT  5338  rexxfrd  5359  rexxfr2d  5361  rexxfrd2  5363  rexxfr  5366  dtruOLD  5396  opthneg  5436  snopeqop  5461  otiunsndisj  5475  poeq1  5542  pocl  5547  swopo  5550  sotric  5569  sotrieq  5570  isso2i  5576  somo  5578  freq1  5598  frirr  5607  fr2nr  5608  frminex  5610  tz7.2  5614  wereu2  5628  poinxp  5712  frinxp  5714  posn  5717  frsn  5719  rexiunxp  5794  rexxpf  5801  intirr  6079  poirr2  6085  cnvpo  6248  dfpo2  6257  predpoirr  6294  predfrirr  6295  frpomin  6301  nordeq  6339  ordtri1  6353  ordtri3  6356  fvmpti  6949  fndmdif  6996  rexrnmptw  7049  rexrnmpt  7051  rexima  7194  f1imapss  7223  f1ounsn  7229  cbvexfo  7247  nf1const  7261  soisoi  7285  isopolem  7302  weniso  7311  imaeqsalvOLD  7321  canth  7323  riotaclb  7367  rexrnmpo  7509  ndmovg  7552  sorpssuni  7688  sorpssint  7689  fr3nr  7728  dfwe2  7730  ordsucsssuc  7778  nlimsucg  7798  orduninsuc  7799  dfom2  7824  ssnlim  7842  resf1extb  7890  f1oweALT  7930  frxp  8082  poxp  8084  frxp2  8100  frxp3  8107  xpord3inddlem  8110  soseq  8115  suppofssd  8159  suppcoss  8163  smoword  8312  tz7.48lem  8386  oacan  8489  oaword  8490  omlimcl  8519  omeulem1  8523  nnaword  8568  nnmword  8574  nneob  8597  naddss1  8630  brdifun  8678  swoer  8679  undifixp  8884  boxcutc  8891  2dom  8978  php  9148  phpeqd  9153  nndomog  9154  onomeneq  9155  nnsdomo  9159  unxpdomlem2  9174  frfi  9208  unfilem1  9230  supeq3  9376  supeq123d  9377  supmo  9379  eqsup  9383  supub  9386  sup0  9394  suppr  9399  supisolem  9401  supisoex  9402  eqinf  9412  infval  9414  infmo  9424  infpr  9432  infempty  9436  oieq1  9441  ordtypecbv  9446  ordtypelem7  9453  wemapsolem  9479  canthwdom  9508  zfregcl  9523  elirrv  9525  elirr  9526  noinfep  9589  cantnfp1lem3  9609  ttrcltr  9645  rankr1clem  9749  carden2b  9896  domtri2  9918  alephord3  10007  alephdom2  10016  alephval3  10039  dfac9  10066  kmlem2  10081  kmlem4  10083  isfin4  10226  isfin7  10230  fin23lem11  10246  isf32lem5  10286  isf34lem4  10306  fin1a2lem6  10334  fin1a2lem7  10335  fin1a2lem12  10340  itunisuc  10348  ac6n  10414  zorn2g  10432  zornn0g  10434  ttukeylem7  10444  axpowndlem3  10528  axpowndlem4  10529  axregnd  10533  elgch  10551  engch  10557  fpwwe2lem12  10571  fpwwe2  10572  pwfseqlem1  10587  pwfseqlem3  10589  hargch  10602  addnidpi  10830  pinq  10856  nqereu  10858  ltsonq  10898  prlem934  10962  ltexprlem7  10971  addcanpr  10975  prlem936  10976  reclem2pr  10977  reclem3pr  10978  supexpr  10983  ltsosr  11023  supsrlem  11040  axpre-lttri  11094  axpre-sup  11098  xrlenlt  11215  axlttri  11221  axsup  11225  ltne  11247  dedekind  11313  readdcan  11324  leadd1  11622  ltsub1  11650  ltsub2  11651  leord1  11681  lediv1  12024  lemuldiv  12039  lerec  12042  le2msq  12059  infm3  12118  suprnub  12124  infregelb  12143  avgle1  12398  avgle2  12399  znnnlt1  12536  indstr  12851  zsupss  12872  uzsupss  12875  rpneg  12961  xralrple  13141  xleneg  13154  xltadd1  13192  xposdif  13198  xmulneg1  13205  xltmul1  13228  xrsupexmnf  13241  xrinfmexpnf  13242  xrsupsslem  13243  xrinfmsslem  13244  xrub  13248  supxrleub  13262  infxrgelb  13272  difreicc  13421  nn0disj  13581  nelfzo  13601  elfznelfzo  13709  fvinim0ffz  13723  injresinjlem  13724  ssnn0fi  13926  leexp2  14112  exp11nnd  14202  hashbnd  14277  hasheni  14289  hashfundm  14383  hashbc  14394  wrdsymb0  14490  swrdnd  14595  swrdnd2  14596  pfxnd0  14629  repswswrd  14725  repswccat  14727  cshwidxmod  14744  cnpart  15182  sqrtlt  15203  limsuplt  15421  rlimrege0  15521  isercoll  15610  efle  16062  odd2np1  16287  sumodd  16334  divalglem7  16345  ndvdsadd  16356  fldivndvdslt  16362  bitsfval  16369  bitsval  16370  bits0  16374  bitsp1  16377  bitsmod  16382  bitscmp  16384  bitsinv1lem  16387  sadadd2lem2  16396  saddisjlem  16410  bitsshft  16421  gcdneg  16468  algcvgblem  16523  lcmneg  16549  isprm3  16629  dvdsnprmd  16636  isprm5  16653  rpexp  16668  phiprmpw  16722  m1dvdsndvds  16745  pythagtrip  16781  pcgcd1  16824  prmpwdvds  16851  prmreclem2  16864  prmreclem3  16865  prmreclem5  16867  prmreclem6  16868  vdwlem6  16933  vdwnnlem2  16943  vdwnnlem3  16944  vdwnn  16945  prmlem0  17052  prmlem1a  17053  divsfval  17486  mrisval  17571  ismri  17572  ismri2dad  17578  cidpropd  17651  cat1lem  18038  plttr  18281  joinval  18316  meetval  18330  acsfiindd  18494  isnsgrp  18632  smndex1n0mnd  18821  mgm2nsgrplem2  18828  sgrp2nmndlem3  18834  symgpssefmnd  19310  symgfix2  19330  pmtrdifellem4  19393  psgnunilem1  19407  psgnunilem5  19408  psgnunilem2  19409  psgnunilem3  19410  pmtrsn  19433  sylow1lem3  19514  sylow2alem2  19532  efgsfo  19653  ablfac1eulem  19988  ablfac1eu  19989  pgpfac1lem1  19990  pgpfac1lem5  19995  nzrunit  20444  zrninitoringc  20596  islbs  21015  lbsind  21019  lbspss  21021  lbspropd  21038  lspsnne1  21059  islbs2  21096  lbsacsbs  21098  lbsextlem1  21100  lbsextlem3  21102  lbsextlem4  21103  lbsextg  21104  frlmlbs  21739  islindf  21754  islinds2  21755  islindf2  21756  lindfind  21758  lindsind  21759  lindfrn  21763  lindfmm  21769  lsslindf  21772  islindf4  21780  opsrtoslem2  21996  psdmul  22086  cply1coe0  22221  cply1coe0bi  22222  mdetunilem7  22538  mdetunilem8  22539  mdetunilem9  22540  maducoeval2  22560  pmatcollpw3fi1lem1  22706  fvmptnn04ifa  22770  fvmptnn04ifc  22772  fvmptnn04ifd  22773  chfacffsupp  22776  chfacfscmul0  22778  chfacfpmmul0  22782  elcls  22993  maxlp  23067  perfi  23075  ordtbaslem  23108  ordtval  23109  ordtbas2  23111  ordtopn1  23114  ordtopn2  23115  ordtcnv  23121  ordtrest  23122  ordtrest2lem  23123  ordtrest2  23124  pnfnei  23140  mnfnei  23141  isreg2  23297  ordthauslem  23303  cmpfi  23328  cmpfii  23329  bwth  23330  nconnsubb  23343  hausdiag  23565  txkgen  23572  kqdisj  23652  ordthmeolem  23721  fbfinnfr  23761  trfbas  23764  fbunfip  23789  fbasrn  23804  trfil3  23808  ufileu  23839  fin1aufil  23852  hausflim  23901  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALTlem4  23970  ptcmplem2  23973  ptcmplem3  23974  stdbdbl  24438  iccntr  24743  reconnlem2  24749  iccpnfcnv  24875  xrhmeo  24877  lebnumlem1  24893  lebnumlem2  24894  lebnumlem3  24895  bcthlem4  25260  minveclem3b  25361  ivthlem2  25386  ivthlem3  25387  mbfmax  25583  mbfposr  25586  i1fd  25615  mbfi1fseqlem4  25652  itg2splitlem  25682  itg2monolem1  25684  itg2cnlem1  25695  dvne0  25949  lhop1lem  25951  deg1nn0clb  26028  dgrle  26181  coemulhi  26192  aaliou3lem9  26291  cos11  26475  logleb  26545  argrege0  26553  logdivle  26564  ellogdm  26581  cxple  26637  cxplt2  26640  cxple3  26643  isosctrlem1  26761  atandm  26819  atans2  26874  atantayl2  26881  eldmgm  26965  ftalem7  27022  isppw2  27058  musum  27134  dchrsum2  27212  bposlem1  27228  lgsmod  27267  lgsdir2lem2  27270  lgsdir2  27274  lgsne0  27279  lgsprme0  27283  gausslemma2dlem4  27313  lgsquadlem1  27324  2lgslem3  27348  2lgsoddprm  27360  2sq2  27377  addsqrexnreu  27386  rpvmasumlem  27431  padicabv  27574  ostth3  27582  ostth  27583  noextenddif  27613  nodenselem4  27632  nodenselem5  27633  nodenselem7  27635  nolt02o  27640  nogt01o  27641  noresle  27642  nosupprefixmo  27645  noinfprefixmo  27646  nosupcbv  27647  nosupdm  27649  nosupfv  27651  nosupres  27652  nosupbnd1lem1  27653  nosupbnd1lem3  27655  nosupbnd1lem5  27657  nosupbnd1  27659  nosupbnd2lem1  27660  nosupbnd2  27661  noinfcbv  27662  noinfdm  27664  noinffv  27666  noinfres  27667  noinfbnd1lem1  27668  noinfbnd1lem3  27670  noinfbnd1lem5  27672  noinfbnd1  27674  noinfbnd2lem1  27675  noinfbnd2  27676  slenlt  27697  sltne  27715  nocvxminlem  27723  slerec  27765  eqscut3  27770  cuteq1  27783  newbday  27851  sltlpss  27857  cofcutr  27872  lrrecfr  27890  addsval  27909  sltadd2  27938  sleneg  27992  slesubsubbd  28030  slesubsub2bd  28031  slesubsub3bd  28032  slesubaddd  28037  sltmul2  28114  slemul2d  28117  slemul1d  28118  onscutlt  28205  istrkgld  28439  axtgupdim2  28451  tglowdim2l  28630  axlowdimlem16  28937  axlowdim2  28940  axlowdim  28941  numedglnl  29124  usgredg2v  29207  lfuhgr1v0e  29234  cusgrfi  29439  vtxd0nedgb  29469  vtxduhgr0edgnel  29475  1loopgrnb0  29483  1hevtxdg0  29486  vtxdgoddnumeven  29534  wlkp1lem1  29652  wlkp1lem2  29653  wlkp1lem5  29656  dfpth2  29709  crctcsh  29804  clwlkclwwlklem2a4  29976  eupth2eucrct  30196  eupth2lem3lem3  30209  eupth2lem3lem4  30210  eupth2lem3lem6  30212  eupth2lem3lem7  30213  eupth2lems  30217  eupth2  30218  konigsberglem4  30234  nfrgr2v  30251  frgrwopreglem3  30293  fusgr2wsp2nb  30313  frgrreggt1  30372  friendshipgt3  30377  lpni  30459  nmobndseqi  30758  minvecolem5  30860  chpsscon3  31482  chnle  31493  nonbooli  31630  pjnel  31705  specval  31877  nmcfnlbi  32031  stri  32236  hstri  32244  cvbr  32261  cvcon3  32263  chcv1  32334  cvexchlem  32347  chrelat2  32349  nelun  32492  elpreq  32507  nelpr  32510  ifeqeqx  32521  nfpconfp  32606  suppiniseg  32659  isoun  32675  suppss3  32697  xrge0infss  32733  infxrge0gelb  32739  eliccelico  32750  elicoelioo  32751  nndiffz1  32759  hashgt1  32783  expgt0b  32791  nn0min  32795  ccatws1f1o  32923  toslublem  32944  tosglblem  32946  pmtrcnel  33061  cycpmco2  33105  isarchi2  33154  archiabl  33167  elrgspnlem2  33210  elrgspnlem3  33211  0nellinds  33334  lindssn  33342  lindfpropd  33346  ssdifidlprm  33422  mxidlirred  33436  ssmxidl  33438  lbslsat  33605  lindsunlem  33613  rtelextdg2lem  33709  constrsqrtcl  33762  ordtcnvNEW  33903  ordtrestNEW  33904  ordtrest2NEWlem  33905  ordtrest2NEW  33906  ordtconnlem1  33907  xrge0iifcnv  33916  esumpcvgval  34061  esum2d  34076  ddemeas  34219  omssubadd  34284  oddpwdc  34338  eulerpartlems  34344  eulerpartlemf  34354  eulerpartlemt  34355  eulerpartlemr  34358  eulerpartlemgvv  34360  eulerpartlemn  34365  ballotlemfc0  34477  ballotlemfcc  34478  ballotlem4  34483  ballotlemimin  34490  ballotlem7  34520  plymulx  34532  signsply0  34535  reprinfz1  34606  reprpmtf1o  34610  reprdifc  34611  hgt750lema  34641  hgt750leme  34642  istrkg2d  34650  bnj23  34701  bnj1185  34776  bnj1228  34994  bnj1388  35016  bnj1417  35024  nummin  35074  axnulg  35075  onvf1odlem2  35084  onvf1odlem3  35085  revwlk  35105  isacycgr  35125  acycgr0v  35128  prclisacycgr  35131  erdszelem10  35180  satf0n0  35358  fmlaomn0  35370  fmlasucdisj  35379  satfv1fvfmla1  35403  satefvfmla1  35405  ismfs  35529  mvtinf  35535  untelirr  35688  untsucf  35690  untangtr  35694  dfon2lem3  35766  dfon2lem4  35767  dfon2lem7  35770  dfon2lem9  35772  distel  35784  funpartfv  35926  dfrdg4  35932  nn0prpwlem  36303  nn0prpw  36304  limsucncmpi  36426  limsucncmp  36427  ordcmp  36428  weiunlem2  36444  weiunfrlem  36445  weiunfr  36448  unblimceq0  36488  unbdqndv1  36489  bj-hbntbi  36685  bj-equsexvwd  36762  bj-cbvexdv  36781  bj-ru1  36924  bj-nuliota  37038  topdifinffinlem  37328  topdifinffin  37329  icorempo  37332  relowlpssretop  37345  finxpreclem2  37371  finxpreclem6  37377  wl-issetft  37563  wl-ax11-lem8  37573  leceifl  37596  lindsadd  37600  lindsenlbs  37602  matunitlindflem1  37603  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem21  37628  poimirlem23  37630  poimirlem26  37633  poimirlem27  37634  poimirlem28  37635  poimirlem31  37638  poimir  37640  mblfinlem2  37645  mblfinlem3  37646  ismblfin  37648  cnambfre  37655  itg2addnclem  37658  itg2addnclem2  37659  iblabsnclem  37670  ftc1anclem1  37680  areacirc  37700  heibor1lem  37796  heiborlem1  37798  heiborlem6  37803  heiborlem8  37805  heiborlem10  37807  smprngopr  38039  ecin0  38327  ax12inda  38934  riotaclbgBAD  38940  lcvfbr  39006  lcvbr  39007  lsatcv0  39017  l1cvpat  39040  opltcon3b  39190  cvrfval  39254  cvrval  39255  cvrnbtwn  39257  cvrval2  39260  cvrnbtwn2  39261  cvrnbtwn3  39262  cvrcon3b  39263  cvrnbtwn4  39265  atnlt  39299  iscvlat  39309  cvlexch1  39314  hlsuprexch  39368  hlrelat5N  39388  hlrelat2  39390  cvrval5  39402  3dimlem1  39445  3dim1lem5  39453  3dim2  39455  3dim3  39456  llnnlt  39510  islpln5  39522  lplni2  39524  lvolex3N  39525  lplnnle2at  39528  islpln2a  39535  lplnribN  39538  lplnexllnN  39551  lplnnlt  39552  lvoli3  39564  islvol5  39566  lvoli2  39568  lvolnle3at  39569  islvol2aN  39579  4atlem11  39596  lvolnltN  39605  dalawlem15  39872  4atexlemex2  40058  4atex  40063  4atex2-0aOLDN  40065  4atex2-0cOLDN  40067  lautcvr  40079  ltrnfset  40104  ltrnset  40105  ltrnu  40108  trlfset  40147  trlset  40148  trlval2  40150  cdlemd6  40190  cdleme0nex  40277  cdleme18d  40282  cdleme25b  40341  cdleme25cv  40345  cdleme29b  40362  cdleme31fv  40377  cdleme31fv2  40380  cdlemefrs29bpre0  40383  cdlemefr32sn2aw  40391  cdlemefr29bpre0N  40393  cdlemefr29clN  40394  cdlemefr32fvaN  40396  cdlemefr32fva1  40397  cdlemefs32sn1aw  40401  cdleme32fva  40424  cdleme32fvaw  40426  cdleme40v  40456  cdleme42b  40465  cdleme46f2g2  40480  cdleme46f2g1  40481  cdleme48gfv  40524  cdlemg1fvawlemN  40560  cdlemg1cex  40575  cdlemg6d  40608  cdlemm10N  41105  dicffval  41161  dicfval  41162  dicval  41163  dicfnN  41170  dicvalrelN  41172  dihffval  41217  dihfval  41218  dihlsscpre  41221  dvh4dimat  41425  dvh3dimatN  41426  dvh4dimlem  41430  dvh3dim  41433  dvh4dimN  41434  dvh3dim2  41435  dvh3dim3N  41436  mapdcv  41647  mapdh9aOLDN  41777  hdmapfval  41814  hdmapval  41815  hdmapval2  41819  hdmap11lem2  41829  dvrelog2b  42047  aks4d1p4  42060  aks4d1p5  42061  aks4d1p7  42064  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1  42070  aks6d1c2p2  42100  hashnexinj  42109  rspcsbnea  42112  aks6d1c5  42120  aks6d1c6lem3  42153  aks6d1c7  42165  supinf  42223  oexpreposd  42303  mullt0b2d  42465  flt4lem7  42640  nna4b4nsq  42641  ellz1  42748  rencldnfilem  42801  jm2.22  42977  jm2.23  42978  wepwsolem  43024  fnwe2lem2  43033  aomclem8  43043  unxpwdom3  43077  onsupmaxb  43221  onexlimgt  43225  onsupeqnmax  43229  onov0suclim  43256  oaordnr  43278  omnord1  43287  oenord1  43298  oaomoencom  43299  oenass  43301  cantnfresb  43306  tfsnfin  43334  ralopabb  43393  nlimsuc  43423  ifpbi12  43470  dfsucon  43505  sqrtcvallem1  43613  ss2iundf  43641  frege124d  43743  clsk3nimkb  44022  clsk1indlem1  44027  clsk1independent  44028  ntrneineine1lem  44066  ntrneicls11  44072  clsneiel1  44090  clsneiel2  44091  neicvgel1  44101  neicvgel2  44102  radcnvrat  44296  rusbcALT  44421  en3lpVD  44827  0elaxnul  44966  omssaxinf2  44971  permaxnul  44991  permaxinf2lem  44995  nregmodel  45000  eliin2f  45091  nssd  45092  wessf1ornlem  45172  rexanuz2nf  45481  limsupre2lem  45715  icccncfext  45878  stoweidlem14  46005  stoweidlem34  46025  stoweidlem59  46050  etransclem24  46249  nnfoctbdjlem  46446  nnfoctbdj  46447  hspmbllem2  46618  nsssmfmbflem  46769  fsetsnprcnex  47049  eu2ndop1stv  47119  afvfv0bi  47146  afvco2  47170  ndmaovg  47178  ndfatafv2nrn  47215  afv2ndefb  47218  afv2fv0  47259  nelbr  47268  otiunsndisjX  47273  fun2dmnopgexmpl  47278  ltnltne  47293  readdcnnred  47297  resubcnnred  47298  recnmulnred  47299  cndivrenred  47300  ichnreuop  47466  fmtnoinf  47530  odz2prm2pw  47557  prmdvdsfmtnof1lem2  47579  lighneallem3  47601  lighneallem4  47604  requad1  47616  isodd3  47646  bits0ALTV  47673  nfermltl8rev  47736  nfermltl2rev  47737  nfermltlrev  47738  upgrimpths  47902  isubgr3stgrlem3  47960  usgrexmpl12ngric  48022  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  pgnbgreunbgrlem5lem1  48103  pgnbgreunbgrlem5lem2  48104  pgnbgreunbgrlem5lem3  48105  lgricngricex  48112  lidldomnnring  48217  ztprmneprm  48328  lindepsnlininds  48434  islindeps  48435  lindslinindsimp2lem5  48444  lindslinindsimp2  48445  line2ylem  48733  line2xlem  48735  map0cor  48836  nelsubc3lem  49052  fulltermc2  49494  setc1onsubc  49584  cnelsubclem  49585  elsetrecslem  49681