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  27320  cuteq1  27334  newbday  27396  sltlpss  27401  cofcutr  27411  lrrecfr  27427  addsval  27446  sltadd2  27474  sleneg  27520  slesubsubbd  27553  slesubsub2bd  27554  slesubsub3bd  27555  sltmul2  27623  slemul2d  27626  slemul1d  27627  istrkgld  27710  axtgupdim2  27722  tglowdim2l  27901  axlowdimlem16  28215  axlowdim2  28218  axlowdim  28219  numedglnl  28404  usgredg2v  28484  lfuhgr1v0e  28511  cusgrfi  28715  vtxd0nedgb  28745  vtxduhgr0edgnel  28751  1loopgrnb0  28759  1hevtxdg0  28762  vtxdgoddnumeven  28810  wlkp1lem1  28930  wlkp1lem2  28931  wlkp1lem5  28934  crctcsh  29078  clwlkclwwlklem2a4  29250  eupth2eucrct  29470  eupth2lem3lem3  29483  eupth2lem3lem4  29484  eupth2lem3lem6  29486  eupth2lem3lem7  29487  eupth2lems  29491  eupth2  29492  konigsberglem4  29508  nfrgr2v  29525  frgrwopreglem3  29567  fusgr2wsp2nb  29587  frgrreggt1  29646  friendshipgt3  29651  lpni  29733  nmobndseqi  30032  minvecolem5  30134  chpsscon3  30756  chnle  30767  nonbooli  30904  pjnel  30979  specval  31151  nmcfnlbi  31305  stri  31510  hstri  31518  cvbr  31535  cvcon3  31537  chcv1  31608  cvexchlem  31621  chrelat2  31623  nelun  31751  elpreq  31767  nelpr  31768  ifeqeqx  31774  nfpconfp  31856  suppiniseg  31908  isoun  31923  suppss3  31949  xrge0infss  31973  infxrge0gelb  31979  eliccelico  31988  elicoelioo  31989  nndiffz1  31997  hashgt1  32020  nn0min  32026  toslublem  32142  tosglblem  32144  pmtrcnel  32250  cycpmco2  32292  isarchi2  32331  archiabl  32344  0nellinds  32483  lindssn  32494  lindfpropd  32498  mxidlirred  32588  ssmxidl  32590  lbslsat  32701  lindsunlem  32709  ordtcnvNEW  32900  ordtrestNEW  32901  ordtrest2NEWlem  32902  ordtrest2NEW  32903  ordtconnlem1  32904  xrge0iifcnv  32913  esumpcvgval  33076  esum2d  33091  ddemeas  33234  omssubadd  33299  oddpwdc  33353  eulerpartlems  33359  eulerpartlemf  33369  eulerpartlemt  33370  eulerpartlemr  33373  eulerpartlemgvv  33375  eulerpartlemn  33380  ballotlemfc0  33491  ballotlemfcc  33492  ballotlem4  33497  ballotlemimin  33504  ballotlem7  33534  plymulx  33559  signsply0  33562  reprinfz1  33634  reprpmtf1o  33638  reprdifc  33639  hgt750lema  33669  hgt750leme  33670  istrkg2d  33678  bnj23  33729  bnj1185  33804  bnj1228  34022  bnj1388  34044  bnj1417  34052  nummin  34094  revwlk  34115  isacycgr  34136  acycgr0v  34139  prclisacycgr  34142  erdszelem10  34191  satf0n0  34369  fmlaomn0  34381  fmlasucdisj  34390  satfv1fvfmla1  34414  satefvfmla1  34416  ismfs  34540  mvtinf  34546  untelirr  34677  untsucf  34679  untangtr  34683  dfon2lem3  34757  dfon2lem4  34758  dfon2lem7  34761  dfon2lem9  34763  distel  34775  funpartfv  34917  dfrdg4  34923  nn0prpwlem  35207  nn0prpw  35208  limsucncmpi  35330  limsucncmp  35331  ordcmp  35332  unblimceq0  35383  unbdqndv1  35384  bj-hbntbi  35582  bj-equsexvwd  35659  bj-cbvexdv  35678  bj-ru0  35823  bj-nuliota  35938  topdifinffinlem  36228  topdifinffin  36229  icorempo  36232  relowlpssretop  36245  finxpreclem2  36271  finxpreclem6  36277  wl-issetft  36444  wl-ax11-lem8  36454  leceifl  36477  lindsadd  36481  lindsenlbs  36483  matunitlindflem1  36484  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem21  36509  poimirlem23  36511  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem31  36519  poimir  36521  mblfinlem2  36526  mblfinlem3  36527  ismblfin  36529  cnambfre  36536  itg2addnclem  36539  itg2addnclem2  36540  iblabsnclem  36551  ftc1anclem1  36561  areacirc  36581  heibor1lem  36677  heiborlem1  36679  heiborlem6  36684  heiborlem8  36686  heiborlem10  36688  smprngopr  36920  ecin0  37221  ax12inda  37818  riotaclbgBAD  37824  lcvfbr  37890  lcvbr  37891  lsatcv0  37901  l1cvpat  37924  opltcon3b  38074  cvrfval  38138  cvrval  38139  cvrnbtwn  38141  cvrval2  38144  cvrnbtwn2  38145  cvrnbtwn3  38146  cvrcon3b  38147  cvrnbtwn4  38149  atnlt  38183  iscvlat  38193  cvlexch1  38198  hlsuprexch  38252  hlrelat5N  38272  hlrelat2  38274  cvrval5  38286  3dimlem1  38329  3dim1lem5  38337  3dim2  38339  3dim3  38340  llnnlt  38394  islpln5  38406  lplni2  38408  lvolex3N  38409  lplnnle2at  38412  islpln2a  38419  lplnribN  38422  lplnexllnN  38435  lplnnlt  38436  lvoli3  38448  islvol5  38450  lvoli2  38452  lvolnle3at  38453  islvol2aN  38463  4atlem11  38480  lvolnltN  38489  dalawlem15  38756  4atexlemex2  38942  4atex  38947  4atex2-0aOLDN  38949  4atex2-0cOLDN  38951  lautcvr  38963  ltrnfset  38988  ltrnset  38989  ltrnu  38992  trlfset  39031  trlset  39032  trlval2  39034  cdlemd6  39074  cdleme0nex  39161  cdleme18d  39166  cdleme25b  39225  cdleme25cv  39229  cdleme29b  39246  cdleme31fv  39261  cdleme31fv2  39264  cdlemefrs29bpre0  39267  cdlemefr32sn2aw  39275  cdlemefr29bpre0N  39277  cdlemefr29clN  39278  cdlemefr32fvaN  39280  cdlemefr32fva1  39281  cdlemefs32sn1aw  39285  cdleme32fva  39308  cdleme32fvaw  39310  cdleme40v  39340  cdleme42b  39349  cdleme46f2g2  39364  cdleme46f2g1  39365  cdleme48gfv  39408  cdlemg1fvawlemN  39444  cdlemg1cex  39459  cdlemg6d  39492  cdlemm10N  39989  dicffval  40045  dicfval  40046  dicval  40047  dicfnN  40054  dicvalrelN  40056  dihffval  40101  dihfval  40102  dihlsscpre  40105  dvh4dimat  40309  dvh3dimatN  40310  dvh4dimlem  40314  dvh3dim  40317  dvh4dimN  40318  dvh3dim2  40319  dvh3dim3N  40320  mapdcv  40531  mapdh9aOLDN  40661  hdmapfval  40698  hdmapval  40699  hdmapval2  40703  hdmap11lem2  40713  dvrelog2b  40931  aks4d1p4  40944  aks4d1p5  40945  aks4d1p7  40948  aks4d1p8d2  40950  aks4d1p8  40952  aks4d1  40954  aks6d1c2p2  40957  metakunt27  41011  metakunt28  41012  metakunt29  41013  oexpreposd  41212  exp11nnd  41215  flt4lem7  41401  nna4b4nsq  41402  ellz1  41505  rencldnfilem  41558  jm2.22  41734  jm2.23  41735  wepwsolem  41784  fnwe2lem2  41793  aomclem8  41803  unxpwdom3  41837  onsupmaxb  41988  onexlimgt  41992  onsupeqnmax  41996  onov0suclim  42024  oaordnr  42046  omnord1  42055  oenord1  42066  oaomoencom  42067  oenass  42069  cantnfresb  42074  tfsnfin  42102  ralopabb  42162  nlimsuc  42192  ifpbi12  42239  dfsucon  42274  sqrtcvallem1  42382  ss2iundf  42410  frege124d  42512  clsk3nimkb  42791  clsk1indlem1  42796  clsk1independent  42797  ntrneineine1lem  42835  ntrneicls11  42841  clsneiel1  42859  clsneiel2  42860  neicvgel1  42870  neicvgel2  42871  radcnvrat  43073  rusbcALT  43198  en3lpVD  43606  eliin2f  43793  nssd  43794  wessf1ornlem  43882  rexanuz2nf  44203  limsupre2lem  44440  icccncfext  44603  stoweidlem14  44730  stoweidlem34  44750  stoweidlem59  44775  etransclem24  44974  nnfoctbdjlem  45171  nnfoctbdj  45172  hspmbllem2  45343  nsssmfmbflem  45494  fsetsnprcnex  45765  eu2ndop1stv  45833  afvfv0bi  45860  afvco2  45884  ndmaovg  45892  ndfatafv2nrn  45929  afv2ndefb  45932  afv2fv0  45973  nelbr  45982  otiunsndisjX  45987  fun2dmnopgexmpl  45992  ltnltne  46007  readdcnnred  46011  resubcnnred  46012  recnmulnred  46013  cndivrenred  46014  ichnreuop  46140  fmtnoinf  46204  odz2prm2pw  46231  prmdvdsfmtnof1lem2  46253  lighneallem3  46275  lighneallem4  46278  requad1  46290  isodd3  46320  bits0ALTV  46347  nfermltl8rev  46410  nfermltl2rev  46411  nfermltlrev  46412  lidldomnnring  46828  zrninitoringc  46969  ztprmneprm  47023  lindepsnlininds  47133  islindeps  47134  lindslinindsimp2lem5  47143  lindslinindsimp2  47144  difmodm1lt  47208  line2ylem  47437  line2xlem  47439  map0cor  47521  elsetrecslem  47744