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 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  319  annotanannot  832  ifpbi123dOLD  1078  con3ALT  1084  xorbi12d  1522  norassOLD  1536  equsexvw  2009  cbvexvw  2041  cbvexdvaw  2043  hbe1w  2052  19.8aw  2054  exexw  2055  cbvexv1  2340  cbvex2v  2343  drex1v  2370  cbvex  2400  cbvex2  2413  drex1  2442  eujustALT  2573  necon3abid  2981  neleq12d  3054  rexbiOLD  3175  rexeqbidvv  3340  cbvrexfw  3371  cbvrexf  3373  cgsex4g  3477  gencbval  3491  spcegf  3532  spc2gv  3540  spc2d  3542  spc3gv  3544  cdeqnot  3704  rru  3715  ru  3716  sbcng  3767  sbcrext  3807  cbvrexcsf  3879  difjust  3890  eldif  3898  dfpss3  4022  dfdif3  4050  difeq2  4052  ab0OLD  4310  disjne  4389  pssdifcom1  4421  eldifpr  4594  rexsng  4611  elpwunsn  4620  eldiftp  4623  rexprg  4633  preqsnd  4790  disjxun  5073  nalset  5238  dtruALT2  5294  dtruALT  5312  rexxfrd  5333  rexxfr2d  5335  rexxfrd2  5337  rexxfr  5340  dtru  5360  opthneg  5397  snopeqop  5421  otiunsndisj  5435  poeq1  5507  pocl  5511  poclOLD  5512  swopo  5515  sotric  5532  sotrieq  5533  isso2i  5539  somo  5541  freq1  5560  frirr  5567  fr2nr  5568  frminex  5570  tz7.2  5574  wereu2  5587  poinxp  5668  frinxp  5670  posn  5673  frsn  5675  rexiunxp  5752  rexxpf  5759  intirr  6028  poirr2  6034  cnvpo  6194  dfpo2  6203  predpoirr  6240  predfrirr  6241  frpomin  6247  nordeq  6289  ordtri1  6303  ordtri3  6306  fvmpti  6883  fndmdif  6928  rexrnmptw  6980  rexrnmpt  6982  2f1fvneq  7142  f1imapss  7148  cbvexfo  7171  nf1const  7185  soisoi  7208  isopolem  7225  weniso  7234  canth  7238  riotaclb  7283  rexrnmpo  7422  ndmovg  7464  sorpssuni  7594  sorpssint  7595  fr3nr  7631  dfwe2  7633  ordsucsssuc  7679  nlimsucg  7698  orduninsuc  7699  dfom2  7723  ssnlim  7741  f1oweALT  7824  frxp  7976  poxp  7978  suppofssd  8028  suppcoss  8032  wfrlem10OLD  8158  smoword  8206  tz7.48lem  8281  oacan  8388  oaword  8389  omlimcl  8418  omeulem1  8422  nnaword  8467  nnmword  8473  nneob  8495  brdifun  8536  swoer  8537  undifixp  8731  boxcutc  8738  2dom  8829  php  9002  phpeqd  9007  nndomog  9008  phpOLD  9014  nndomogOLD  9018  onomeneq  9020  nnsdomo  9026  unxpdomlem2  9037  frfi  9068  unfilem1  9087  supeq3  9217  supeq123d  9218  supmo  9220  eqsup  9224  supub  9227  sup0  9234  suppr  9239  supisolem  9241  supisoex  9242  eqinf  9252  infval  9254  infmo  9263  infpr  9271  infempty  9275  oieq1  9280  ordtypecbv  9285  ordtypelem7  9292  wemapsolem  9318  canthwdom  9347  zfregcl  9362  elirrv  9364  elirr  9365  noinfep  9427  cantnfp1lem3  9447  ttrcltr  9483  rankr1clem  9587  carden2b  9734  domtri2  9756  alephord3  9843  alephdom2  9852  alephval3  9875  dfac9  9901  kmlem2  9916  kmlem4  9918  isfin4  10062  isfin7  10066  fin23lem11  10082  isf32lem5  10122  isf34lem4  10142  fin1a2lem6  10170  fin1a2lem7  10171  fin1a2lem12  10176  itunisuc  10184  ac6n  10250  zorn2g  10268  zornn0g  10270  ttukeylem7  10280  axpowndlem3  10364  axpowndlem4  10365  axregnd  10369  elgch  10387  engch  10393  fpwwe2lem12  10407  fpwwe2  10408  pwfseqlem1  10423  pwfseqlem3  10425  hargch  10438  addnidpi  10666  pinq  10692  nqereu  10694  ltsonq  10734  prlem934  10798  ltexprlem7  10807  addcanpr  10811  prlem936  10812  reclem2pr  10813  reclem3pr  10814  supexpr  10819  ltsosr  10859  supsrlem  10876  axpre-lttri  10930  axpre-sup  10934  xrlenlt  11049  axlttri  11055  axsup  11059  ltne  11081  dedekind  11147  readdcan  11158  leadd1  11452  ltsub1  11480  ltsub2  11481  leord1  11511  lediv1  11849  lemuldiv  11864  lerec  11867  le2msq  11884  infm3  11943  suprnub  11949  infregelb  11968  avgle1  12222  avgle2  12223  znnnlt1  12356  indstr  12665  zsupss  12686  uzsupss  12689  rpneg  12771  xralrple  12948  xleneg  12961  xltadd1  12999  xposdif  13005  xmulneg1  13012  xltmul1  13035  xrsupexmnf  13048  xrinfmexpnf  13049  xrsupsslem  13050  xrinfmsslem  13051  xrub  13055  supxrleub  13069  infxrgelb  13078  difreicc  13225  nn0disj  13381  nelfzo  13401  elfznelfzo  13501  fvinim0ffz  13515  injresinjlem  13516  ssnn0fi  13714  leexp2  13898  hashbnd  14059  hasheni  14071  hashbc  14174  wrdsymb0  14261  swrdnd  14376  swrdnd2  14377  pfxnd0  14410  repswswrd  14506  repswccat  14508  cshwidxmod  14525  cnpart  14960  sqrtlt  14982  limsuplt  15197  rlimrege0  15297  isercoll  15388  efle  15836  odd2np1  16059  sumodd  16106  divalglem7  16117  ndvdsadd  16128  fldivndvdslt  16132  bitsfval  16139  bitsval  16140  bits0  16144  bitsp1  16147  bitsmod  16152  bitscmp  16154  bitsinv1lem  16157  sadadd2lem2  16166  saddisjlem  16180  bitsshft  16191  gcdneg  16238  algcvgblem  16291  lcmneg  16317  isprm3  16397  dvdsnprmd  16404  isprm5  16421  rpexp  16436  phiprmpw  16486  m1dvdsndvds  16508  pythagtrip  16544  pcgcd1  16587  prmpwdvds  16614  prmreclem2  16627  prmreclem3  16628  prmreclem5  16630  prmreclem6  16631  vdwlem6  16696  vdwnnlem2  16706  vdwnnlem3  16707  vdwnn  16708  prmlem0  16816  prmlem1a  16817  divsfval  17267  mrisval  17348  ismri  17349  ismri2dad  17355  cidpropd  17428  cat1lem  17820  plttr  18069  joinval  18104  meetval  18118  acsfiindd  18280  isnsgrp  18388  smndex1n0mnd  18560  mgm2nsgrplem2  18567  sgrp2nmndlem3  18573  symgpssefmnd  19012  symgfix2  19033  pmtrdifellem4  19096  psgnunilem1  19110  psgnunilem5  19111  psgnunilem2  19112  psgnunilem3  19113  pmtrsn  19136  sylow1lem3  19214  sylow2alem2  19232  efgsfo  19354  ablfac1eulem  19684  ablfac1eu  19685  pgpfac1lem1  19686  pgpfac1lem5  19691  islbs  20347  lbsind  20351  lbspss  20353  lbspropd  20370  lspsnne1  20388  islbs2  20425  lbsacsbs  20427  lbsextlem1  20429  lbsextlem3  20431  lbsextlem4  20432  lbsextg  20433  nzrunit  20547  frlmlbs  21013  islindf  21028  islinds2  21029  islindf2  21030  lindfind  21032  lindsind  21033  lindfrn  21037  lindfmm  21043  lsslindf  21046  islindf4  21054  opsrtoslem2  21272  cply1coe0  21479  cply1coe0bi  21480  mdetunilem7  21776  mdetunilem8  21777  mdetunilem9  21778  maducoeval2  21798  pmatcollpw3fi1lem1  21944  fvmptnn04ifa  22008  fvmptnn04ifc  22010  fvmptnn04ifd  22011  chfacffsupp  22014  chfacfscmul0  22016  chfacfpmmul0  22020  elcls  22233  maxlp  22307  perfi  22315  ordtbaslem  22348  ordtval  22349  ordtbas2  22351  ordtopn1  22354  ordtopn2  22355  ordtcnv  22361  ordtrest  22362  ordtrest2lem  22363  ordtrest2  22364  pnfnei  22380  mnfnei  22381  isreg2  22537  ordthauslem  22543  cmpfi  22568  cmpfii  22569  bwth  22570  nconnsubb  22583  hausdiag  22805  txkgen  22812  kqdisj  22892  ordthmeolem  22961  fbfinnfr  23001  trfbas  23004  fbunfip  23029  fbasrn  23044  trfil3  23048  ufileu  23079  fin1aufil  23092  hausflim  23141  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  ptcmplem2  23213  ptcmplem3  23214  stdbdbl  23682  iccntr  23993  reconnlem2  23999  iccpnfcnv  24116  xrhmeo  24118  lebnumlem1  24133  lebnumlem2  24134  lebnumlem3  24135  bcthlem4  24500  minveclem3b  24601  ivthlem2  24625  ivthlem3  24626  mbfmax  24822  mbfposr  24825  i1fd  24854  mbfi1fseqlem4  24892  itg2splitlem  24922  itg2monolem1  24924  itg2cnlem1  24935  dvne0  25184  lhop1lem  25186  deg1nn0clb  25264  dgrle  25413  coemulhi  25424  aaliou3lem9  25519  cos11  25698  logleb  25767  argrege0  25775  logdivle  25786  ellogdm  25803  cxple  25859  cxplt2  25862  cxple3  25865  isosctrlem1  25977  atandm  26035  atans2  26090  atantayl2  26097  eldmgm  26180  ftalem7  26237  isppw2  26273  musum  26349  dchrsum2  26425  bposlem1  26441  lgsmod  26480  lgsdir2lem2  26483  lgsdir2  26487  lgsne0  26492  lgsprme0  26496  gausslemma2dlem4  26526  lgsquadlem1  26537  2lgslem3  26561  2lgsoddprm  26573  2sq2  26590  addsqrexnreu  26599  rpvmasumlem  26644  padicabv  26787  ostth3  26795  ostth  26796  istrkgld  26829  axtgupdim2  26841  tglowdim2l  27020  axlowdimlem16  27334  axlowdim2  27337  axlowdim  27338  numedglnl  27523  usgredg2v  27603  lfuhgr1v0e  27630  cusgrfi  27834  vtxd0nedgb  27864  vtxduhgr0edgnel  27870  1loopgrnb0  27878  1hevtxdg0  27881  vtxdgoddnumeven  27929  wlkp1lem1  28050  wlkp1lem2  28051  wlkp1lem5  28054  crctcsh  28198  clwlkclwwlklem2a4  28370  eupth2eucrct  28590  eupth2lem3lem3  28603  eupth2lem3lem4  28604  eupth2lem3lem6  28606  eupth2lem3lem7  28607  eupth2lems  28611  eupth2  28612  konigsberglem4  28628  nfrgr2v  28645  frgrwopreglem3  28687  fusgr2wsp2nb  28707  frgrreggt1  28766  friendshipgt3  28771  lpni  28851  nmobndseqi  29150  minvecolem5  29252  chpsscon3  29874  chnle  29885  nonbooli  30022  pjnel  30097  specval  30269  nmcfnlbi  30423  stri  30628  hstri  30636  cvbr  30653  cvcon3  30655  chcv1  30726  cvexchlem  30739  chrelat2  30741  nelun  30868  elpreq  30887  nelpr  30888  ifeqeqx  30894  nfpconfp  30976  suppiniseg  31029  isoun  31043  suppss3  31068  xrge0infss  31092  infxrge0gelb  31098  eliccelico  31107  elicoelioo  31108  nndiffz1  31116  hashgt1  31137  nn0min  31143  toslublem  31259  tosglblem  31261  pmtrcnel  31367  cycpmco2  31409  isarchi2  31448  archiabl  31461  0nellinds  31575  lindssn  31582  lindfpropd  31585  ssmxidl  31651  lbslsat  31708  lindsunlem  31714  ordtcnvNEW  31879  ordtrestNEW  31880  ordtrest2NEWlem  31881  ordtrest2NEW  31882  ordtconnlem1  31883  xrge0iifcnv  31892  esumpcvgval  32055  esum2d  32070  ddemeas  32213  omssubadd  32276  oddpwdc  32330  eulerpartlems  32336  eulerpartlemf  32346  eulerpartlemt  32347  eulerpartlemr  32350  eulerpartlemgvv  32352  eulerpartlemn  32357  ballotlemfc0  32468  ballotlemfcc  32469  ballotlem4  32474  ballotlemimin  32481  ballotlem7  32511  plymulx  32536  signsply0  32539  reprinfz1  32611  reprpmtf1o  32615  reprdifc  32616  hgt750lema  32646  hgt750leme  32647  istrkg2d  32655  bnj23  32706  bnj1185  32782  bnj1228  33000  bnj1388  33022  bnj1417  33030  nummin  33072  hashfundm  33083  revwlk  33095  isacycgr  33116  acycgr0v  33119  prclisacycgr  33122  erdszelem10  33171  satf0n0  33349  fmlaomn0  33361  fmlasucdisj  33370  satfv1fvfmla1  33394  satefvfmla1  33396  ismfs  33520  mvtinf  33526  untelirr  33658  untsucf  33660  untangtr  33664  ceqsralv2  33679  imaeqsalv  33700  dfon2lem3  33770  dfon2lem4  33771  dfon2lem7  33774  dfon2lem9  33776  distel  33788  frxp2  33800  frxp3  33806  soseq  33812  naddss1  33850  noextenddif  33880  nodenselem4  33899  nodenselem5  33900  nodenselem7  33902  nolt02o  33907  nogt01o  33908  noresle  33909  nosupprefixmo  33912  noinfprefixmo  33913  nosupcbv  33914  nosupdm  33916  nosupfv  33918  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem3  33922  nosupbnd1lem5  33924  nosupbnd1  33926  nosupbnd2lem1  33927  nosupbnd2  33928  noinfcbv  33929  noinfdm  33931  noinffv  33933  noinfres  33934  noinfbnd1lem1  33935  noinfbnd1lem3  33937  noinfbnd1lem5  33939  noinfbnd1  33941  noinfbnd2lem1  33942  noinfbnd2  33943  slenlt  33964  nocvxminlem  33981  slerec  34022  newbday  34091  sltlpss  34096  cofcutr  34101  lrrecfr  34109  addsval  34135  funpartfv  34256  dfrdg4  34262  nn0prpwlem  34520  nn0prpw  34521  limsucncmpi  34643  limsucncmp  34644  ordcmp  34645  unblimceq0  34696  unbdqndv1  34697  bj-hbntbi  34895  bj-equsexvwd  34972  bj-cbvexdv  34991  bj-dtru  35008  bj-ru0  35140  bj-nuliota  35237  topdifinffinlem  35527  topdifinffin  35528  icorempo  35531  relowlpssretop  35544  finxpreclem2  35570  finxpreclem6  35576  wl-ax11-lem8  35752  leceifl  35775  lindsadd  35779  lindsenlbs  35781  matunitlindflem1  35782  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem21  35807  poimirlem23  35809  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem31  35817  poimir  35819  mblfinlem2  35824  mblfinlem3  35825  ismblfin  35827  cnambfre  35834  itg2addnclem  35837  itg2addnclem2  35838  iblabsnclem  35849  ftc1anclem1  35859  areacirc  35879  heibor1lem  35976  heiborlem1  35978  heiborlem6  35983  heiborlem8  35985  heiborlem10  35987  smprngopr  36219  ecin0  36491  ax12inda  36969  riotaclbgBAD  36975  lcvfbr  37041  lcvbr  37042  lsatcv0  37052  l1cvpat  37075  opltcon3b  37225  cvrfval  37289  cvrval  37290  cvrnbtwn  37292  cvrval2  37295  cvrnbtwn2  37296  cvrnbtwn3  37297  cvrcon3b  37298  cvrnbtwn4  37300  atnlt  37334  iscvlat  37344  cvlexch1  37349  hlsuprexch  37402  hlrelat5N  37422  hlrelat2  37424  cvrval5  37436  3dimlem1  37479  3dim1lem5  37487  3dim2  37489  3dim3  37490  llnnlt  37544  islpln5  37556  lplni2  37558  lvolex3N  37559  lplnnle2at  37562  islpln2a  37569  lplnribN  37572  lplnexllnN  37585  lplnnlt  37586  lvoli3  37598  islvol5  37600  lvoli2  37602  lvolnle3at  37603  islvol2aN  37613  4atlem11  37630  lvolnltN  37639  dalawlem15  37906  4atexlemex2  38092  4atex  38097  4atex2-0aOLDN  38099  4atex2-0cOLDN  38101  lautcvr  38113  ltrnfset  38138  ltrnset  38139  ltrnu  38142  trlfset  38181  trlset  38182  trlval2  38184  cdlemd6  38224  cdleme0nex  38311  cdleme18d  38316  cdleme25b  38375  cdleme25cv  38379  cdleme29b  38396  cdleme31fv  38411  cdleme31fv2  38414  cdlemefrs29bpre0  38417  cdlemefr32sn2aw  38425  cdlemefr29bpre0N  38427  cdlemefr29clN  38428  cdlemefr32fvaN  38430  cdlemefr32fva1  38431  cdlemefs32sn1aw  38435  cdleme32fva  38458  cdleme32fvaw  38460  cdleme40v  38490  cdleme42b  38499  cdleme46f2g2  38514  cdleme46f2g1  38515  cdleme48gfv  38558  cdlemg1fvawlemN  38594  cdlemg1cex  38609  cdlemg6d  38642  cdlemm10N  39139  dicffval  39195  dicfval  39196  dicval  39197  dicfnN  39204  dicvalrelN  39206  dihffval  39251  dihfval  39252  dihlsscpre  39255  dvh4dimat  39459  dvh3dimatN  39460  dvh4dimlem  39464  dvh3dim  39467  dvh4dimN  39468  dvh3dim2  39469  dvh3dim3N  39470  mapdcv  39681  mapdh9aOLDN  39811  hdmapfval  39848  hdmapval  39849  hdmapval2  39853  hdmap11lem2  39863  dvrelog2b  40081  aks4d1p4  40094  aks4d1p5  40095  aks4d1p7  40098  aks4d1p8d2  40100  aks4d1p8  40102  aks4d1  40104  metakunt27  40158  metakunt28  40159  metakunt29  40160  oexpreposd  40328  exp11nnd  40331  flt4lem7  40503  nna4b4nsq  40504  ellz1  40596  rencldnfilem  40649  jm2.22  40824  jm2.23  40825  wepwsolem  40874  fnwe2lem2  40883  aomclem8  40893  unxpwdom3  40927  nlimsuc  41055  ifpbi12  41102  dfsucon  41137  sqrtcvallem1  41246  ss2iundf  41274  frege124d  41376  clsk3nimkb  41657  clsk1indlem1  41662  clsk1independent  41663  ntrneineine1lem  41701  ntrneicls11  41707  clsneiel1  41725  clsneiel2  41726  neicvgel1  41736  neicvgel2  41737  radcnvrat  41939  rusbcALT  42064  en3lpVD  42472  eliin2f  42661  nssd  42662  wessf1ornlem  42729  limsupre2lem  43272  icccncfext  43435  stoweidlem14  43562  stoweidlem34  43582  stoweidlem59  43607  etransclem24  43806  nnfoctbdjlem  44000  nnfoctbdj  44001  hspmbllem2  44172  nsssmfmbflem  44323  fsetsnprcnex  44560  eu2ndop1stv  44628  afvfv0bi  44655  afvco2  44679  ndmaovg  44687  ndfatafv2nrn  44724  afv2ndefb  44727  afv2fv0  44768  nelbr  44777  otiunsndisjX  44782  fun2dmnopgexmpl  44787  ltnltne  44802  readdcnnred  44806  resubcnnred  44807  recnmulnred  44808  cndivrenred  44809  ichnreuop  44935  fmtnoinf  44999  odz2prm2pw  45026  prmdvdsfmtnof1lem2  45048  lighneallem3  45070  lighneallem4  45073  requad1  45085  isodd3  45115  bits0ALTV  45142  nfermltl8rev  45205  nfermltl2rev  45206  nfermltlrev  45207  lidldomnnring  45499  zrninitoringc  45640  ztprmneprm  45694  lindepsnlininds  45804  islindeps  45805  lindslinindsimp2lem5  45814  lindslinindsimp2  45815  difmodm1lt  45879  line2ylem  46108  line2xlem  46110  map0cor  46193  elsetrecslem  46415