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  elirrvOLD  9526  elirr  9527  noinfep  9591  cantnfp1lem3  9611  ttrcltr  9647  rankr1clem  9751  carden2b  9898  domtri2  9920  alephord3  10009  alephdom2  10018  alephval3  10041  dfac9  10068  kmlem2  10083  kmlem4  10085  isfin4  10228  isfin7  10232  fin23lem11  10248  isf32lem5  10288  isf34lem4  10308  fin1a2lem6  10336  fin1a2lem7  10337  fin1a2lem12  10342  itunisuc  10350  ac6n  10416  zorn2g  10434  zornn0g  10436  ttukeylem7  10446  axpowndlem3  10530  axpowndlem4  10531  axregnd  10535  elgch  10553  engch  10559  fpwwe2lem12  10573  fpwwe2  10574  pwfseqlem1  10589  pwfseqlem3  10591  hargch  10604  addnidpi  10832  pinq  10858  nqereu  10860  ltsonq  10900  prlem934  10964  ltexprlem7  10973  addcanpr  10977  prlem936  10978  reclem2pr  10979  reclem3pr  10980  supexpr  10985  ltsosr  11025  supsrlem  11042  axpre-lttri  11096  axpre-sup  11100  xrlenlt  11217  axlttri  11223  axsup  11227  ltne  11249  dedekind  11315  readdcan  11326  leadd1  11624  ltsub1  11652  ltsub2  11653  leord1  11683  lediv1  12026  lemuldiv  12041  lerec  12044  le2msq  12061  infm3  12120  suprnub  12126  infregelb  12145  avgle1  12400  avgle2  12401  znnnlt1  12538  indstr  12853  zsupss  12874  uzsupss  12877  rpneg  12963  xralrple  13143  xleneg  13156  xltadd1  13194  xposdif  13200  xmulneg1  13207  xltmul1  13230  xrsupexmnf  13243  xrinfmexpnf  13244  xrsupsslem  13245  xrinfmsslem  13246  xrub  13250  supxrleub  13264  infxrgelb  13274  difreicc  13423  nn0disj  13583  nelfzo  13603  elfznelfzo  13711  fvinim0ffz  13725  injresinjlem  13726  ssnn0fi  13928  leexp2  14114  exp11nnd  14204  hashbnd  14279  hasheni  14291  hashfundm  14385  hashbc  14396  wrdsymb0  14492  swrdnd  14597  swrdnd2  14598  pfxnd0  14631  repswswrd  14726  repswccat  14728  cshwidxmod  14745  cnpart  15183  sqrtlt  15204  limsuplt  15422  rlimrege0  15522  isercoll  15611  efle  16063  odd2np1  16288  sumodd  16335  divalglem7  16346  ndvdsadd  16357  fldivndvdslt  16363  bitsfval  16370  bitsval  16371  bits0  16375  bitsp1  16378  bitsmod  16383  bitscmp  16385  bitsinv1lem  16388  sadadd2lem2  16397  saddisjlem  16411  bitsshft  16422  gcdneg  16469  algcvgblem  16524  lcmneg  16550  isprm3  16630  dvdsnprmd  16637  isprm5  16654  rpexp  16669  phiprmpw  16723  m1dvdsndvds  16746  pythagtrip  16782  pcgcd1  16825  prmpwdvds  16852  prmreclem2  16865  prmreclem3  16866  prmreclem5  16868  prmreclem6  16869  vdwlem6  16934  vdwnnlem2  16944  vdwnnlem3  16945  vdwnn  16946  prmlem0  17053  prmlem1a  17054  divsfval  17487  mrisval  17572  ismri  17573  ismri2dad  17579  cidpropd  17652  cat1lem  18039  plttr  18282  joinval  18317  meetval  18331  acsfiindd  18495  isnsgrp  18633  smndex1n0mnd  18822  mgm2nsgrplem2  18829  sgrp2nmndlem3  18835  symgpssefmnd  19311  symgfix2  19331  pmtrdifellem4  19394  psgnunilem1  19408  psgnunilem5  19409  psgnunilem2  19410  psgnunilem3  19411  pmtrsn  19434  sylow1lem3  19515  sylow2alem2  19533  efgsfo  19654  ablfac1eulem  19989  ablfac1eu  19990  pgpfac1lem1  19991  pgpfac1lem5  19996  nzrunit  20445  zrninitoringc  20597  islbs  21016  lbsind  21020  lbspss  21022  lbspropd  21039  lspsnne1  21060  islbs2  21097  lbsacsbs  21099  lbsextlem1  21101  lbsextlem3  21103  lbsextlem4  21104  lbsextg  21105  frlmlbs  21740  islindf  21755  islinds2  21756  islindf2  21757  lindfind  21759  lindsind  21760  lindfrn  21764  lindfmm  21770  lsslindf  21773  islindf4  21781  opsrtoslem2  21997  psdmul  22087  cply1coe0  22222  cply1coe0bi  22223  mdetunilem7  22539  mdetunilem8  22540  mdetunilem9  22541  maducoeval2  22561  pmatcollpw3fi1lem1  22707  fvmptnn04ifa  22771  fvmptnn04ifc  22773  fvmptnn04ifd  22774  chfacffsupp  22777  chfacfscmul0  22779  chfacfpmmul0  22783  elcls  22994  maxlp  23068  perfi  23076  ordtbaslem  23109  ordtval  23110  ordtbas2  23112  ordtopn1  23115  ordtopn2  23116  ordtcnv  23122  ordtrest  23123  ordtrest2lem  23124  ordtrest2  23125  pnfnei  23141  mnfnei  23142  isreg2  23298  ordthauslem  23304  cmpfi  23329  cmpfii  23330  bwth  23331  nconnsubb  23344  hausdiag  23566  txkgen  23573  kqdisj  23653  ordthmeolem  23722  fbfinnfr  23762  trfbas  23765  fbunfip  23790  fbasrn  23805  trfil3  23809  ufileu  23840  fin1aufil  23853  hausflim  23902  alexsubALTlem2  23969  alexsubALTlem3  23970  alexsubALTlem4  23971  ptcmplem2  23974  ptcmplem3  23975  stdbdbl  24439  iccntr  24744  reconnlem2  24750  iccpnfcnv  24876  xrhmeo  24878  lebnumlem1  24894  lebnumlem2  24895  lebnumlem3  24896  bcthlem4  25261  minveclem3b  25362  ivthlem2  25387  ivthlem3  25388  mbfmax  25584  mbfposr  25587  i1fd  25616  mbfi1fseqlem4  25653  itg2splitlem  25683  itg2monolem1  25685  itg2cnlem1  25696  dvne0  25950  lhop1lem  25952  deg1nn0clb  26029  dgrle  26182  coemulhi  26193  aaliou3lem9  26292  cos11  26476  logleb  26546  argrege0  26554  logdivle  26565  ellogdm  26582  cxple  26638  cxplt2  26641  cxple3  26644  isosctrlem1  26762  atandm  26820  atans2  26875  atantayl2  26882  eldmgm  26966  ftalem7  27023  isppw2  27059  musum  27135  dchrsum2  27213  bposlem1  27229  lgsmod  27268  lgsdir2lem2  27271  lgsdir2  27275  lgsne0  27280  lgsprme0  27284  gausslemma2dlem4  27314  lgsquadlem1  27325  2lgslem3  27349  2lgsoddprm  27361  2sq2  27378  addsqrexnreu  27387  rpvmasumlem  27432  padicabv  27575  ostth3  27583  ostth  27584  noextenddif  27614  nodenselem4  27633  nodenselem5  27634  nodenselem7  27636  nolt02o  27641  nogt01o  27642  noresle  27643  nosupprefixmo  27646  noinfprefixmo  27647  nosupcbv  27648  nosupdm  27650  nosupfv  27652  nosupres  27653  nosupbnd1lem1  27654  nosupbnd1lem3  27656  nosupbnd1lem5  27658  nosupbnd1  27660  nosupbnd2lem1  27661  nosupbnd2  27662  noinfcbv  27663  noinfdm  27665  noinffv  27667  noinfres  27668  noinfbnd1lem1  27669  noinfbnd1lem3  27671  noinfbnd1lem5  27673  noinfbnd1  27675  noinfbnd2lem1  27676  noinfbnd2  27677  slenlt  27698  sltne  27716  nocvxminlem  27724  slerec  27766  eqscut3  27771  cuteq1  27784  newbday  27852  sltlpss  27858  cofcutr  27873  lrrecfr  27891  addsval  27910  sltadd2  27939  sleneg  27993  slesubsubbd  28031  slesubsub2bd  28032  slesubsub3bd  28033  slesubaddd  28038  sltmul2  28115  slemul2d  28118  slemul1d  28119  onscutlt  28206  istrkgld  28440  axtgupdim2  28452  tglowdim2l  28631  axlowdimlem16  28938  axlowdim2  28941  axlowdim  28942  numedglnl  29125  usgredg2v  29208  lfuhgr1v0e  29235  cusgrfi  29440  vtxd0nedgb  29470  vtxduhgr0edgnel  29476  1loopgrnb0  29484  1hevtxdg0  29487  vtxdgoddnumeven  29535  wlkp1lem1  29653  wlkp1lem2  29654  wlkp1lem5  29657  dfpth2  29710  crctcsh  29805  clwlkclwwlklem2a4  29977  eupth2eucrct  30197  eupth2lem3lem3  30210  eupth2lem3lem4  30211  eupth2lem3lem6  30213  eupth2lem3lem7  30214  eupth2lems  30218  eupth2  30219  konigsberglem4  30235  nfrgr2v  30252  frgrwopreglem3  30294  fusgr2wsp2nb  30314  frgrreggt1  30373  friendshipgt3  30378  lpni  30460  nmobndseqi  30759  minvecolem5  30861  chpsscon3  31483  chnle  31494  nonbooli  31631  pjnel  31706  specval  31878  nmcfnlbi  32032  stri  32237  hstri  32245  cvbr  32262  cvcon3  32264  chcv1  32335  cvexchlem  32348  chrelat2  32350  nelun  32493  elpreq  32508  nelpr  32511  ifeqeqx  32522  nfpconfp  32607  suppiniseg  32660  isoun  32676  suppss3  32698  xrge0infss  32734  infxrge0gelb  32740  eliccelico  32751  elicoelioo  32752  nndiffz1  32760  hashgt1  32784  expgt0b  32792  nn0min  32796  ccatws1f1o  32924  toslublem  32945  tosglblem  32947  pmtrcnel  33062  cycpmco2  33106  isarchi2  33155  archiabl  33168  elrgspnlem2  33211  elrgspnlem3  33212  0nellinds  33335  lindssn  33343  lindfpropd  33347  ssdifidlprm  33423  mxidlirred  33437  ssmxidl  33439  lbslsat  33606  lindsunlem  33614  rtelextdg2lem  33710  constrsqrtcl  33763  ordtcnvNEW  33904  ordtrestNEW  33905  ordtrest2NEWlem  33906  ordtrest2NEW  33907  ordtconnlem1  33908  xrge0iifcnv  33917  esumpcvgval  34062  esum2d  34077  ddemeas  34220  omssubadd  34285  oddpwdc  34339  eulerpartlems  34345  eulerpartlemf  34355  eulerpartlemt  34356  eulerpartlemr  34359  eulerpartlemgvv  34361  eulerpartlemn  34366  ballotlemfc0  34478  ballotlemfcc  34479  ballotlem4  34484  ballotlemimin  34491  ballotlem7  34521  plymulx  34533  signsply0  34536  reprinfz1  34607  reprpmtf1o  34611  reprdifc  34612  hgt750lema  34642  hgt750leme  34643  istrkg2d  34651  bnj23  34702  bnj1185  34777  bnj1228  34995  bnj1388  35017  bnj1417  35025  nummin  35075  axnulg  35076  onvf1odlem2  35085  onvf1odlem3  35086  revwlk  35106  isacycgr  35126  acycgr0v  35129  prclisacycgr  35132  erdszelem10  35181  satf0n0  35359  fmlaomn0  35371  fmlasucdisj  35380  satfv1fvfmla1  35404  satefvfmla1  35406  ismfs  35530  mvtinf  35536  untelirr  35689  untsucf  35691  untangtr  35695  dfon2lem3  35767  dfon2lem4  35768  dfon2lem7  35771  dfon2lem9  35773  distel  35785  funpartfv  35927  dfrdg4  35933  nn0prpwlem  36304  nn0prpw  36305  limsucncmpi  36427  limsucncmp  36428  ordcmp  36429  weiunlem2  36445  weiunfrlem  36446  weiunfr  36449  unblimceq0  36489  unbdqndv1  36490  bj-hbntbi  36686  bj-equsexvwd  36763  bj-cbvexdv  36782  bj-ru1  36925  bj-nuliota  37039  topdifinffinlem  37329  topdifinffin  37330  icorempo  37333  relowlpssretop  37346  finxpreclem2  37372  finxpreclem6  37378  wl-issetft  37564  wl-ax11-lem8  37574  leceifl  37597  lindsadd  37601  lindsenlbs  37603  matunitlindflem1  37604  poimirlem16  37624  poimirlem17  37625  poimirlem18  37626  poimirlem19  37627  poimirlem21  37629  poimirlem23  37631  poimirlem26  37634  poimirlem27  37635  poimirlem28  37636  poimirlem31  37639  poimir  37641  mblfinlem2  37646  mblfinlem3  37647  ismblfin  37649  cnambfre  37656  itg2addnclem  37659  itg2addnclem2  37660  iblabsnclem  37671  ftc1anclem1  37681  areacirc  37701  heibor1lem  37797  heiborlem1  37799  heiborlem6  37804  heiborlem8  37806  heiborlem10  37808  smprngopr  38040  ecin0  38328  ax12inda  38935  riotaclbgBAD  38941  lcvfbr  39007  lcvbr  39008  lsatcv0  39018  l1cvpat  39041  opltcon3b  39191  cvrfval  39255  cvrval  39256  cvrnbtwn  39258  cvrval2  39261  cvrnbtwn2  39262  cvrnbtwn3  39263  cvrcon3b  39264  cvrnbtwn4  39266  atnlt  39300  iscvlat  39310  cvlexch1  39315  hlsuprexch  39369  hlrelat5N  39389  hlrelat2  39391  cvrval5  39403  3dimlem1  39446  3dim1lem5  39454  3dim2  39456  3dim3  39457  llnnlt  39511  islpln5  39523  lplni2  39525  lvolex3N  39526  lplnnle2at  39529  islpln2a  39536  lplnribN  39539  lplnexllnN  39552  lplnnlt  39553  lvoli3  39565  islvol5  39567  lvoli2  39569  lvolnle3at  39570  islvol2aN  39580  4atlem11  39597  lvolnltN  39606  dalawlem15  39873  4atexlemex2  40059  4atex  40064  4atex2-0aOLDN  40066  4atex2-0cOLDN  40068  lautcvr  40080  ltrnfset  40105  ltrnset  40106  ltrnu  40109  trlfset  40148  trlset  40149  trlval2  40151  cdlemd6  40191  cdleme0nex  40278  cdleme18d  40283  cdleme25b  40342  cdleme25cv  40346  cdleme29b  40363  cdleme31fv  40378  cdleme31fv2  40381  cdlemefrs29bpre0  40384  cdlemefr32sn2aw  40392  cdlemefr29bpre0N  40394  cdlemefr29clN  40395  cdlemefr32fvaN  40397  cdlemefr32fva1  40398  cdlemefs32sn1aw  40402  cdleme32fva  40425  cdleme32fvaw  40427  cdleme40v  40457  cdleme42b  40466  cdleme46f2g2  40481  cdleme46f2g1  40482  cdleme48gfv  40525  cdlemg1fvawlemN  40561  cdlemg1cex  40576  cdlemg6d  40609  cdlemm10N  41106  dicffval  41162  dicfval  41163  dicval  41164  dicfnN  41171  dicvalrelN  41173  dihffval  41218  dihfval  41219  dihlsscpre  41222  dvh4dimat  41426  dvh3dimatN  41427  dvh4dimlem  41431  dvh3dim  41434  dvh4dimN  41435  dvh3dim2  41436  dvh3dim3N  41437  mapdcv  41648  mapdh9aOLDN  41778  hdmapfval  41815  hdmapval  41816  hdmapval2  41820  hdmap11lem2  41830  dvrelog2b  42048  aks4d1p4  42061  aks4d1p5  42062  aks4d1p7  42065  aks4d1p8d2  42067  aks4d1p8  42069  aks4d1  42071  aks6d1c2p2  42101  hashnexinj  42110  rspcsbnea  42113  aks6d1c5  42121  aks6d1c6lem3  42154  aks6d1c7  42166  supinf  42224  oexpreposd  42304  mullt0b2d  42466  flt4lem7  42641  nna4b4nsq  42642  ellz1  42749  rencldnfilem  42802  jm2.22  42978  jm2.23  42979  wepwsolem  43025  fnwe2lem2  43034  aomclem8  43044  unxpwdom3  43078  onsupmaxb  43222  onexlimgt  43226  onsupeqnmax  43230  onov0suclim  43257  oaordnr  43279  omnord1  43288  oenord1  43299  oaomoencom  43300  oenass  43302  cantnfresb  43307  tfsnfin  43335  ralopabb  43394  nlimsuc  43424  ifpbi12  43471  dfsucon  43506  sqrtcvallem1  43614  ss2iundf  43642  frege124d  43744  clsk3nimkb  44023  clsk1indlem1  44028  clsk1independent  44029  ntrneineine1lem  44067  ntrneicls11  44073  clsneiel1  44091  clsneiel2  44092  neicvgel1  44102  neicvgel2  44103  radcnvrat  44297  rusbcALT  44422  en3lpVD  44828  0elaxnul  44967  omssaxinf2  44972  permaxnul  44992  permaxinf2lem  44996  nregmodel  45001  eliin2f  45092  nssd  45093  wessf1ornlem  45173  rexanuz2nf  45482  limsupre2lem  45716  icccncfext  45879  stoweidlem14  46006  stoweidlem34  46026  stoweidlem59  46051  etransclem24  46250  nnfoctbdjlem  46447  nnfoctbdj  46448  hspmbllem2  46619  nsssmfmbflem  46770  fsetsnprcnex  47050  eu2ndop1stv  47120  afvfv0bi  47147  afvco2  47171  ndmaovg  47179  ndfatafv2nrn  47216  afv2ndefb  47219  afv2fv0  47260  nelbr  47269  otiunsndisjX  47274  fun2dmnopgexmpl  47279  ltnltne  47294  readdcnnred  47298  resubcnnred  47299  recnmulnred  47300  cndivrenred  47301  ichnreuop  47467  fmtnoinf  47531  odz2prm2pw  47558  prmdvdsfmtnof1lem2  47580  lighneallem3  47602  lighneallem4  47605  requad1  47617  isodd3  47647  bits0ALTV  47674  nfermltl8rev  47737  nfermltl2rev  47738  nfermltlrev  47739  upgrimpths  47903  isubgr3stgrlem3  47961  usgrexmpl12ngric  48023  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  pgnbgreunbgrlem5lem1  48104  pgnbgreunbgrlem5lem2  48105  pgnbgreunbgrlem5lem3  48106  lgricngricex  48113  lidldomnnring  48218  ztprmneprm  48329  lindepsnlininds  48435  islindeps  48436  lindslinindsimp2lem5  48445  lindslinindsimp2  48446  line2ylem  48734  line2xlem  48736  map0cor  48837  nelsubc3lem  49053  fulltermc2  49495  setc1onsubc  49585  cnelsubclem  49586  elsetrecslem  49682