Theorem notbid 317

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 314	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
3		notnotb 314	. . 3 ⊢ (𝜒 ↔ ¬ ¬ 𝜒)
4	1, 2, 3	3bitr3g 312	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
5	4	con4bid 316	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  318  annotanannot  833  con3ALT  1082  xorbi12d  1519  equsexvw  2001  cbvexvw  2033  cbvexdvaw  2035  hbe1w  2044  19.8aw  2046  exexw  2047  cbvexv1  2333  cbvex2v  2335  drex1v  2363  cbvex  2393  cbvex2  2406  drex1  2435  eujustALT  2561  necon3abid  2967  neleq12d  3041  rexbiOLD  3095  cbvrexdva  3228  cbvrexfw  3293  rexeqbidvvOLD  3322  cbvrexdva2  3333  cbvrexf  3345  issetft  3477  cgsex4gOLD  3512  ceqsex  3514  ceqsexv  3516  gencbval  3529  spcegf  3578  spc2gv  3586  spc2d  3588  spc3gv  3590  ceqsralbv  3642  cdeqnot  3762  rru  3773  ru  3774  ruOLD  3775  sbcng  3827  sbcrext  3866  cbvrexcsf  3938  difjust  3949  eldif  3957  dfpss3  4085  dfdif3  4113  difeq2  4115  ab0OLD  4380  disjne  4459  pssdifcom1  4494  eldifpr  4665  rexsng  4683  elpwunsn  4692  eldiftp  4695  rexprg  4705  preqsnd  4865  disjxun  5151  nalset  5318  dtruALT2  5374  dtruALT  5392  rexxfrd  5413  rexxfr2d  5415  rexxfrd2  5417  rexxfr  5420  dtruOLD  5447  opthneg  5487  snopeqop  5512  otiunsndisj  5526  poeq1  5597  pocl  5601  poclOLD  5602  swopo  5605  sotric  5622  sotrieq  5623  isso2i  5629  somo  5631  freq1  5652  frirr  5659  fr2nr  5660  frminex  5662  tz7.2  5666  wereu2  5679  poinxp  5762  frinxp  5764  posn  5767  frsn  5769  rexiunxp  5847  rexxpf  5854  intirr  6130  poirr2  6136  cnvpo  6298  dfpo2  6307  predpoirr  6346  predfrirr  6347  frpomin  6353  nordeq  6395  ordtri1  6409  ordtri3  6412  fvmpti  7008  fndmdif  7055  rexrnmptw  7109  rexrnmpt  7111  2f1fvneq  7275  f1imapss  7281  cbvexfo  7304  nf1const  7317  soisoi  7340  isopolem  7357  weniso  7366  imaeqsalv  7376  canth  7377  riotaclb  7422  rexrnmpo  7566  ndmovg  7609  sorpssuni  7743  sorpssint  7744  fr3nr  7780  dfwe2  7782  ordsucsssuc  7832  nlimsucg  7852  orduninsuc  7853  dfom2  7878  ssnlim  7896  f1oweALT  7986  frxp  8140  poxp  8142  frxp2  8158  frxp3  8165  xpord3inddlem  8168  soseq  8173  suppofssd  8218  suppcoss  8222  wfrlem10OLD  8348  smoword  8396  tz7.48lem  8471  oacan  8578  oaword  8579  omlimcl  8608  omeulem1  8612  nnaword  8657  nnmword  8663  nneob  8686  naddss1  8719  brdifun  8764  swoer  8765  undifixp  8963  boxcutc  8970  2dom  9066  php  9244  phpeqd  9249  nndomog  9250  phpOLD  9256  nndomogOLD  9260  onomeneq  9262  nnsdomo  9268  unxpdomlem2  9285  frfi  9322  unfilem1  9344  supeq3  9492  supeq123d  9493  supmo  9495  eqsup  9499  supub  9502  sup0  9509  suppr  9514  supisolem  9516  supisoex  9517  eqinf  9527  infval  9529  infmo  9538  infpr  9546  infempty  9550  oieq1  9555  ordtypecbv  9560  ordtypelem7  9567  wemapsolem  9593  canthwdom  9622  zfregcl  9637  elirrv  9639  elirr  9640  noinfep  9703  cantnfp1lem3  9723  ttrcltr  9759  rankr1clem  9863  carden2b  10010  domtri2  10032  alephord3  10121  alephdom2  10130  alephval3  10153  dfac9  10179  kmlem2  10194  kmlem4  10196  isfin4  10340  isfin7  10344  fin23lem11  10360  isf32lem5  10400  isf34lem4  10420  fin1a2lem6  10448  fin1a2lem7  10449  fin1a2lem12  10454  itunisuc  10462  ac6n  10528  zorn2g  10546  zornn0g  10548  ttukeylem7  10558  axpowndlem3  10642  axpowndlem4  10643  axregnd  10647  elgch  10665  engch  10671  fpwwe2lem12  10685  fpwwe2  10686  pwfseqlem1  10701  pwfseqlem3  10703  hargch  10716  addnidpi  10944  pinq  10970  nqereu  10972  ltsonq  11012  prlem934  11076  ltexprlem7  11085  addcanpr  11089  prlem936  11090  reclem2pr  11091  reclem3pr  11092  supexpr  11097  ltsosr  11137  supsrlem  11154  axpre-lttri  11208  axpre-sup  11212  xrlenlt  11329  axlttri  11335  axsup  11339  ltne  11361  dedekind  11427  readdcan  11438  leadd1  11732  ltsub1  11760  ltsub2  11761  leord1  11791  lediv1  12131  lemuldiv  12146  lerec  12149  le2msq  12166  infm3  12225  suprnub  12231  infregelb  12250  avgle1  12504  avgle2  12505  znnnlt1  12641  indstr  12952  zsupss  12973  uzsupss  12976  rpneg  13060  xralrple  13238  xleneg  13251  xltadd1  13289  xposdif  13295  xmulneg1  13302  xltmul1  13325  xrsupexmnf  13338  xrinfmexpnf  13339  xrsupsslem  13340  xrinfmsslem  13341  xrub  13345  supxrleub  13359  infxrgelb  13368  difreicc  13515  nn0disj  13671  nelfzo  13691  elfznelfzo  13792  fvinim0ffz  13806  injresinjlem  13807  ssnn0fi  14005  leexp2  14190  exp11nnd  14278  hashbnd  14353  hasheni  14365  hashfundm  14459  hashbc  14470  wrdsymb0  14557  swrdnd  14662  swrdnd2  14663  pfxnd0  14696  repswswrd  14792  repswccat  14794  cshwidxmod  14811  cnpart  15245  sqrtlt  15266  limsuplt  15481  rlimrege0  15581  isercoll  15672  efle  16120  odd2np1  16343  sumodd  16390  divalglem7  16401  ndvdsadd  16412  fldivndvdslt  16416  bitsfval  16423  bitsval  16424  bits0  16428  bitsp1  16431  bitsmod  16436  bitscmp  16438  bitsinv1lem  16441  sadadd2lem2  16450  saddisjlem  16464  bitsshft  16475  gcdneg  16522  algcvgblem  16578  lcmneg  16604  isprm3  16684  dvdsnprmd  16691  isprm5  16708  rpexp  16724  phiprmpw  16778  m1dvdsndvds  16800  pythagtrip  16836  pcgcd1  16879  prmpwdvds  16906  prmreclem2  16919  prmreclem3  16920  prmreclem5  16922  prmreclem6  16923  vdwlem6  16988  vdwnnlem2  16998  vdwnnlem3  16999  vdwnn  17000  prmlem0  17108  prmlem1a  17109  divsfval  17562  mrisval  17643  ismri  17644  ismri2dad  17650  cidpropd  17723  cat1lem  18118  plttr  18367  joinval  18402  meetval  18416  acsfiindd  18578  isnsgrp  18716  smndex1n0mnd  18902  mgm2nsgrplem2  18909  sgrp2nmndlem3  18915  symgpssefmnd  19393  symgfix2  19414  pmtrdifellem4  19477  psgnunilem1  19491  psgnunilem5  19492  psgnunilem2  19493  psgnunilem3  19494  pmtrsn  19517  sylow1lem3  19598  sylow2alem2  19616  efgsfo  19737  ablfac1eulem  20072  ablfac1eu  20073  pgpfac1lem1  20074  pgpfac1lem5  20079  nzrunit  20506  zrninitoringc  20654  islbs  21054  lbsind  21058  lbspss  21060  lbspropd  21077  lspsnne1  21098  islbs2  21135  lbsacsbs  21137  lbsextlem1  21139  lbsextlem3  21141  lbsextlem4  21142  lbsextg  21143  frlmlbs  21795  islindf  21810  islinds2  21811  islindf2  21812  lindfind  21814  lindsind  21815  lindfrn  21819  lindfmm  21825  lsslindf  21828  islindf4  21836  opsrtoslem2  22069  psdmul  22160  cply1coe0  22292  cply1coe0bi  22293  mdetunilem7  22611  mdetunilem8  22612  mdetunilem9  22613  maducoeval2  22633  pmatcollpw3fi1lem1  22779  fvmptnn04ifa  22843  fvmptnn04ifc  22845  fvmptnn04ifd  22846  chfacffsupp  22849  chfacfscmul0  22851  chfacfpmmul0  22855  elcls  23068  maxlp  23142  perfi  23150  ordtbaslem  23183  ordtval  23184  ordtbas2  23186  ordtopn1  23189  ordtopn2  23190  ordtcnv  23196  ordtrest  23197  ordtrest2lem  23198  ordtrest2  23199  pnfnei  23215  mnfnei  23216  isreg2  23372  ordthauslem  23378  cmpfi  23403  cmpfii  23404  bwth  23405  nconnsubb  23418  hausdiag  23640  txkgen  23647  kqdisj  23727  ordthmeolem  23796  fbfinnfr  23836  trfbas  23839  fbunfip  23864  fbasrn  23879  trfil3  23883  ufileu  23914  fin1aufil  23927  hausflim  23976  alexsubALTlem2  24043  alexsubALTlem3  24044  alexsubALTlem4  24045  ptcmplem2  24048  ptcmplem3  24049  stdbdbl  24517  iccntr  24828  reconnlem2  24834  iccpnfcnv  24960  xrhmeo  24962  lebnumlem1  24978  lebnumlem2  24979  lebnumlem3  24980  bcthlem4  25346  minveclem3b  25447  ivthlem2  25472  ivthlem3  25473  mbfmax  25669  mbfposr  25672  i1fd  25701  mbfi1fseqlem4  25739  itg2splitlem  25769  itg2monolem1  25771  itg2cnlem1  25782  dvne0  26035  lhop1lem  26037  deg1nn0clb  26117  dgrle  26270  coemulhi  26281  aaliou3lem9  26378  cos11  26560  logleb  26630  argrege0  26638  logdivle  26649  ellogdm  26666  cxple  26722  cxplt2  26725  cxple3  26728  isosctrlem1  26846  atandm  26904  atans2  26959  atantayl2  26966  eldmgm  27050  ftalem7  27107  isppw2  27143  musum  27219  dchrsum2  27297  bposlem1  27313  lgsmod  27352  lgsdir2lem2  27355  lgsdir2  27359  lgsne0  27364  lgsprme0  27368  gausslemma2dlem4  27398  lgsquadlem1  27409  2lgslem3  27433  2lgsoddprm  27445  2sq2  27462  addsqrexnreu  27471  rpvmasumlem  27516  padicabv  27659  ostth3  27667  ostth  27668  noextenddif  27698  nodenselem4  27717  nodenselem5  27718  nodenselem7  27720  nolt02o  27725  nogt01o  27726  noresle  27727  nosupprefixmo  27730  noinfprefixmo  27731  nosupcbv  27732  nosupdm  27734  nosupfv  27736  nosupres  27737  nosupbnd1lem1  27738  nosupbnd1lem3  27740  nosupbnd1lem5  27742  nosupbnd1  27744  nosupbnd2lem1  27745  nosupbnd2  27746  noinfcbv  27747  noinfdm  27749  noinffv  27751  noinfres  27752  noinfbnd1lem1  27753  noinfbnd1lem3  27755  noinfbnd1lem5  27757  noinfbnd1  27759  noinfbnd2lem1  27760  noinfbnd2  27761  slenlt  27782  sltne  27800  nocvxminlem  27807  slerec  27849  cuteq1  27863  newbday  27925  sltlpss  27930  cofcutr  27941  lrrecfr  27957  addsval  27976  sltadd2  28005  sleneg  28055  slesubsubbd  28093  slesubsub2bd  28094  slesubsub3bd  28095  slesubaddd  28100  sltmul2  28172  slemul2d  28175  slemul1d  28176  istrkgld  28386  axtgupdim2  28398  tglowdim2l  28577  axlowdimlem16  28891  axlowdim2  28894  axlowdim  28895  numedglnl  29080  usgredg2v  29163  lfuhgr1v0e  29190  cusgrfi  29395  vtxd0nedgb  29425  vtxduhgr0edgnel  29431  1loopgrnb0  29439  1hevtxdg0  29442  vtxdgoddnumeven  29490  wlkp1lem1  29610  wlkp1lem2  29611  wlkp1lem5  29614  crctcsh  29758  clwlkclwwlklem2a4  29930  eupth2eucrct  30150  eupth2lem3lem3  30163  eupth2lem3lem4  30164  eupth2lem3lem6  30166  eupth2lem3lem7  30167  eupth2lems  30171  eupth2  30172  konigsberglem4  30188  nfrgr2v  30205  frgrwopreglem3  30247  fusgr2wsp2nb  30267  frgrreggt1  30326  friendshipgt3  30331  lpni  30413  nmobndseqi  30712  minvecolem5  30814  chpsscon3  31436  chnle  31447  nonbooli  31584  pjnel  31659  specval  31831  nmcfnlbi  31985  stri  32190  hstri  32198  cvbr  32215  cvcon3  32217  chcv1  32288  cvexchlem  32301  chrelat2  32303  nelun  32439  elpreq  32456  nelpr  32457  ifeqeqx  32463  nfpconfp  32549  suppiniseg  32598  isoun  32613  suppss3  32638  xrge0infss  32664  infxrge0gelb  32670  eliccelico  32679  elicoelioo  32680  nndiffz1  32688  hashgt1  32712  expgt0b  32717  nn0min  32721  ccatws1f1o  32815  toslublem  32842  tosglblem  32844  pmtrcnel  32967  cycpmco2  33011  isarchi2  33050  archiabl  33063  0nellinds  33245  lindssn  33253  lindfpropd  33257  ssdifidlprm  33333  mxidlirred  33347  ssmxidl  33349  lbslsat  33511  lindsunlem  33519  rtelextdg2lem  33604  ordtcnvNEW  33735  ordtrestNEW  33736  ordtrest2NEWlem  33737  ordtrest2NEW  33738  ordtconnlem1  33739  xrge0iifcnv  33748  esumpcvgval  33911  esum2d  33926  ddemeas  34069  omssubadd  34134  oddpwdc  34188  eulerpartlems  34194  eulerpartlemf  34204  eulerpartlemt  34205  eulerpartlemr  34208  eulerpartlemgvv  34210  eulerpartlemn  34215  ballotlemfc0  34326  ballotlemfcc  34327  ballotlem4  34332  ballotlemimin  34339  ballotlem7  34369  plymulx  34394  signsply0  34397  reprinfz1  34468  reprpmtf1o  34472  reprdifc  34473  hgt750lema  34503  hgt750leme  34504  istrkg2d  34512  bnj23  34563  bnj1185  34638  bnj1228  34856  bnj1388  34878  bnj1417  34886  nummin  34928  revwlk  34952  isacycgr  34973  acycgr0v  34976  prclisacycgr  34979  erdszelem10  35028  satf0n0  35206  fmlaomn0  35218  fmlasucdisj  35227  satfv1fvfmla1  35251  satefvfmla1  35253  ismfs  35377  mvtinf  35383  untelirr  35530  untsucf  35532  untangtr  35536  dfon2lem3  35609  dfon2lem4  35610  dfon2lem7  35613  dfon2lem9  35615  distel  35627  funpartfv  35769  dfrdg4  35775  nn0prpwlem  36034  nn0prpw  36035  limsucncmpi  36157  limsucncmp  36158  ordcmp  36159  unblimceq0  36210  unbdqndv1  36211  bj-hbntbi  36409  bj-equsexvwd  36486  bj-cbvexdv  36505  bj-ru0  36649  bj-nuliota  36764  topdifinffinlem  37054  topdifinffin  37055  icorempo  37058  relowlpssretop  37071  finxpreclem2  37097  finxpreclem6  37103  wl-issetft  37277  wl-ax11-lem8  37287  leceifl  37310  lindsadd  37314  lindsenlbs  37316  matunitlindflem1  37317  poimirlem16  37337  poimirlem17  37338  poimirlem18  37339  poimirlem19  37340  poimirlem21  37342  poimirlem23  37344  poimirlem26  37347  poimirlem27  37348  poimirlem28  37349  poimirlem31  37352  poimir  37354  mblfinlem2  37359  mblfinlem3  37360  ismblfin  37362  cnambfre  37369  itg2addnclem  37372  itg2addnclem2  37373  iblabsnclem  37384  ftc1anclem1  37394  areacirc  37414  heibor1lem  37510  heiborlem1  37512  heiborlem6  37517  heiborlem8  37519  heiborlem10  37521  smprngopr  37753  ecin0  38050  ax12inda  38646  riotaclbgBAD  38652  lcvfbr  38718  lcvbr  38719  lsatcv0  38729  l1cvpat  38752  opltcon3b  38902  cvrfval  38966  cvrval  38967  cvrnbtwn  38969  cvrval2  38972  cvrnbtwn2  38973  cvrnbtwn3  38974  cvrcon3b  38975  cvrnbtwn4  38977  atnlt  39011  iscvlat  39021  cvlexch1  39026  hlsuprexch  39080  hlrelat5N  39100  hlrelat2  39102  cvrval5  39114  3dimlem1  39157  3dim1lem5  39165  3dim2  39167  3dim3  39168  llnnlt  39222  islpln5  39234  lplni2  39236  lvolex3N  39237  lplnnle2at  39240  islpln2a  39247  lplnribN  39250  lplnexllnN  39263  lplnnlt  39264  lvoli3  39276  islvol5  39278  lvoli2  39280  lvolnle3at  39281  islvol2aN  39291  4atlem11  39308  lvolnltN  39317  dalawlem15  39584  4atexlemex2  39770  4atex  39775  4atex2-0aOLDN  39777  4atex2-0cOLDN  39779  lautcvr  39791  ltrnfset  39816  ltrnset  39817  ltrnu  39820  trlfset  39859  trlset  39860  trlval2  39862  cdlemd6  39902  cdleme0nex  39989  cdleme18d  39994  cdleme25b  40053  cdleme25cv  40057  cdleme29b  40074  cdleme31fv  40089  cdleme31fv2  40092  cdlemefrs29bpre0  40095  cdlemefr32sn2aw  40103  cdlemefr29bpre0N  40105  cdlemefr29clN  40106  cdlemefr32fvaN  40108  cdlemefr32fva1  40109  cdlemefs32sn1aw  40113  cdleme32fva  40136  cdleme32fvaw  40138  cdleme40v  40168  cdleme42b  40177  cdleme46f2g2  40192  cdleme46f2g1  40193  cdleme48gfv  40236  cdlemg1fvawlemN  40272  cdlemg1cex  40287  cdlemg6d  40320  cdlemm10N  40817  dicffval  40873  dicfval  40874  dicval  40875  dicfnN  40882  dicvalrelN  40884  dihffval  40929  dihfval  40930  dihlsscpre  40933  dvh4dimat  41137  dvh3dimatN  41138  dvh4dimlem  41142  dvh3dim  41145  dvh4dimN  41146  dvh3dim2  41147  dvh3dim3N  41148  mapdcv  41359  mapdh9aOLDN  41489  hdmapfval  41526  hdmapval  41527  hdmapval2  41531  hdmap11lem2  41541  dvrelog2b  41765  aks4d1p4  41778  aks4d1p5  41779  aks4d1p7  41782  aks4d1p8d2  41784  aks4d1p8  41786  aks4d1  41788  aks6d1c2p2  41817  hashnexinj  41826  rspcsbnea  41829  aks6d1c5  41837  aks6d1c6lem3  41870  aks6d1c7  41882  metakunt27  41917  metakunt28  41918  metakunt29  41919  supinf  41966  oexpreposd  42120  flt4lem7  42313  nna4b4nsq  42314  nfa1w  42330  ellz1  42424  rencldnfilem  42477  jm2.22  42653  jm2.23  42654  wepwsolem  42703  fnwe2lem2  42712  aomclem8  42722  unxpwdom3  42756  onsupmaxb  42904  onexlimgt  42908  onsupeqnmax  42912  onov0suclim  42940  oaordnr  42962  omnord1  42971  oenord1  42982  oaomoencom  42983  oenass  42985  cantnfresb  42990  tfsnfin  43018  ralopabb  43078  nlimsuc  43108  ifpbi12  43155  dfsucon  43190  sqrtcvallem1  43298  ss2iundf  43326  frege124d  43428  clsk3nimkb  43707  clsk1indlem1  43712  clsk1independent  43713  ntrneineine1lem  43751  ntrneicls11  43757  clsneiel1  43775  clsneiel2  43776  neicvgel1  43786  neicvgel2  43787  radcnvrat  43988  rusbcALT  44113  en3lpVD  44521  eliin2f  44705  nssd  44706  wessf1ornlem  44792  rexanuz2nf  45108  limsupre2lem  45345  icccncfext  45508  stoweidlem14  45635  stoweidlem34  45655  stoweidlem59  45680  etransclem24  45879  nnfoctbdjlem  46076  nnfoctbdj  46077  hspmbllem2  46248  nsssmfmbflem  46399  fsetsnprcnex  46670  eu2ndop1stv  46738  afvfv0bi  46765  afvco2  46789  ndmaovg  46797  ndfatafv2nrn  46834  afv2ndefb  46837  afv2fv0  46878  nelbr  46887  otiunsndisjX  46892  fun2dmnopgexmpl  46897  ltnltne  46912  readdcnnred  46916  resubcnnred  46917  recnmulnred  46918  cndivrenred  46919  ichnreuop  47044  fmtnoinf  47108  odz2prm2pw  47135  prmdvdsfmtnof1lem2  47157  lighneallem3  47179  lighneallem4  47182  requad1  47194  isodd3  47224  bits0ALTV  47251  nfermltl8rev  47314  nfermltl2rev  47315  nfermltlrev  47316  lidldomnnring  47613  ztprmneprm  47726  lindepsnlininds  47835  islindeps  47836  lindslinindsimp2lem5  47845  lindslinindsimp2  47846  difmodm1lt  47910  line2ylem  48139  line2xlem  48141  map0cor  48222  elsetrecslem  48445