Theorem notbid 307

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

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

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 197

This theorem is referenced by:  notbi  308  annotanannot  823  ifpbi123d  1064  con3ALT  1069  nanbi1  1603  xorbi12d  1626  cbvexvw  2126  hba1wOLD  2132  hbe1w  2133  cbvexv1  2337  cbvex  2433  cbvexv  2435  cbvex2  2439  cbvexdva  2441  drex1  2477  eujustALT  2621  necon3abid  2979  neleq12d  3050  cbvrexf  3315  gencbval  3404  spcegf  3441  spc2gv  3448  spc3gv  3450  cdeqnot  3576  ru  3587  sbcng  3629  sbcrext  3662  cbvrexcsf  3716  difjust  3726  eldif  3734  dfpss3  3844  dfdif3  3872  difeq2  3874  disjne  4166  pssdifcom1  4197  eldifpr  4344  elpwunsn  4363  eldiftp  4366  prel12OLD  4515  prel12gOLD  4519  preqsnd  4524  disjxun  4785  nalset  4930  pwnss  4962  dtru  4989  rexxfrd  5010  rexxfr2d  5012  rexxfrd2  5014  rexxfr  5017  dtruALT  5028  dtruALT2  5040  opthneg  5078  snopeqop  5099  otiunsndisj  5114  poeq1  5174  pocl  5178  swopo  5181  sotric  5197  sotrieq  5198  isso2i  5203  somo  5205  freq1  5220  frirr  5227  fr2nr  5228  frminex  5230  tz7.2  5234  wereu2  5247  poinxp  5323  frinxp  5325  posn  5328  frsn  5330  rexiunxp  5402  rexxpf  5409  intirr  5656  poirr2  5662  cnvpo  5818  predpoirr  5852  predfrirr  5853  nordeq  5886  ordtri1  5900  ordtri3  5903  ordtri3OLD  5904  fvmpti  6424  fndmdif  6465  rexrnmpt  6513  2f1fvneq  6661  f1imapss  6667  cbvexfo  6689  soisoi  6722  isopolem  6739  weniso  6748  canth  6752  riotaclb  6793  rexrnmpt2  6924  ndmovg  6965  sorpssuni  7094  sorpssint  7095  fr3nr  7127  dfwe2  7129  ordsucsssuc  7171  nlimsucg  7190  orduninsuc  7191  dfom2  7215  ssnlim  7231  f1oweALT  7300  frxp  7439  poxp  7441  wfrlem10  7578  smoword  7617  tz7.48lem  7690  oacan  7783  oaword  7784  omlimcl  7813  omeulem1  7817  nnaword  7862  nnmword  7868  nneob  7887  brdifun  7926  swoer  7927  undifixp  8099  boxcutc  8106  2dom  8183  php  8301  nndomo  8311  nnsdomo  8312  unxpdomlem2  8322  frfi  8362  unfilem1  8381  supeq3  8512  supeq123d  8513  supmo  8515  eqsup  8519  supub  8522  sup0  8529  suppr  8534  supisolem  8536  supisoex  8537  eqinf  8547  infval  8549  infmo  8558  infpr  8566  infempty  8569  oieq1  8574  ordtypecbv  8579  ordtypelem7  8586  wemapsolem  8612  canthwdom  8641  zfregcl  8656  elirrv  8658  elirr  8659  noinfep  8722  cantnfp1lem3  8742  rankr1clem  8848  carden2b  8994  domtri2  9016  alephord3  9102  alephdom2  9111  alephval3  9134  dfac9  9161  kmlem2  9176  kmlem4  9178  isfin4  9322  isfin7  9326  fin23lem11  9342  isf32lem5  9382  isf34lem4  9402  fin1a2lem6  9430  fin1a2lem7  9431  fin1a2lem12  9436  itunisuc  9444  ac6n  9510  zorn2g  9528  zornn0g  9530  ttukeylem7  9540  axpowndlem3  9624  axpowndlem4  9625  axregnd  9629  elgch  9647  engch  9653  fpwwe2lem13  9667  fpwwe2  9668  pwfseqlem1  9683  pwfseqlem3  9685  hargch  9698  addnidpi  9926  pinq  9952  nqereu  9954  ltsonq  9994  prlem934  10058  ltexprlem7  10067  addcanpr  10071  prlem936  10072  reclem2pr  10073  reclem3pr  10074  supexpr  10079  ltsosr  10118  supsrlem  10135  axpre-lttri  10189  axpre-sup  10193  xrlenlt  10306  axlttri  10312  axsup  10316  ltne  10337  dedekind  10403  readdcan  10413  leadd1  10699  ltsub1  10727  ltsub2  10728  leord1  10758  lediv1  11091  lemuldiv  11106  lerec  11109  le2msq  11126  infm3  11185  suprnub  11191  infregelb  11210  avgle1  11475  avgle2  11476  znnnlt1  11607  indstr  11960  zsupss  11981  uzsupss  11984  rpneg  12067  xralrple  12242  xleneg  12255  xltadd1  12292  xposdif  12298  xmulneg1  12305  xltmul1  12328  xrsupexmnf  12341  xrinfmexpnf  12342  xrsupsslem  12343  xrinfmsslem  12344  xrub  12348  supxrleub  12362  infxrgelb  12371  difreicc  12512  nn0disj  12664  nelfzo  12684  elfznelfzo  12782  fvinim0ffz  12796  injresinjlem  12797  ssnn0fi  12993  leexp2  13123  hashbnd  13328  hasheni  13341  hashbc  13440  wrdsymb0  13536  swrdnd  13642  swrdnd2  13643  repswswrd  13741  repswccat  13742  cshwidxmod  13759  cnpart  14189  sqrtlt  14211  limsuplt  14419  rlimrege0  14519  isercoll  14607  efle  15055  odd2np1  15274  sumodd  15320  divalglem7  15331  ndvdsadd  15343  fldivndvdslt  15347  bitsfval  15354  bitsval  15355  bits0  15359  bitsp1  15362  bitsmod  15367  bitscmp  15369  bitsinv1lem  15372  sadadd2lem2  15381  saddisjlem  15395  bitsshft  15406  gcdneg  15452  algcvgblem  15499  lcmneg  15525  isprm3  15604  dvdsnprmd  15611  isprm5  15627  rpexp  15640  phiprmpw  15689  m1dvdsndvds  15711  pythagtrip  15747  pcgcd1  15789  prmpwdvds  15816  prmreclem2  15829  prmreclem3  15830  prmreclem5  15832  prmreclem6  15833  vdwlem6  15898  vdwnnlem2  15908  vdwnnlem3  15909  vdwnn  15910  prmo1  15949  prmlem0  16020  prmlem1a  16021  divsfval  16416  mrisval  16499  ismri  16500  ismri2dad  16506  cidpropd  16578  plttr  17179  joinval  17214  meetval  17228  acsfiindd  17386  isnsgrp  17497  mgm2nsgrplem2  17615  sgrp2nmndlem3  17621  symgfix2  18044  pmtrdifellem4  18107  psgnunilem1  18121  psgnunilem5  18122  psgnunilem2  18123  psgnunilem3  18124  pmtrsn  18147  sylow1lem3  18223  sylow2alem2  18241  efgsfo  18360  ablfac1eulem  18680  ablfac1eu  18681  pgpfac1lem1  18682  pgpfac1lem5  18687  islbs  19290  lbsind  19294  lbspss  19296  lbspropd  19313  lspsnne1  19331  islbs2  19370  lbsacsbs  19372  lbsextlem1  19374  lbsextlem3  19376  lbsextlem4  19377  lbsextg  19378  nzrunit  19483  opsrtoslem2  19701  cply1coe0  19885  cply1coe0bi  19886  frlmlbs  20354  islindf  20369  islinds2  20370  islindf2  20371  lindfind  20373  lindsind  20374  lindfrn  20378  lindfmm  20384  lsslindf  20387  islindf4  20395  mdetunilem7  20643  mdetunilem8  20644  mdetunilem9  20645  maducoeval2  20665  pmatcollpw3fi1lem1  20812  fvmptnn04ifa  20876  fvmptnn04ifc  20878  fvmptnn04ifd  20879  chfacffsupp  20882  chfacfscmul0  20884  chfacfpmmul0  20888  elcls  21099  maxlp  21173  perfi  21181  ordtbaslem  21214  ordtval  21215  ordtbas2  21217  ordtopn1  21220  ordtopn2  21221  ordtcnv  21227  ordtrest  21228  ordtrest2lem  21229  ordtrest2  21230  pnfnei  21246  mnfnei  21247  isreg2  21403  ordthauslem  21409  cmpfi  21433  cmpfii  21434  bwth  21435  nconnsubb  21448  hausdiag  21670  txkgen  21677  kqdisj  21757  ordthmeolem  21826  fbfinnfr  21866  trfbas  21869  fbunfip  21894  fbasrn  21909  trfil3  21913  ufileu  21944  fin1aufil  21957  hausflim  22006  alexsubALTlem2  22073  alexsubALTlem3  22074  alexsubALTlem4  22075  ptcmplem2  22078  ptcmplem3  22079  stdbdbl  22543  iccntr  22845  reconnlem2  22851  iccpnfcnv  22964  xrhmeo  22966  lebnumlem1  22981  lebnumlem2  22982  lebnumlem3  22983  bcthlem4  23344  minveclem3b  23419  ivthlem2  23441  ivthlem3  23442  mbfmax  23637  mbfposr  23640  i1fd  23669  mbfi1fseqlem4  23706  itg2splitlem  23736  itg2monolem1  23738  itg2cnlem1  23749  dvne0  23995  lhop1lem  23997  deg1nn0clb  24071  dgrle  24220  coemulhi  24231  aaliou3lem9  24326  cos11  24501  logleb  24571  argrege0  24579  logdivle  24590  ellogdm  24607  cxple  24663  cxplt2  24666  cxple3  24669  isosctrlem1  24770  atandm  24825  atans2  24880  atantayl2  24887  eldmgm  24970  ftalem7  25027  isppw2  25063  musum  25139  dchrsum2  25215  bposlem1  25231  lgsmod  25270  lgsdir2lem2  25273  lgsdir2  25277  lgsne0  25282  lgsprme0  25286  gausslemma2dlem4  25316  lgsquadlem1  25327  2lgslem3  25351  2lgsoddprm  25363  rpvmasumlem  25398  padicabv  25541  ostth3  25549  ostth  25550  istrkgld  25580  axtgupdim2  25592  tglowdim2l  25767  axlowdimlem16  26059  axlowdim2  26062  axlowdim  26063  numedglnl  26262  usgredg2v  26342  lfuhgr1v0e  26370  cusgrfi  26590  vtxd0nedgb  26620  vtxduhgr0edgnel  26626  1loopgrnb0  26634  1hevtxdg0  26637  vtxdgoddnumeven  26685  wlkp1lem1  26806  wlkp1lem2  26807  wlkp1lem5  26810  crctcsh  26953  clwwlknclwwlkdifsOLD  27130  clwlkclwwlklem2a4  27148  eupth2eucrct  27398  eupth2lem3lem3  27411  eupth2lem3lem4  27412  eupth2lem3lem6  27414  eupth2lem3lem7  27415  eupth2lems  27419  eupth2  27420  konigsberglem4  27436  nfrgr2v  27455  frgrwopreglem3  27497  fusgr2wsp2nb  27517  frgrreggt1  27593  friendshipgt3  27598  lpni  27675  nmobndseqi  27975  minvecolem5  28078  chpsscon3  28703  chnle  28714  nonbooli  28851  pjnel  28926  specval  29098  nmcfnlbi  29252  stri  29457  hstri  29465  cvbr  29482  cvcon3  29484  chcv1  29555  cvexchlem  29568  chrelat2  29570  spc2d  29654  elpreq  29699  ifeqeqx  29700  isoun  29820  suppss3  29843  xrge0infss  29866  infxrge0gelb  29872  eliccelico  29880  elicoelioo  29881  nndiffz1  29889  nn0min  29908  toslublem  30008  tosglblem  30010  isarchi2  30080  archiabl  30093  ordtcnvNEW  30307  ordtrestNEW  30308  ordtrest2NEWlem  30309  ordtrest2NEW  30310  ordtconnlem1  30311  xrge0iifcnv  30320  elzdif0  30365  esumpcvgval  30481  esum2d  30496  ddemeas  30640  omssubadd  30703  oddpwdc  30757  eulerpartlems  30763  eulerpartlemf  30773  eulerpartlemt  30774  eulerpartlemr  30777  eulerpartlemgvv  30779  eulerpartlemn  30784  ballotlemfc0  30895  ballotlemfcc  30896  ballotlem4  30901  ballotlemimin  30908  ballotlem7  30938  plymulx  30966  signsply0  30969  reprinfz1  31041  reprpmtf1o  31045  reprdifc  31046  hgt750lema  31076  hgt750leme  31077  istrkg2d  31085  bnj23  31125  bnj1185  31203  bnj1228  31418  bnj1388  31440  bnj1417  31448  erdszelem10  31521  ismfs  31785  mvtinf  31791  untelirr  31924  untsucf  31926  untangtr  31930  ceqsralv2  31946  inffzOLD  31954  dfpo2  31984  dfon2lem3  32027  dfon2lem4  32028  dfon2lem7  32031  dfon2lem9  32033  distel  32046  frpomin  32076  soseq  32092  noextenddif  32159  nodenselem4  32175  nodenselem5  32176  nodenselem7  32178  nolt02o  32183  noresle  32184  noprefixmo  32186  nosupdm  32188  nosupfv  32190  nosupres  32191  nosupbnd1lem1  32192  nosupbnd1lem3  32194  nosupbnd1lem5  32196  nosupbnd1  32198  nosupbnd2lem1  32199  nosupbnd2  32200  slenlt  32215  nocvxminlem  32231  slerec  32261  funpartfv  32390  dfrdg4  32396  nn0prpwlem  32655  nn0prpw  32656  limsucncmpi  32782  limsucncmp  32783  ordcmp  32784  unblimceq0  32836  unbdqndv1  32837  bj-hbntbi  33033  bj-cbvexdv  33073  bj-cbvex2v  33075  bj-drex1v  33086  bj-nalset  33131  bj-dtru  33134  bj-ru0  33265  bj-nuliota  33351  topdifinffinlem  33533  topdifinffin  33534  icorempt2  33537  relowlpssretop  33550  finxpreclem2  33565  finxpreclem6  33571  wl-ax11-lem8  33704  leceifl  33732  lindsenlbs  33738  matunitlindflem1  33739  poimirlem16  33759  poimirlem17  33760  poimirlem18  33761  poimirlem19  33762  poimirlem21  33764  poimirlem23  33766  poimirlem26  33769  poimirlem27  33770  poimirlem28  33771  poimirlem31  33774  poimir  33776  mblfinlem2  33781  mblfinlem3  33782  ismblfin  33784  cnambfre  33791  itg2addnclem  33794  itg2addnclem2  33795  iblabsnclem  33806  ftc1anclem1  33818  areacirc  33838  heibor1lem  33941  heiborlem1  33943  heiborlem6  33948  heiborlem8  33950  heiborlem10  33952  smprngopr  34184  ecin0  34460  ax12inda  34757  riotaclbgBAD  34763  lcvfbr  34830  lcvbr  34831  lsatcv0  34841  l1cvpat  34864  opltcon3b  35014  cvrfval  35078  cvrval  35079  cvrnbtwn  35081  cvrval2  35084  cvrnbtwn2  35085  cvrnbtwn3  35086  cvrcon3b  35087  cvrnbtwn4  35089  atnlt  35123  iscvlat  35133  cvlexch1  35138  hlsuprexch  35190  hlrelat5N  35210  hlrelat2  35212  cvrval5  35224  3dimlem1  35267  3dim1lem5  35275  3dim2  35277  3dim3  35278  llnnlt  35332  islpln5  35344  lplni2  35346  lvolex3N  35347  lplnnle2at  35350  islpln2a  35357  lplnribN  35360  lplnexllnN  35373  lplnnlt  35374  lvoli3  35386  islvol5  35388  lvoli2  35390  lvolnle3at  35391  islvol2aN  35401  4atlem11  35418  lvolnltN  35427  dalawlem15  35694  4atexlemex2  35880  4atex  35885  4atex2-0aOLDN  35887  4atex2-0cOLDN  35889  lautcvr  35901  ltrnfset  35926  ltrnset  35927  ltrnu  35930  trlfset  35970  trlset  35971  trlval2  35973  cdlemd6  36013  cdleme0nex  36100  cdleme18d  36105  cdleme25b  36164  cdleme25cv  36168  cdleme29b  36185  cdleme31fv  36200  cdleme31fv2  36203  cdlemefrs29bpre0  36206  cdlemefr32sn2aw  36214  cdlemefr29bpre0N  36216  cdlemefr29clN  36217  cdlemefr32fvaN  36219  cdlemefr32fva1  36220  cdlemefs32sn1aw  36224  cdleme32fva  36247  cdleme32fvaw  36249  cdleme40v  36279  cdleme42b  36288  cdleme46f2g2  36303  cdleme46f2g1  36304  cdleme48gfv  36347  cdlemg1fvawlemN  36383  cdlemg1cex  36398  cdlemg6d  36431  cdlemm10N  36929  dicffval  36985  dicfval  36986  dicval  36987  dicfnN  36994  dicvalrelN  36996  dihffval  37041  dihfval  37042  dihlsscpre  37045  dvh4dimat  37249  dvh3dimatN  37250  dvh4dimlem  37254  dvh3dim  37257  dvh4dimN  37258  dvh3dim2  37259  dvh3dim3N  37260  mapdcv  37471  mapdh9aOLDN  37601  hdmapfval  37638  hdmapval  37639  hdmapval2  37643  hdmap11lem2  37653  ellz1  37857  rencldnfilem  37911  jm2.22  38089  jm2.23  38090  wepwsolem  38139  fnwe2lem2  38148  aomclem8  38158  unxpwdom3  38192  ifpbi12  38360  ifpbi123  38362  relintabex  38414  ss2iundf  38478  frege124d  38580  clsk3nimkb  38865  clsk1indlem1  38870  clsk1independent  38871  ntrneineine1lem  38909  ntrneicls11  38915  clsneiel1  38933  clsneiel2  38934  neicvgel1  38944  neicvgel2  38945  radcnvrat  39040  rusbcALT  39167  en3lpVD  39603  eliin2f  39809  nssd  39810  wessf1ornlem  39892  limsupre2lem  40475  icccncfext  40619  stoweidlem14  40749  stoweidlem34  40769  stoweidlem59  40794  etransclem24  40993  nnfoctbdjlem  41190  nnfoctbdj  41191  hspmbllem2  41362  smfmbfcex  41489  nsssmfmbflem  41507  eu2ndop1stv  41723  afvfv0bi  41753  afvco2  41777  ndmaovg  41785  nelbr  41815  otiunsndisjX  41822  fun2dmnopgexmpl  41827  ltnltne  41842  fmtnoinf  41977  odz2prm2pw  42004  prmdvdsfmtnof1lem2  42026  lighneallem3  42053  lighneallem4  42056  isodd3  42094  bits0ALTV  42119  lidldomnnring  42459  zrninitoringc  42600  ztprmneprm  42654  lindepsnlininds  42770  islindeps  42771  lindslinindsimp2lem5  42780  lindslinindsimp2  42781  difmodm1lt  42846  elsetrecslem  42974