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  2004  cbvexvw  2036  cbvexdvaw  2038  excomimw  2043  hbe1w  2048  19.8aw  2050  exexw  2051  ru0  2127  cbvexv1  2343  cbvex2v  2345  drex1v  2373  cbvex  2403  cbvex2  2416  drex1  2445  eujustALT  2571  necon3abid  2968  neleq12d  3041  cbvrexdva  3223  cbvrexfw  3285  rexeqbidvvOLD  3316  cbvrexdva2  3328  cbvrexf  3340  cbvexeqsetf  3474  cgsex4gOLD  3508  ceqsex  3509  ceqsexv  3511  gencbval  3522  spcegf  3571  spc2gv  3579  spc2d  3581  spc3gv  3583  ceqsralbv  3636  cdeqnot  3751  rru  3762  ruOLD  3764  sbcng  3813  sbcrext  3848  cbvrexcsf  3917  difjust  3928  eldif  3936  dfpss3  4064  dfdif3OLD  4093  difeq2  4095  disjne  4430  pssdifcom1  4465  eldifpr  4634  rexsng  4652  elpwunsn  4660  eldiftp  4663  rexprg  4673  preqsnd  4835  disjxun  5117  nalset  5283  dtruALT2  5340  dtruALT  5358  rexxfrd  5379  rexxfr2d  5381  rexxfrd2  5383  rexxfr  5386  dtruOLD  5416  opthneg  5456  snopeqop  5481  otiunsndisj  5495  poeq1  5564  pocl  5569  swopo  5572  sotric  5591  sotrieq  5592  isso2i  5598  somo  5600  freq1  5621  frirr  5630  fr2nr  5631  frminex  5633  tz7.2  5637  wereu2  5651  poinxp  5735  frinxp  5737  posn  5740  frsn  5742  rexiunxp  5820  rexxpf  5827  intirr  6107  poirr2  6113  cnvpo  6276  dfpo2  6285  predpoirr  6322  predfrirr  6323  frpomin  6329  nordeq  6371  ordtri1  6385  ordtri3  6388  fvmpti  6984  fndmdif  7031  rexrnmptw  7084  rexrnmpt  7086  rexima  7229  f1imapss  7258  f1ounsn  7264  cbvexfo  7282  nf1const  7296  soisoi  7320  isopolem  7337  weniso  7346  imaeqsalvOLD  7356  canth  7357  riotaclb  7401  rexrnmpo  7545  ndmovg  7588  sorpssuni  7724  sorpssint  7725  fr3nr  7764  dfwe2  7766  ordsucsssuc  7815  nlimsucg  7835  orduninsuc  7836  dfom2  7861  ssnlim  7879  resf1extb  7928  f1oweALT  7969  frxp  8123  poxp  8125  frxp2  8141  frxp3  8148  xpord3inddlem  8151  soseq  8156  suppofssd  8200  suppcoss  8204  wfrlem10OLD  8330  smoword  8378  tz7.48lem  8453  oacan  8558  oaword  8559  omlimcl  8588  omeulem1  8592  nnaword  8637  nnmword  8643  nneob  8666  naddss1  8699  brdifun  8747  swoer  8748  undifixp  8946  boxcutc  8953  2dom  9042  php  9219  phpeqd  9224  nndomog  9225  phpOLD  9229  nndomogOLD  9233  onomeneq  9235  nnsdomo  9240  unxpdomlem2  9257  frfi  9291  unfilem1  9313  supeq3  9459  supeq123d  9460  supmo  9462  eqsup  9466  supub  9469  sup0  9477  suppr  9482  supisolem  9484  supisoex  9485  eqinf  9495  infval  9497  infmo  9507  infpr  9515  infempty  9519  oieq1  9524  ordtypecbv  9529  ordtypelem7  9536  wemapsolem  9562  canthwdom  9591  zfregcl  9606  elirrv  9608  elirr  9609  noinfep  9672  cantnfp1lem3  9692  ttrcltr  9728  rankr1clem  9832  carden2b  9979  domtri2  10001  alephord3  10090  alephdom2  10099  alephval3  10122  dfac9  10149  kmlem2  10164  kmlem4  10166  isfin4  10309  isfin7  10313  fin23lem11  10329  isf32lem5  10369  isf34lem4  10389  fin1a2lem6  10417  fin1a2lem7  10418  fin1a2lem12  10423  itunisuc  10431  ac6n  10497  zorn2g  10515  zornn0g  10517  ttukeylem7  10527  axpowndlem3  10611  axpowndlem4  10612  axregnd  10616  elgch  10634  engch  10640  fpwwe2lem12  10654  fpwwe2  10655  pwfseqlem1  10670  pwfseqlem3  10672  hargch  10685  addnidpi  10913  pinq  10939  nqereu  10941  ltsonq  10981  prlem934  11045  ltexprlem7  11054  addcanpr  11058  prlem936  11059  reclem2pr  11060  reclem3pr  11061  supexpr  11066  ltsosr  11106  supsrlem  11123  axpre-lttri  11177  axpre-sup  11181  xrlenlt  11298  axlttri  11304  axsup  11308  ltne  11330  dedekind  11396  readdcan  11407  leadd1  11703  ltsub1  11731  ltsub2  11732  leord1  11762  lediv1  12105  lemuldiv  12120  lerec  12123  le2msq  12140  infm3  12199  suprnub  12205  infregelb  12224  avgle1  12479  avgle2  12480  znnnlt1  12617  indstr  12930  zsupss  12951  uzsupss  12954  rpneg  13039  xralrple  13219  xleneg  13232  xltadd1  13270  xposdif  13276  xmulneg1  13283  xltmul1  13306  xrsupexmnf  13319  xrinfmexpnf  13320  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  supxrleub  13340  infxrgelb  13350  difreicc  13499  nn0disj  13659  nelfzo  13679  elfznelfzo  13786  fvinim0ffz  13800  injresinjlem  13801  ssnn0fi  14001  leexp2  14187  exp11nnd  14277  hashbnd  14352  hasheni  14364  hashfundm  14458  hashbc  14469  wrdsymb0  14565  swrdnd  14670  swrdnd2  14671  pfxnd0  14704  repswswrd  14800  repswccat  14802  cshwidxmod  14819  cnpart  15257  sqrtlt  15278  limsuplt  15493  rlimrege0  15593  isercoll  15682  efle  16134  odd2np1  16358  sumodd  16405  divalglem7  16416  ndvdsadd  16427  fldivndvdslt  16433  bitsfval  16440  bitsval  16441  bits0  16445  bitsp1  16448  bitsmod  16453  bitscmp  16455  bitsinv1lem  16458  sadadd2lem2  16467  saddisjlem  16481  bitsshft  16492  gcdneg  16539  algcvgblem  16594  lcmneg  16620  isprm3  16700  dvdsnprmd  16707  isprm5  16724  rpexp  16739  phiprmpw  16793  m1dvdsndvds  16816  pythagtrip  16852  pcgcd1  16895  prmpwdvds  16922  prmreclem2  16935  prmreclem3  16936  prmreclem5  16938  prmreclem6  16939  vdwlem6  17004  vdwnnlem2  17014  vdwnnlem3  17015  vdwnn  17016  prmlem0  17123  prmlem1a  17124  divsfval  17559  mrisval  17640  ismri  17641  ismri2dad  17647  cidpropd  17720  cat1lem  18107  plttr  18350  joinval  18385  meetval  18399  acsfiindd  18561  isnsgrp  18699  smndex1n0mnd  18888  mgm2nsgrplem2  18895  sgrp2nmndlem3  18901  symgpssefmnd  19375  symgfix2  19395  pmtrdifellem4  19458  psgnunilem1  19472  psgnunilem5  19473  psgnunilem2  19474  psgnunilem3  19475  pmtrsn  19498  sylow1lem3  19579  sylow2alem2  19597  efgsfo  19718  ablfac1eulem  20053  ablfac1eu  20054  pgpfac1lem1  20055  pgpfac1lem5  20060  nzrunit  20482  zrninitoringc  20634  islbs  21032  lbsind  21036  lbspss  21038  lbspropd  21055  lspsnne1  21076  islbs2  21113  lbsacsbs  21115  lbsextlem1  21117  lbsextlem3  21119  lbsextlem4  21120  lbsextg  21121  frlmlbs  21755  islindf  21770  islinds2  21771  islindf2  21772  lindfind  21774  lindsind  21775  lindfrn  21779  lindfmm  21785  lsslindf  21788  islindf4  21796  opsrtoslem2  22012  psdmul  22102  cply1coe0  22237  cply1coe0bi  22238  mdetunilem7  22554  mdetunilem8  22555  mdetunilem9  22556  maducoeval2  22576  pmatcollpw3fi1lem1  22722  fvmptnn04ifa  22786  fvmptnn04ifc  22788  fvmptnn04ifd  22789  chfacffsupp  22792  chfacfscmul0  22794  chfacfpmmul0  22798  elcls  23009  maxlp  23083  perfi  23091  ordtbaslem  23124  ordtval  23125  ordtbas2  23127  ordtopn1  23130  ordtopn2  23131  ordtcnv  23137  ordtrest  23138  ordtrest2lem  23139  ordtrest2  23140  pnfnei  23156  mnfnei  23157  isreg2  23313  ordthauslem  23319  cmpfi  23344  cmpfii  23345  bwth  23346  nconnsubb  23359  hausdiag  23581  txkgen  23588  kqdisj  23668  ordthmeolem  23737  fbfinnfr  23777  trfbas  23780  fbunfip  23805  fbasrn  23820  trfil3  23824  ufileu  23855  fin1aufil  23868  hausflim  23917  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  ptcmplem2  23989  ptcmplem3  23990  stdbdbl  24454  iccntr  24759  reconnlem2  24765  iccpnfcnv  24891  xrhmeo  24893  lebnumlem1  24909  lebnumlem2  24910  lebnumlem3  24911  bcthlem4  25277  minveclem3b  25378  ivthlem2  25403  ivthlem3  25404  mbfmax  25600  mbfposr  25603  i1fd  25632  mbfi1fseqlem4  25669  itg2splitlem  25699  itg2monolem1  25701  itg2cnlem1  25712  dvne0  25966  lhop1lem  25968  deg1nn0clb  26045  dgrle  26198  coemulhi  26209  aaliou3lem9  26308  cos11  26492  logleb  26562  argrege0  26570  logdivle  26581  ellogdm  26598  cxple  26654  cxplt2  26657  cxple3  26660  isosctrlem1  26778  atandm  26836  atans2  26891  atantayl2  26898  eldmgm  26982  ftalem7  27039  isppw2  27075  musum  27151  dchrsum2  27229  bposlem1  27245  lgsmod  27284  lgsdir2lem2  27287  lgsdir2  27291  lgsne0  27296  lgsprme0  27300  gausslemma2dlem4  27330  lgsquadlem1  27341  2lgslem3  27365  2lgsoddprm  27377  2sq2  27394  addsqrexnreu  27403  rpvmasumlem  27448  padicabv  27591  ostth3  27599  ostth  27600  noextenddif  27630  nodenselem4  27649  nodenselem5  27650  nodenselem7  27652  nolt02o  27657  nogt01o  27658  noresle  27659  nosupprefixmo  27662  noinfprefixmo  27663  nosupcbv  27664  nosupdm  27666  nosupfv  27668  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem3  27672  nosupbnd1lem5  27674  nosupbnd1  27676  nosupbnd2lem1  27677  nosupbnd2  27678  noinfcbv  27679  noinfdm  27681  noinffv  27683  noinfres  27684  noinfbnd1lem1  27685  noinfbnd1lem3  27687  noinfbnd1lem5  27689  noinfbnd1  27691  noinfbnd2lem1  27692  noinfbnd2  27693  slenlt  27714  sltne  27732  nocvxminlem  27739  slerec  27781  cuteq1  27795  newbday  27857  sltlpss  27862  cofcutr  27875  lrrecfr  27893  addsval  27912  sltadd2  27941  sleneg  27995  slesubsubbd  28033  slesubsub2bd  28034  slesubsub3bd  28035  slesubaddd  28040  sltmul2  28114  slemul2d  28117  slemul1d  28118  istrkgld  28384  axtgupdim2  28396  tglowdim2l  28575  axlowdimlem16  28882  axlowdim2  28885  axlowdim  28886  numedglnl  29069  usgredg2v  29152  lfuhgr1v0e  29179  cusgrfi  29384  vtxd0nedgb  29414  vtxduhgr0edgnel  29420  1loopgrnb0  29428  1hevtxdg0  29431  vtxdgoddnumeven  29479  wlkp1lem1  29599  wlkp1lem2  29600  wlkp1lem5  29603  dfpth2  29657  crctcsh  29752  clwlkclwwlklem2a4  29924  eupth2eucrct  30144  eupth2lem3lem3  30157  eupth2lem3lem4  30158  eupth2lem3lem6  30160  eupth2lem3lem7  30161  eupth2lems  30165  eupth2  30166  konigsberglem4  30182  nfrgr2v  30199  frgrwopreglem3  30241  fusgr2wsp2nb  30261  frgrreggt1  30320  friendshipgt3  30325  lpni  30407  nmobndseqi  30706  minvecolem5  30808  chpsscon3  31430  chnle  31441  nonbooli  31578  pjnel  31653  specval  31825  nmcfnlbi  31979  stri  32184  hstri  32192  cvbr  32209  cvcon3  32211  chcv1  32282  cvexchlem  32295  chrelat2  32297  nelun  32440  elpreq  32455  nelpr  32458  ifeqeqx  32469  nfpconfp  32556  suppiniseg  32609  isoun  32625  suppss3  32647  xrge0infss  32683  infxrge0gelb  32689  eliccelico  32700  elicoelioo  32701  nndiffz1  32709  hashgt1  32733  expgt0b  32741  nn0min  32745  ccatws1f1o  32873  toslublem  32898  tosglblem  32900  pmtrcnel  33046  cycpmco2  33090  isarchi2  33129  archiabl  33142  elrgspnlem2  33184  elrgspnlem3  33185  0nellinds  33331  lindssn  33339  lindfpropd  33343  ssdifidlprm  33419  mxidlirred  33433  ssmxidl  33435  lbslsat  33602  lindsunlem  33610  rtelextdg2lem  33706  constrsqrtcl  33759  ordtcnvNEW  33897  ordtrestNEW  33898  ordtrest2NEWlem  33899  ordtrest2NEW  33900  ordtconnlem1  33901  xrge0iifcnv  33910  esumpcvgval  34055  esum2d  34070  ddemeas  34213  omssubadd  34278  oddpwdc  34332  eulerpartlems  34338  eulerpartlemf  34348  eulerpartlemt  34349  eulerpartlemr  34352  eulerpartlemgvv  34354  eulerpartlemn  34359  ballotlemfc0  34471  ballotlemfcc  34472  ballotlem4  34477  ballotlemimin  34484  ballotlem7  34514  plymulx  34526  signsply0  34529  reprinfz1  34600  reprpmtf1o  34604  reprdifc  34605  hgt750lema  34635  hgt750leme  34636  istrkg2d  34644  bnj23  34695  bnj1185  34770  bnj1228  34988  bnj1388  35010  bnj1417  35018  nummin  35068  axnulg  35069  revwlk  35093  isacycgr  35113  acycgr0v  35116  prclisacycgr  35119  erdszelem10  35168  satf0n0  35346  fmlaomn0  35358  fmlasucdisj  35367  satfv1fvfmla1  35391  satefvfmla1  35393  ismfs  35517  mvtinf  35523  untelirr  35671  untsucf  35673  untangtr  35677  dfon2lem3  35749  dfon2lem4  35750  dfon2lem7  35753  dfon2lem9  35755  distel  35767  funpartfv  35909  dfrdg4  35915  nn0prpwlem  36286  nn0prpw  36287  limsucncmpi  36409  limsucncmp  36410  ordcmp  36411  weiunlem2  36427  weiunfrlem  36428  weiunfr  36431  unblimceq0  36471  unbdqndv1  36472  bj-hbntbi  36668  bj-equsexvwd  36745  bj-cbvexdv  36764  bj-ru1  36907  bj-nuliota  37021  topdifinffinlem  37311  topdifinffin  37312  icorempo  37315  relowlpssretop  37328  finxpreclem2  37354  finxpreclem6  37360  wl-issetft  37546  wl-ax11-lem8  37556  leceifl  37579  lindsadd  37583  lindsenlbs  37585  matunitlindflem1  37586  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem21  37611  poimirlem23  37613  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem31  37621  poimir  37623  mblfinlem2  37628  mblfinlem3  37629  ismblfin  37631  cnambfre  37638  itg2addnclem  37641  itg2addnclem2  37642  iblabsnclem  37653  ftc1anclem1  37663  areacirc  37683  heibor1lem  37779  heiborlem1  37781  heiborlem6  37786  heiborlem8  37788  heiborlem10  37790  smprngopr  38022  ecin0  38316  ax12inda  38912  riotaclbgBAD  38918  lcvfbr  38984  lcvbr  38985  lsatcv0  38995  l1cvpat  39018  opltcon3b  39168  cvrfval  39232  cvrval  39233  cvrnbtwn  39235  cvrval2  39238  cvrnbtwn2  39239  cvrnbtwn3  39240  cvrcon3b  39241  cvrnbtwn4  39243  atnlt  39277  iscvlat  39287  cvlexch1  39292  hlsuprexch  39346  hlrelat5N  39366  hlrelat2  39368  cvrval5  39380  3dimlem1  39423  3dim1lem5  39431  3dim2  39433  3dim3  39434  llnnlt  39488  islpln5  39500  lplni2  39502  lvolex3N  39503  lplnnle2at  39506  islpln2a  39513  lplnribN  39516  lplnexllnN  39529  lplnnlt  39530  lvoli3  39542  islvol5  39544  lvoli2  39546  lvolnle3at  39547  islvol2aN  39557  4atlem11  39574  lvolnltN  39583  dalawlem15  39850  4atexlemex2  40036  4atex  40041  4atex2-0aOLDN  40043  4atex2-0cOLDN  40045  lautcvr  40057  ltrnfset  40082  ltrnset  40083  ltrnu  40086  trlfset  40125  trlset  40126  trlval2  40128  cdlemd6  40168  cdleme0nex  40255  cdleme18d  40260  cdleme25b  40319  cdleme25cv  40323  cdleme29b  40340  cdleme31fv  40355  cdleme31fv2  40358  cdlemefrs29bpre0  40361  cdlemefr32sn2aw  40369  cdlemefr29bpre0N  40371  cdlemefr29clN  40372  cdlemefr32fvaN  40374  cdlemefr32fva1  40375  cdlemefs32sn1aw  40379  cdleme32fva  40402  cdleme32fvaw  40404  cdleme40v  40434  cdleme42b  40443  cdleme46f2g2  40458  cdleme46f2g1  40459  cdleme48gfv  40502  cdlemg1fvawlemN  40538  cdlemg1cex  40553  cdlemg6d  40586  cdlemm10N  41083  dicffval  41139  dicfval  41140  dicval  41141  dicfnN  41148  dicvalrelN  41150  dihffval  41195  dihfval  41196  dihlsscpre  41199  dvh4dimat  41403  dvh3dimatN  41404  dvh4dimlem  41408  dvh3dim  41411  dvh4dimN  41412  dvh3dim2  41413  dvh3dim3N  41414  mapdcv  41625  mapdh9aOLDN  41755  hdmapfval  41792  hdmapval  41793  hdmapval2  41797  hdmap11lem2  41807  dvrelog2b  42025  aks4d1p4  42038  aks4d1p5  42039  aks4d1p7  42042  aks4d1p8d2  42044  aks4d1p8  42046  aks4d1  42048  aks6d1c2p2  42078  hashnexinj  42087  rspcsbnea  42090  aks6d1c5  42098  aks6d1c6lem3  42131  aks6d1c7  42143  metakunt27  42190  metakunt28  42191  metakunt29  42192  supinf  42240  oexpreposd  42318  flt4lem7  42629  nna4b4nsq  42630  ellz1  42737  rencldnfilem  42790  jm2.22  42966  jm2.23  42967  wepwsolem  43013  fnwe2lem2  43022  aomclem8  43032  unxpwdom3  43066  onsupmaxb  43210  onexlimgt  43214  onsupeqnmax  43218  onov0suclim  43245  oaordnr  43267  omnord1  43276  oenord1  43287  oaomoencom  43288  oenass  43290  cantnfresb  43295  tfsnfin  43323  ralopabb  43382  nlimsuc  43412  ifpbi12  43459  dfsucon  43494  sqrtcvallem1  43602  ss2iundf  43630  frege124d  43732  clsk3nimkb  44011  clsk1indlem1  44016  clsk1independent  44017  ntrneineine1lem  44055  ntrneicls11  44061  clsneiel1  44079  clsneiel2  44080  neicvgel1  44090  neicvgel2  44091  radcnvrat  44286  rusbcALT  44411  en3lpVD  44817  0elaxnul  44956  omssaxinf2  44961  permaxnul  44981  permaxinf2lem  44985  eliin2f  45076  nssd  45077  wessf1ornlem  45157  rexanuz2nf  45467  limsupre2lem  45701  icccncfext  45864  stoweidlem14  45991  stoweidlem34  46011  stoweidlem59  46036  etransclem24  46235  nnfoctbdjlem  46432  nnfoctbdj  46433  hspmbllem2  46604  nsssmfmbflem  46755  fsetsnprcnex  47032  eu2ndop1stv  47102  afvfv0bi  47129  afvco2  47153  ndmaovg  47161  ndfatafv2nrn  47198  afv2ndefb  47201  afv2fv0  47242  nelbr  47251  otiunsndisjX  47256  fun2dmnopgexmpl  47261  ltnltne  47276  readdcnnred  47280  resubcnnred  47281  recnmulnred  47282  cndivrenred  47283  ichnreuop  47434  fmtnoinf  47498  odz2prm2pw  47525  prmdvdsfmtnof1lem2  47547  lighneallem3  47569  lighneallem4  47572  requad1  47584  isodd3  47614  bits0ALTV  47641  nfermltl8rev  47704  nfermltl2rev  47705  nfermltlrev  47706  upgrimpths  47870  isubgr3stgrlem3  47928  usgrexmpl12ngric  47990  lidldomnnring  48159  ztprmneprm  48270  lindepsnlininds  48376  islindeps  48377  lindslinindsimp2lem5  48386  lindslinindsimp2  48387  difmodm1lt  48450  line2ylem  48679  line2xlem  48681  map0cor  48781  nelsubc3lem  48985  fulltermc2  49345  setc1onsubc  49427  cnelsubclem  49428  elsetrecslem  49511