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  834  ifpbi123dOLD  1080  con3ALT  1086  xorbi12d  1526  equsexvw  2009  cbvexvw  2041  cbvexdvaw  2043  hbe1w  2052  19.8aw  2054  exexw  2055  cbvexv1  2339  cbvex2v  2341  drex1v  2369  cbvex  2399  cbvex2  2412  drex1  2441  eujustALT  2567  necon3abid  2978  neleq12d  3052  rexbiOLD  3106  cbvrexdva  3238  cbvrexfw  3303  rexeqbidvvOLD  3333  cbvrexdva2  3346  cbvrexf  3358  cgsex4gOLD  3522  ceqsex  3524  ceqsexv  3526  gencbval  3538  vtoclgft  3541  spcegf  3583  spc2gv  3591  spc2d  3593  spc3gv  3595  ceqsralbv  3646  cdeqnot  3765  rru  3776  ru  3777  sbcng  3828  sbcrext  3868  cbvrexcsf  3940  difjust  3951  eldif  3959  dfpss3  4087  dfdif3  4115  difeq2  4117  ab0OLD  4376  disjne  4455  pssdifcom1  4490  eldifpr  4661  rexsng  4679  elpwunsn  4688  eldiftp  4691  rexprg  4701  preqsnd  4860  disjxun  5147  nalset  5314  dtruALT2  5369  dtruALT  5387  rexxfrd  5408  rexxfr2d  5410  rexxfrd2  5412  rexxfr  5415  dtruOLD  5442  opthneg  5482  snopeqop  5507  otiunsndisj  5521  poeq1  5592  pocl  5596  poclOLD  5597  swopo  5600  sotric  5617  sotrieq  5618  isso2i  5624  somo  5626  freq1  5647  frirr  5654  fr2nr  5655  frminex  5657  tz7.2  5661  wereu2  5674  poinxp  5757  frinxp  5759  posn  5762  frsn  5764  rexiunxp  5841  rexxpf  5848  intirr  6120  poirr2  6126  cnvpo  6287  dfpo2  6296  predpoirr  6335  predfrirr  6336  frpomin  6342  nordeq  6384  ordtri1  6398  ordtri3  6401  fvmpti  6998  fndmdif  7044  rexrnmptw  7097  rexrnmpt  7099  2f1fvneq  7259  f1imapss  7265  cbvexfo  7288  nf1const  7302  soisoi  7325  isopolem  7342  weniso  7351  imaeqsalv  7361  canth  7362  riotaclb  7407  rexrnmpo  7548  ndmovg  7590  sorpssuni  7722  sorpssint  7723  fr3nr  7759  dfwe2  7761  ordsucsssuc  7811  nlimsucg  7831  orduninsuc  7832  dfom2  7857  ssnlim  7875  f1oweALT  7959  frxp  8112  poxp  8114  frxp2  8130  frxp3  8137  xpord3inddlem  8140  soseq  8145  suppofssd  8188  suppcoss  8192  wfrlem10OLD  8318  smoword  8366  tz7.48lem  8441  oacan  8548  oaword  8549  omlimcl  8578  omeulem1  8582  nnaword  8627  nnmword  8633  nneob  8655  naddss1  8688  brdifun  8732  swoer  8733  undifixp  8928  boxcutc  8935  2dom  9030  php  9210  phpeqd  9215  nndomog  9216  phpOLD  9222  nndomogOLD  9226  onomeneq  9228  nnsdomo  9234  unxpdomlem2  9251  frfi  9288  unfilem1  9310  supeq3  9444  supeq123d  9445  supmo  9447  eqsup  9451  supub  9454  sup0  9461  suppr  9466  supisolem  9468  supisoex  9469  eqinf  9479  infval  9481  infmo  9490  infpr  9498  infempty  9502  oieq1  9507  ordtypecbv  9512  ordtypelem7  9519  wemapsolem  9545  canthwdom  9574  zfregcl  9589  elirrv  9591  elirr  9592  noinfep  9655  cantnfp1lem3  9675  ttrcltr  9711  rankr1clem  9815  carden2b  9962  domtri2  9984  alephord3  10073  alephdom2  10082  alephval3  10105  dfac9  10131  kmlem2  10146  kmlem4  10148  isfin4  10292  isfin7  10296  fin23lem11  10312  isf32lem5  10352  isf34lem4  10372  fin1a2lem6  10400  fin1a2lem7  10401  fin1a2lem12  10406  itunisuc  10414  ac6n  10480  zorn2g  10498  zornn0g  10500  ttukeylem7  10510  axpowndlem3  10594  axpowndlem4  10595  axregnd  10599  elgch  10617  engch  10623  fpwwe2lem12  10637  fpwwe2  10638  pwfseqlem1  10653  pwfseqlem3  10655  hargch  10668  addnidpi  10896  pinq  10922  nqereu  10924  ltsonq  10964  prlem934  11028  ltexprlem7  11037  addcanpr  11041  prlem936  11042  reclem2pr  11043  reclem3pr  11044  supexpr  11049  ltsosr  11089  supsrlem  11106  axpre-lttri  11160  axpre-sup  11164  xrlenlt  11279  axlttri  11285  axsup  11289  ltne  11311  dedekind  11377  readdcan  11388  leadd1  11682  ltsub1  11710  ltsub2  11711  leord1  11741  lediv1  12079  lemuldiv  12094  lerec  12097  le2msq  12114  infm3  12173  suprnub  12179  infregelb  12198  avgle1  12452  avgle2  12453  znnnlt1  12589  indstr  12900  zsupss  12921  uzsupss  12924  rpneg  13006  xralrple  13184  xleneg  13197  xltadd1  13235  xposdif  13241  xmulneg1  13248  xltmul1  13271  xrsupexmnf  13284  xrinfmexpnf  13285  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  supxrleub  13305  infxrgelb  13314  difreicc  13461  nn0disj  13617  nelfzo  13637  elfznelfzo  13737  fvinim0ffz  13751  injresinjlem  13752  ssnn0fi  13950  leexp2  14136  hashbnd  14296  hasheni  14308  hashfundm  14402  hashbc  14412  wrdsymb0  14499  swrdnd  14604  swrdnd2  14605  pfxnd0  14638  repswswrd  14734  repswccat  14736  cshwidxmod  14753  cnpart  15187  sqrtlt  15208  limsuplt  15423  rlimrege0  15523  isercoll  15614  efle  16061  odd2np1  16284  sumodd  16331  divalglem7  16342  ndvdsadd  16353  fldivndvdslt  16357  bitsfval  16364  bitsval  16365  bits0  16369  bitsp1  16372  bitsmod  16377  bitscmp  16379  bitsinv1lem  16382  sadadd2lem2  16391  saddisjlem  16405  bitsshft  16416  gcdneg  16463  algcvgblem  16514  lcmneg  16540  isprm3  16620  dvdsnprmd  16627  isprm5  16644  rpexp  16659  phiprmpw  16709  m1dvdsndvds  16731  pythagtrip  16767  pcgcd1  16810  prmpwdvds  16837  prmreclem2  16850  prmreclem3  16851  prmreclem5  16853  prmreclem6  16854  vdwlem6  16919  vdwnnlem2  16929  vdwnnlem3  16930  vdwnn  16931  prmlem0  17039  prmlem1a  17040  divsfval  17493  mrisval  17574  ismri  17575  ismri2dad  17581  cidpropd  17654  cat1lem  18046  plttr  18295  joinval  18330  meetval  18344  acsfiindd  18506  isnsgrp  18614  smndex1n0mnd  18793  mgm2nsgrplem2  18800  sgrp2nmndlem3  18806  symgpssefmnd  19263  symgfix2  19284  pmtrdifellem4  19347  psgnunilem1  19361  psgnunilem5  19362  psgnunilem2  19363  psgnunilem3  19364  pmtrsn  19387  sylow1lem3  19468  sylow2alem2  19486  efgsfo  19607  ablfac1eulem  19942  ablfac1eu  19943  pgpfac1lem1  19944  pgpfac1lem5  19949  nzrunit  20301  islbs  20687  lbsind  20691  lbspss  20693  lbspropd  20710  lspsnne1  20730  islbs2  20767  lbsacsbs  20769  lbsextlem1  20771  lbsextlem3  20773  lbsextlem4  20774  lbsextg  20775  frlmlbs  21352  islindf  21367  islinds2  21368  islindf2  21369  lindfind  21371  lindsind  21372  lindfrn  21376  lindfmm  21382  lsslindf  21385  islindf4  21393  opsrtoslem2  21617  cply1coe0  21823  cply1coe0bi  21824  mdetunilem7  22120  mdetunilem8  22121  mdetunilem9  22122  maducoeval2  22142  pmatcollpw3fi1lem1  22288  fvmptnn04ifa  22352  fvmptnn04ifc  22354  fvmptnn04ifd  22355  chfacffsupp  22358  chfacfscmul0  22360  chfacfpmmul0  22364  elcls  22577  maxlp  22651  perfi  22659  ordtbaslem  22692  ordtval  22693  ordtbas2  22695  ordtopn1  22698  ordtopn2  22699  ordtcnv  22705  ordtrest  22706  ordtrest2lem  22707  ordtrest2  22708  pnfnei  22724  mnfnei  22725  isreg2  22881  ordthauslem  22887  cmpfi  22912  cmpfii  22913  bwth  22914  nconnsubb  22927  hausdiag  23149  txkgen  23156  kqdisj  23236  ordthmeolem  23305  fbfinnfr  23345  trfbas  23348  fbunfip  23373  fbasrn  23388  trfil3  23392  ufileu  23423  fin1aufil  23436  hausflim  23485  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  ptcmplem2  23557  ptcmplem3  23558  stdbdbl  24026  iccntr  24337  reconnlem2  24343  iccpnfcnv  24460  xrhmeo  24462  lebnumlem1  24477  lebnumlem2  24478  lebnumlem3  24479  bcthlem4  24844  minveclem3b  24945  ivthlem2  24969  ivthlem3  24970  mbfmax  25166  mbfposr  25169  i1fd  25198  mbfi1fseqlem4  25236  itg2splitlem  25266  itg2monolem1  25268  itg2cnlem1  25279  dvne0  25528  lhop1lem  25530  deg1nn0clb  25608  dgrle  25757  coemulhi  25768  aaliou3lem9  25863  cos11  26042  logleb  26111  argrege0  26119  logdivle  26130  ellogdm  26147  cxple  26203  cxplt2  26206  cxple3  26209  isosctrlem1  26323  atandm  26381  atans2  26436  atantayl2  26443  eldmgm  26526  ftalem7  26583  isppw2  26619  musum  26695  dchrsum2  26771  bposlem1  26787  lgsmod  26826  lgsdir2lem2  26829  lgsdir2  26833  lgsne0  26838  lgsprme0  26842  gausslemma2dlem4  26872  lgsquadlem1  26883  2lgslem3  26907  2lgsoddprm  26919  2sq2  26936  addsqrexnreu  26945  rpvmasumlem  26990  padicabv  27133  ostth3  27141  ostth  27142  noextenddif  27171  nodenselem4  27190  nodenselem5  27191  nodenselem7  27193  nolt02o  27198  nogt01o  27199  noresle  27200  nosupprefixmo  27203  noinfprefixmo  27204  nosupcbv  27205  nosupdm  27207  nosupfv  27209  nosupres  27210  nosupbnd1lem1  27211  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd1  27217  nosupbnd2lem1  27218  nosupbnd2  27219  noinfcbv  27220  noinfdm  27222  noinffv  27224  noinfres  27225  noinfbnd1lem1  27226  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd1  27232  noinfbnd2lem1  27233  noinfbnd2  27234  slenlt  27255  sltne  27273  nocvxminlem  27279  slerec  27321  cuteq1  27335  newbday  27397  sltlpss  27402  cofcutr  27413  lrrecfr  27429  addsval  27448  sltadd2  27477  sleneg  27523  slesubsubbd  27556  slesubsub2bd  27557  slesubsub3bd  27558  sltmul2  27626  slemul2d  27629  slemul1d  27630  istrkgld  27741  axtgupdim2  27753  tglowdim2l  27932  axlowdimlem16  28246  axlowdim2  28249  axlowdim  28250  numedglnl  28435  usgredg2v  28515  lfuhgr1v0e  28542  cusgrfi  28746  vtxd0nedgb  28776  vtxduhgr0edgnel  28782  1loopgrnb0  28790  1hevtxdg0  28793  vtxdgoddnumeven  28841  wlkp1lem1  28961  wlkp1lem2  28962  wlkp1lem5  28965  crctcsh  29109  clwlkclwwlklem2a4  29281  eupth2eucrct  29501  eupth2lem3lem3  29514  eupth2lem3lem4  29515  eupth2lem3lem6  29517  eupth2lem3lem7  29518  eupth2lems  29522  eupth2  29523  konigsberglem4  29539  nfrgr2v  29556  frgrwopreglem3  29598  fusgr2wsp2nb  29618  frgrreggt1  29677  friendshipgt3  29682  lpni  29764  nmobndseqi  30063  minvecolem5  30165  chpsscon3  30787  chnle  30798  nonbooli  30935  pjnel  31010  specval  31182  nmcfnlbi  31336  stri  31541  hstri  31549  cvbr  31566  cvcon3  31568  chcv1  31639  cvexchlem  31652  chrelat2  31654  nelun  31782  elpreq  31798  nelpr  31799  ifeqeqx  31805  nfpconfp  31887  suppiniseg  31939  isoun  31954  suppss3  31980  xrge0infss  32004  infxrge0gelb  32010  eliccelico  32019  elicoelioo  32020  nndiffz1  32028  hashgt1  32051  nn0min  32057  toslublem  32173  tosglblem  32175  pmtrcnel  32281  cycpmco2  32323  isarchi2  32362  archiabl  32375  0nellinds  32514  lindssn  32525  lindfpropd  32529  mxidlirred  32619  ssmxidl  32621  lbslsat  32732  lindsunlem  32740  ordtcnvNEW  32931  ordtrestNEW  32932  ordtrest2NEWlem  32933  ordtrest2NEW  32934  ordtconnlem1  32935  xrge0iifcnv  32944  esumpcvgval  33107  esum2d  33122  ddemeas  33265  omssubadd  33330  oddpwdc  33384  eulerpartlems  33390  eulerpartlemf  33400  eulerpartlemt  33401  eulerpartlemr  33404  eulerpartlemgvv  33406  eulerpartlemn  33411  ballotlemfc0  33522  ballotlemfcc  33523  ballotlem4  33528  ballotlemimin  33535  ballotlem7  33565  plymulx  33590  signsply0  33593  reprinfz1  33665  reprpmtf1o  33669  reprdifc  33670  hgt750lema  33700  hgt750leme  33701  istrkg2d  33709  bnj23  33760  bnj1185  33835  bnj1228  34053  bnj1388  34075  bnj1417  34083  nummin  34125  revwlk  34146  isacycgr  34167  acycgr0v  34170  prclisacycgr  34173  erdszelem10  34222  satf0n0  34400  fmlaomn0  34412  fmlasucdisj  34421  satfv1fvfmla1  34445  satefvfmla1  34447  ismfs  34571  mvtinf  34577  untelirr  34708  untsucf  34710  untangtr  34714  dfon2lem3  34788  dfon2lem4  34789  dfon2lem7  34792  dfon2lem9  34794  distel  34806  funpartfv  34948  dfrdg4  34954  nn0prpwlem  35255  nn0prpw  35256  limsucncmpi  35378  limsucncmp  35379  ordcmp  35380  unblimceq0  35431  unbdqndv1  35432  bj-hbntbi  35630  bj-equsexvwd  35707  bj-cbvexdv  35726  bj-ru0  35871  bj-nuliota  35986  topdifinffinlem  36276  topdifinffin  36277  icorempo  36280  relowlpssretop  36293  finxpreclem2  36319  finxpreclem6  36325  wl-issetft  36492  wl-ax11-lem8  36502  leceifl  36525  lindsadd  36529  lindsenlbs  36531  matunitlindflem1  36532  poimirlem16  36552  poimirlem17  36553  poimirlem18  36554  poimirlem19  36555  poimirlem21  36557  poimirlem23  36559  poimirlem26  36562  poimirlem27  36563  poimirlem28  36564  poimirlem31  36567  poimir  36569  mblfinlem2  36574  mblfinlem3  36575  ismblfin  36577  cnambfre  36584  itg2addnclem  36587  itg2addnclem2  36588  iblabsnclem  36599  ftc1anclem1  36609  areacirc  36629  heibor1lem  36725  heiborlem1  36727  heiborlem6  36732  heiborlem8  36734  heiborlem10  36736  smprngopr  36968  ecin0  37269  ax12inda  37866  riotaclbgBAD  37872  lcvfbr  37938  lcvbr  37939  lsatcv0  37949  l1cvpat  37972  opltcon3b  38122  cvrfval  38186  cvrval  38187  cvrnbtwn  38189  cvrval2  38192  cvrnbtwn2  38193  cvrnbtwn3  38194  cvrcon3b  38195  cvrnbtwn4  38197  atnlt  38231  iscvlat  38241  cvlexch1  38246  hlsuprexch  38300  hlrelat5N  38320  hlrelat2  38322  cvrval5  38334  3dimlem1  38377  3dim1lem5  38385  3dim2  38387  3dim3  38388  llnnlt  38442  islpln5  38454  lplni2  38456  lvolex3N  38457  lplnnle2at  38460  islpln2a  38467  lplnribN  38470  lplnexllnN  38483  lplnnlt  38484  lvoli3  38496  islvol5  38498  lvoli2  38500  lvolnle3at  38501  islvol2aN  38511  4atlem11  38528  lvolnltN  38537  dalawlem15  38804  4atexlemex2  38990  4atex  38995  4atex2-0aOLDN  38997  4atex2-0cOLDN  38999  lautcvr  39011  ltrnfset  39036  ltrnset  39037  ltrnu  39040  trlfset  39079  trlset  39080  trlval2  39082  cdlemd6  39122  cdleme0nex  39209  cdleme18d  39214  cdleme25b  39273  cdleme25cv  39277  cdleme29b  39294  cdleme31fv  39309  cdleme31fv2  39312  cdlemefrs29bpre0  39315  cdlemefr32sn2aw  39323  cdlemefr29bpre0N  39325  cdlemefr29clN  39326  cdlemefr32fvaN  39328  cdlemefr32fva1  39329  cdlemefs32sn1aw  39333  cdleme32fva  39356  cdleme32fvaw  39358  cdleme40v  39388  cdleme42b  39397  cdleme46f2g2  39412  cdleme46f2g1  39413  cdleme48gfv  39456  cdlemg1fvawlemN  39492  cdlemg1cex  39507  cdlemg6d  39540  cdlemm10N  40037  dicffval  40093  dicfval  40094  dicval  40095  dicfnN  40102  dicvalrelN  40104  dihffval  40149  dihfval  40150  dihlsscpre  40153  dvh4dimat  40357  dvh3dimatN  40358  dvh4dimlem  40362  dvh3dim  40365  dvh4dimN  40366  dvh3dim2  40367  dvh3dim3N  40368  mapdcv  40579  mapdh9aOLDN  40709  hdmapfval  40746  hdmapval  40747  hdmapval2  40751  hdmap11lem2  40761  dvrelog2b  40979  aks4d1p4  40992  aks4d1p5  40993  aks4d1p7  40996  aks4d1p8d2  40998  aks4d1p8  41000  aks4d1  41002  aks6d1c2p2  41005  metakunt27  41059  metakunt28  41060  metakunt29  41061  oexpreposd  41260  exp11nnd  41263  flt4lem7  41449  nna4b4nsq  41450  ellz1  41553  rencldnfilem  41606  jm2.22  41782  jm2.23  41783  wepwsolem  41832  fnwe2lem2  41841  aomclem8  41851  unxpwdom3  41885  onsupmaxb  42036  onexlimgt  42040  onsupeqnmax  42044  onov0suclim  42072  oaordnr  42094  omnord1  42103  oenord1  42114  oaomoencom  42115  oenass  42117  cantnfresb  42122  tfsnfin  42150  ralopabb  42210  nlimsuc  42240  ifpbi12  42287  dfsucon  42322  sqrtcvallem1  42430  ss2iundf  42458  frege124d  42560  clsk3nimkb  42839  clsk1indlem1  42844  clsk1independent  42845  ntrneineine1lem  42883  ntrneicls11  42889  clsneiel1  42907  clsneiel2  42908  neicvgel1  42918  neicvgel2  42919  radcnvrat  43121  rusbcALT  43246  en3lpVD  43654  eliin2f  43841  nssd  43842  wessf1ornlem  43930  rexanuz2nf  44251  limsupre2lem  44488  icccncfext  44651  stoweidlem14  44778  stoweidlem34  44798  stoweidlem59  44823  etransclem24  45022  nnfoctbdjlem  45219  nnfoctbdj  45220  hspmbllem2  45391  nsssmfmbflem  45542  fsetsnprcnex  45813  eu2ndop1stv  45881  afvfv0bi  45908  afvco2  45932  ndmaovg  45940  ndfatafv2nrn  45977  afv2ndefb  45980  afv2fv0  46021  nelbr  46030  otiunsndisjX  46035  fun2dmnopgexmpl  46040  ltnltne  46055  readdcnnred  46059  resubcnnred  46060  recnmulnred  46061  cndivrenred  46062  ichnreuop  46188  fmtnoinf  46252  odz2prm2pw  46279  prmdvdsfmtnof1lem2  46301  lighneallem3  46323  lighneallem4  46326  requad1  46338  isodd3  46368  bits0ALTV  46395  nfermltl8rev  46458  nfermltl2rev  46459  nfermltlrev  46460  lidldomnnring  46876  zrninitoringc  47017  ztprmneprm  47071  lindepsnlininds  47181  islindeps  47182  lindslinindsimp2lem5  47191  lindslinindsimp2  47192  difmodm1lt  47256  line2ylem  47485  line2xlem  47487  map0cor  47569  elsetrecslem  47792