Theorem notbid 310

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

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

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 199

This theorem is referenced by:  notbi  311  annotanannot  825  ifpbi123d  1061  con3ALT  1068  con3ALTOLD  1069  nanbi1OLD  1571  xorbi12d  1596  cbvexvw  2087  hbe1w  2093  cbvexv1  2313  cbvex  2369  cbvexv  2371  cbvex2  2375  cbvexdva  2377  drex1  2407  eujustALT  2590  necon3abid  3005  neleq12d  3079  cbvrexf  3362  gencbval  3454  spcegf  3491  spc2gv  3498  spc3gv  3500  cdeqnot  3640  ru  3651  sbcng  3694  sbcrext  3729  cbvrexcsf  3784  difjust  3794  eldif  3802  dfpss3  3915  dfdif3  3943  difeq2  3945  disjne  4247  pssdifcom1  4278  eldifpr  4426  elpwunsn  4452  eldiftp  4455  prel12OLD  4611  prel12gOLD  4615  preqsnd  4620  disjxun  4884  nalset  5032  pwnss  5064  dtru  5082  dtruALT  5099  rexxfrd  5121  rexxfr2d  5123  rexxfrd2  5125  rexxfr  5128  dtruALT2  5143  opthneg  5181  snopeqop  5202  otiunsndisj  5217  poeq1  5277  pocl  5281  swopo  5284  sotric  5301  sotrieq  5302  isso2i  5308  somo  5310  freq1  5325  frirr  5332  fr2nr  5333  frminex  5335  tz7.2  5339  wereu2  5352  poinxp  5430  frinxp  5432  posn  5435  frsn  5437  rexiunxp  5508  rexxpf  5515  intirr  5769  poirr2  5775  cnvpo  5927  predpoirr  5961  predfrirr  5962  nordeq  5995  ordtri1  6009  ordtri3  6012  fvmpti  6541  fndmdif  6584  rexrnmpt  6633  2f1fvneq  6789  f1imapss  6795  cbvexfo  6817  soisoi  6850  isopolem  6867  weniso  6876  canth  6880  riotaclb  6921  rexrnmpt2  7053  ndmovg  7094  sorpssuni  7223  sorpssint  7224  fr3nr  7257  dfwe2  7259  ordsucsssuc  7301  nlimsucg  7320  orduninsuc  7321  dfom2  7345  ssnlim  7361  f1oweALT  7429  frxp  7568  poxp  7570  wfrlem10  7707  smoword  7746  tz7.48lem  7819  oacan  7912  oaword  7913  omlimcl  7942  omeulem1  7946  nnaword  7991  nnmword  7997  nneob  8016  brdifun  8055  swoer  8056  undifixp  8230  boxcutc  8237  2dom  8314  php  8432  nndomo  8442  nnsdomo  8443  unxpdomlem2  8453  frfi  8493  unfilem1  8512  supeq3  8643  supeq123d  8644  supmo  8646  eqsup  8650  supub  8653  sup0  8660  suppr  8665  supisolem  8667  supisoex  8668  eqinf  8678  infval  8680  infmo  8689  infpr  8697  infempty  8701  oieq1  8706  ordtypecbv  8711  ordtypelem7  8718  wemapsolem  8744  canthwdom  8773  zfregcl  8788  elirrv  8790  elirr  8791  noinfep  8854  cantnfp1lem3  8874  rankr1clem  8980  carden2b  9126  domtri2  9148  alephord3  9234  alephdom2  9243  alephval3  9266  dfac9  9293  kmlem2  9308  kmlem4  9310  isfin4  9454  isfin7  9458  fin23lem11  9474  isf32lem5  9514  isf34lem4  9534  fin1a2lem6  9562  fin1a2lem7  9563  fin1a2lem12  9568  itunisuc  9576  ac6n  9642  zorn2g  9660  zornn0g  9662  ttukeylem7  9672  axpowndlem3  9756  axpowndlem4  9757  axregnd  9761  elgch  9779  engch  9785  fpwwe2lem13  9799  fpwwe2  9800  pwfseqlem1  9815  pwfseqlem3  9817  hargch  9830  addnidpi  10058  pinq  10084  nqereu  10086  ltsonq  10126  prlem934  10190  ltexprlem7  10199  addcanpr  10203  prlem936  10204  reclem2pr  10205  reclem3pr  10206  supexpr  10211  ltsosr  10251  supsrlem  10268  axpre-lttri  10322  axpre-sup  10326  xrlenlt  10442  axlttri  10448  axsup  10452  ltne  10473  dedekind  10539  readdcan  10550  leadd1  10843  ltsub1  10871  ltsub2  10872  leord1  10902  lediv1  11242  lemuldiv  11257  lerec  11260  le2msq  11277  infm3  11336  suprnub  11342  infregelb  11361  avgle1  11622  avgle2  11623  znnnlt1  11756  indstr  12063  zsupss  12084  uzsupss  12087  rpneg  12171  xralrple  12348  xleneg  12361  xltadd1  12398  xposdif  12404  xmulneg1  12411  xltmul1  12434  xrsupexmnf  12447  xrinfmexpnf  12448  xrsupsslem  12449  xrinfmsslem  12450  xrub  12454  supxrleub  12468  infxrgelb  12477  difreicc  12621  nn0disj  12774  nelfzo  12794  elfznelfzo  12892  fvinim0ffz  12906  injresinjlem  12907  ssnn0fi  13103  leexp2  13233  hashbnd  13441  hasheni  13453  hashbc  13551  wrdsymb0  13639  swrdnd  13749  swrdnd2  13750  pfxnd0  13797  repswswrd  13930  repswccat  13932  cshwidxmod  13954  cnpart  14387  sqrtlt  14409  limsuplt  14618  rlimrege0  14718  isercoll  14806  efle  15250  odd2np1  15469  sumodd  15518  divalglem7  15529  ndvdsadd  15540  fldivndvdslt  15544  bitsfval  15551  bitsval  15552  bits0  15556  bitsp1  15559  bitsmod  15564  bitscmp  15566  bitsinv1lem  15569  sadadd2lem2  15578  saddisjlem  15592  bitsshft  15603  gcdneg  15649  algcvgblem  15696  lcmneg  15722  isprm3  15801  dvdsnprmd  15808  isprm5  15823  rpexp  15836  phiprmpw  15885  m1dvdsndvds  15907  pythagtrip  15943  pcgcd1  15985  prmpwdvds  16012  prmreclem2  16025  prmreclem3  16026  prmreclem5  16028  prmreclem6  16029  vdwlem6  16094  vdwnnlem2  16104  vdwnnlem3  16105  vdwnn  16106  prmlem0  16211  prmlem1a  16212  divsfval  16593  mrisval  16676  ismri  16677  ismri2dad  16683  cidpropd  16755  plttr  17356  joinval  17391  meetval  17405  acsfiindd  17563  isnsgrp  17674  mgm2nsgrplem2  17793  sgrp2nmndlem3  17799  symgfix2  18219  pmtrdifellem4  18282  psgnunilem1  18296  psgnunilem5  18297  psgnunilem5OLD  18298  psgnunilem2  18299  psgnunilem3  18300  pmtrsn  18323  sylow1lem3  18399  sylow2alem2  18417  efgsfo  18537  ablfac1eulem  18858  ablfac1eu  18859  pgpfac1lem1  18860  pgpfac1lem5  18865  islbs  19471  lbsind  19475  lbspss  19477  lbspropd  19494  lspsnne1  19512  islbs2  19551  lbsacsbs  19553  lbsextlem1  19555  lbsextlem3  19557  lbsextlem4  19558  lbsextg  19559  nzrunit  19664  opsrtoslem2  19881  cply1coe0  20065  cply1coe0bi  20066  frlmlbs  20540  islindf  20555  islinds2  20556  islindf2  20557  lindfind  20559  lindsind  20560  lindfrn  20564  lindfmm  20570  lsslindf  20573  islindf4  20581  mdetunilem7  20829  mdetunilem8  20830  mdetunilem9  20831  maducoeval2  20851  pmatcollpw3fi1lem1  20998  fvmptnn04ifa  21062  fvmptnn04ifc  21064  fvmptnn04ifd  21065  chfacffsupp  21068  chfacfscmul0  21070  chfacfpmmul0  21074  elcls  21285  maxlp  21359  perfi  21367  ordtbaslem  21400  ordtval  21401  ordtbas2  21403  ordtopn1  21406  ordtopn2  21407  ordtcnv  21413  ordtrest  21414  ordtrest2lem  21415  ordtrest2  21416  pnfnei  21432  mnfnei  21433  isreg2  21589  ordthauslem  21595  cmpfi  21620  cmpfii  21621  bwth  21622  nconnsubb  21635  hausdiag  21857  txkgen  21864  kqdisj  21944  ordthmeolem  22013  fbfinnfr  22053  trfbas  22056  fbunfip  22081  fbasrn  22096  trfil3  22100  ufileu  22131  fin1aufil  22144  hausflim  22193  alexsubALTlem2  22260  alexsubALTlem3  22261  alexsubALTlem4  22262  ptcmplem2  22265  ptcmplem3  22266  stdbdbl  22730  iccntr  23032  reconnlem2  23038  iccpnfcnv  23151  xrhmeo  23153  lebnumlem1  23168  lebnumlem2  23169  lebnumlem3  23170  bcthlem4  23533  minveclem3b  23634  ivthlem2  23656  ivthlem3  23657  mbfmax  23853  mbfposr  23856  i1fd  23885  mbfi1fseqlem4  23922  itg2splitlem  23952  itg2monolem1  23954  itg2cnlem1  23965  dvne0  24211  lhop1lem  24213  deg1nn0clb  24287  dgrle  24436  coemulhi  24447  aaliou3lem9  24542  cos11  24717  logleb  24786  argrege0  24794  logdivle  24805  ellogdm  24822  cxple  24878  cxplt2  24881  cxple3  24884  isosctrlem1  24996  atandm  25054  atans2  25109  atantayl2  25116  eldmgm  25200  ftalem7  25257  isppw2  25293  musum  25369  dchrsum2  25445  bposlem1  25461  lgsmod  25500  lgsdir2lem2  25503  lgsdir2  25507  lgsne0  25512  lgsprme0  25516  gausslemma2dlem4  25546  lgsquadlem1  25557  2lgslem3  25581  2lgsoddprm  25593  rpvmasumlem  25628  padicabv  25771  ostth3  25779  ostth  25780  istrkgld  25810  axtgupdim2  25822  tglowdim2l  26001  axlowdimlem16  26306  axlowdim2  26309  axlowdim  26310  numedglnl  26493  usgredg2v  26573  lfuhgr1v0e  26601  cusgrfi  26806  vtxd0nedgb  26836  vtxduhgr0edgnel  26842  1loopgrnb0  26850  1hevtxdg0  26853  vtxdgoddnumeven  26901  wlkp1lem1  27024  wlkp1lem2  27025  wlkp1lem5  27028  crctcsh  27173  clwlkclwwlklem2a4  27377  eupth2eucrct  27621  eupth2lem3lem3  27634  eupth2lem3lem4  27635  eupth2lem3lem6  27637  eupth2lem3lem7  27638  eupth2lems  27642  eupth2  27643  konigsberglem4  27661  nfrgr2v  27680  frgrwopreglem3  27722  fusgr2wsp2nb  27742  frgrreggt1  27825  friendshipgt3  27830  lpni  27907  nmobndseqi  28206  minvecolem5  28309  chpsscon3  28934  chnle  28945  nonbooli  29082  pjnel  29157  specval  29329  nmcfnlbi  29483  stri  29688  hstri  29696  cvbr  29713  cvcon3  29715  chcv1  29786  cvexchlem  29799  chrelat2  29801  spc2d  29885  elpreq  29923  ifeqeqx  29924  isoun  30045  suppss3  30068  xrge0infss  30090  infxrge0gelb  30096  eliccelico  30103  elicoelioo  30104  nndiffz1  30112  nn0min  30131  toslublem  30229  tosglblem  30231  isarchi2  30301  archiabl  30314  lbslsat  30432  0nellinds  30434  lindsunlem  30438  ordtcnvNEW  30564  ordtrestNEW  30565  ordtrest2NEWlem  30566  ordtrest2NEW  30567  ordtconnlem1  30568  xrge0iifcnv  30577  elzdif0  30622  esumpcvgval  30738  esum2d  30753  ddemeas  30897  omssubadd  30960  oddpwdc  31014  eulerpartlems  31020  eulerpartlemf  31030  eulerpartlemt  31031  eulerpartlemr  31034  eulerpartlemgvv  31036  eulerpartlemn  31041  ballotlemfc0  31153  ballotlemfcc  31154  ballotlem4  31159  ballotlemimin  31166  ballotlem7  31196  plymulx  31225  signsply0  31228  reprinfz1  31302  reprpmtf1o  31306  reprdifc  31307  hgt750lema  31337  hgt750leme  31338  istrkg2d  31346  bnj23  31386  bnj1185  31463  bnj1228  31678  bnj1388  31700  bnj1417  31708  erdszelem10  31781  ismfs  32045  mvtinf  32051  untelirr  32182  untsucf  32184  untangtr  32188  ceqsralv2  32204  dfpo2  32239  dfon2lem3  32278  dfon2lem4  32279  dfon2lem7  32282  dfon2lem9  32284  distel  32297  frpomin  32327  soseq  32343  noextenddif  32410  nodenselem4  32426  nodenselem5  32427  nodenselem7  32429  nolt02o  32434  noresle  32435  noprefixmo  32437  nosupdm  32439  nosupfv  32441  nosupres  32442  nosupbnd1lem1  32443  nosupbnd1lem3  32445  nosupbnd1lem5  32447  nosupbnd1  32449  nosupbnd2lem1  32450  nosupbnd2  32451  slenlt  32466  nocvxminlem  32482  slerec  32512  funpartfv  32641  dfrdg4  32647  nn0prpwlem  32905  nn0prpw  32906  limsucncmpi  33027  limsucncmp  33028  ordcmp  33029  unblimceq0  33080  unbdqndv1  33081  bj-hbntbi  33283  bj-cbvexdv  33321  bj-cbvex2v  33323  bj-drex1v  33334  bj-nalset  33371  bj-dtru  33373  bj-ru0  33505  bj-nuliota  33591  topdifinffinlem  33790  topdifinffin  33791  icorempt2  33794  relowlpssretop  33807  finxpreclem2  33822  finxpreclem6  33828  wl-ax11-lem8  33963  wl-dfrexf  33982  leceifl  34025  lindsadd  34030  lindsenlbs  34032  matunitlindflem1  34033  poimirlem16  34053  poimirlem17  34054  poimirlem18  34055  poimirlem19  34056  poimirlem21  34058  poimirlem23  34060  poimirlem26  34063  poimirlem27  34064  poimirlem28  34065  poimirlem31  34068  poimir  34070  mblfinlem2  34075  mblfinlem3  34076  ismblfin  34078  cnambfre  34085  itg2addnclem  34088  itg2addnclem2  34089  iblabsnclem  34100  ftc1anclem1  34112  areacirc  34132  heibor1lem  34234  heiborlem1  34236  heiborlem6  34241  heiborlem8  34243  heiborlem10  34245  smprngopr  34477  ecin0  34747  ax12inda  35104  riotaclbgBAD  35110  lcvfbr  35176  lcvbr  35177  lsatcv0  35187  l1cvpat  35210  opltcon3b  35360  cvrfval  35424  cvrval  35425  cvrnbtwn  35427  cvrval2  35430  cvrnbtwn2  35431  cvrnbtwn3  35432  cvrcon3b  35433  cvrnbtwn4  35435  atnlt  35469  iscvlat  35479  cvlexch1  35484  hlsuprexch  35537  hlrelat5N  35557  hlrelat2  35559  cvrval5  35571  3dimlem1  35614  3dim1lem5  35622  3dim2  35624  3dim3  35625  llnnlt  35679  islpln5  35691  lplni2  35693  lvolex3N  35694  lplnnle2at  35697  islpln2a  35704  lplnribN  35707  lplnexllnN  35720  lplnnlt  35721  lvoli3  35733  islvol5  35735  lvoli2  35737  lvolnle3at  35738  islvol2aN  35748  4atlem11  35765  lvolnltN  35774  dalawlem15  36041  4atexlemex2  36227  4atex  36232  4atex2-0aOLDN  36234  4atex2-0cOLDN  36236  lautcvr  36248  ltrnfset  36273  ltrnset  36274  ltrnu  36277  trlfset  36316  trlset  36317  trlval2  36319  cdlemd6  36359  cdleme0nex  36446  cdleme18d  36451  cdleme25b  36510  cdleme25cv  36514  cdleme29b  36531  cdleme31fv  36546  cdleme31fv2  36549  cdlemefrs29bpre0  36552  cdlemefr32sn2aw  36560  cdlemefr29bpre0N  36562  cdlemefr29clN  36563  cdlemefr32fvaN  36565  cdlemefr32fva1  36566  cdlemefs32sn1aw  36570  cdleme32fva  36593  cdleme32fvaw  36595  cdleme40v  36625  cdleme42b  36634  cdleme46f2g2  36649  cdleme46f2g1  36650  cdleme48gfv  36693  cdlemg1fvawlemN  36729  cdlemg1cex  36744  cdlemg6d  36777  cdlemm10N  37274  dicffval  37330  dicfval  37331  dicval  37332  dicfnN  37339  dicvalrelN  37341  dihffval  37386  dihfval  37387  dihlsscpre  37390  dvh4dimat  37594  dvh3dimatN  37595  dvh4dimlem  37599  dvh3dim  37602  dvh4dimN  37603  dvh3dim2  37604  dvh3dim3N  37605  mapdcv  37816  mapdh9aOLDN  37946  hdmapfval  37983  hdmapval  37984  hdmapval2  37988  hdmap11lem2  37998  rru  38140  oexpreposd  38161  ellz1  38294  rencldnfilem  38348  jm2.22  38525  jm2.23  38526  wepwsolem  38575  fnwe2lem2  38584  aomclem8  38594  unxpwdom3  38628  ifpbi12  38795  ifpbi123  38797  relintabex  38848  ss2iundf  38912  frege124d  39014  clsk3nimkb  39298  clsk1indlem1  39303  clsk1independent  39304  ntrneineine1lem  39342  ntrneicls11  39348  clsneiel1  39366  clsneiel2  39367  neicvgel1  39377  neicvgel2  39378  radcnvrat  39473  rusbcALT  39599  en3lpVD  40018  eliin2f  40220  nssd  40221  wessf1ornlem  40298  limsupre2lem  40868  icccncfext  41032  stoweidlem14  41162  stoweidlem34  41182  stoweidlem59  41207  etransclem24  41406  nnfoctbdjlem  41600  nnfoctbdj  41601  hspmbllem2  41772  smfmbfcex  41899  nsssmfmbflem  41917  eu2ndop1stv  42170  afvfv0bi  42197  afvco2  42221  ndmaovg  42229  ndfatafv2nrn  42266  afv2ndefb  42269  afv2fv0  42310  nelbr  42319  otiunsndisjX  42324  fun2dmnopgexmpl  42329  ltnltne  42345  readdcnnred  42349  resubcnnred  42350  recnmulnred  42351  cndivrenred  42352  fmtnoinf  42473  odz2prm2pw  42500  prmdvdsfmtnof1lem2  42522  lighneallem3  42549  lighneallem4  42552  requad1  42564  isodd3  42594  bits0ALTV  42619  lidldomnnring  42949  zrninitoringc  43090  ztprmneprm  43144  lindepsnlininds  43260  islindeps  43261  lindslinindsimp2lem5  43270  lindslinindsimp2  43271  difmodm1lt  43336  line2ylem  43491  line2xlem  43493  elsetrecslem  43554