Theorem notbid 321

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

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

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 210

This theorem is referenced by:  notbi  322  annotanannot  834  ifpbi123dOLD  1080  con3ALT  1086  xorbi12d  1522  norassOLD  1539  equsexvw  2015  cbvexvw  2048  cbvexdvaw  2050  hbe1w  2059  cbvexv1  2343  cbvex2v  2346  drex1v  2369  cbvex  2398  cbvex2  2411  drex1  2440  eujustALT  2573  necon3abid  2970  neleq12d  3042  rexbi  3154  rexeqbidvv  3306  cbvrexfw  3336  cbvrexf  3338  cgsex4g  3441  gencbval  3454  spcegf  3494  spc2gv  3502  spc2d  3504  spc3gv  3506  cdeqnot  3665  rru  3676  rruOLD  3677  ru  3678  sbcng  3726  sbcrext  3762  cbvrexcsf  3831  difjust  3843  eldif  3851  dfpss3  3975  dfdif3  4003  difeq2  4005  ab0OLD  4261  disjne  4341  pssdifcom1  4373  eldifpr  4545  rexsng  4562  elpwunsn  4571  eldiftp  4574  rexprg  4584  preqsnd  4741  disjxun  5025  nalset  5178  dtru  5234  dtruALT  5252  rexxfrd  5273  rexxfr2d  5275  rexxfrd2  5277  rexxfr  5280  dtruALT2  5299  opthneg  5336  snopeqop  5360  otiunsndisj  5374  poeq1  5441  pocl  5445  swopo  5448  sotric  5465  sotrieq  5466  isso2i  5472  somo  5474  freq1  5489  frirr  5496  fr2nr  5497  frminex  5499  tz7.2  5503  wereu2  5516  poinxp  5597  frinxp  5599  posn  5602  frsn  5604  rexiunxp  5677  rexxpf  5684  intirr  5946  poirr2  5952  cnvpo  6113  predpoirr  6151  predfrirr  6152  nordeq  6185  ordtri1  6199  ordtri3  6202  fvmpti  6768  fndmdif  6813  rexrnmptw  6865  rexrnmpt  6867  2f1fvneq  7023  f1imapss  7029  cbvexfo  7051  nf1const  7065  soisoi  7088  isopolem  7105  weniso  7114  canth  7118  riotaclb  7163  rexrnmpo  7299  ndmovg  7341  sorpssuni  7470  sorpssint  7471  fr3nr  7507  dfwe2  7509  ordsucsssuc  7551  nlimsucg  7570  orduninsuc  7571  dfom2  7595  ssnlim  7612  f1oweALT  7691  frxp  7839  poxp  7841  suppofssd  7891  suppcoss  7895  wfrlem10  7986  smoword  8025  tz7.48lem  8099  oacan  8198  oaword  8199  omlimcl  8228  omeulem1  8232  nnaword  8277  nnmword  8283  nneob  8303  brdifun  8342  swoer  8343  undifixp  8537  boxcutc  8544  2dom  8622  php  8744  nndomog  8751  nnsdomo  8786  unxpdomlem2  8795  frfi  8830  unfilem1  8849  supeq3  8979  supeq123d  8980  supmo  8982  eqsup  8986  supub  8989  sup0  8996  suppr  9001  supisolem  9003  supisoex  9004  eqinf  9014  infval  9016  infmo  9025  infpr  9033  infempty  9037  oieq1  9042  ordtypecbv  9047  ordtypelem7  9054  wemapsolem  9080  canthwdom  9109  zfregcl  9124  elirrv  9126  elirr  9127  noinfep  9189  cantnfp1lem3  9209  rankr1clem  9315  carden2b  9462  domtri2  9484  alephord3  9571  alephdom2  9580  alephval3  9603  dfac9  9629  kmlem2  9644  kmlem4  9646  isfin4  9790  isfin7  9794  fin23lem11  9810  isf32lem5  9850  isf34lem4  9870  fin1a2lem6  9898  fin1a2lem7  9899  fin1a2lem12  9904  itunisuc  9912  ac6n  9978  zorn2g  9996  zornn0g  9998  ttukeylem7  10008  axpowndlem3  10092  axpowndlem4  10093  axregnd  10097  elgch  10115  engch  10121  fpwwe2lem12  10135  fpwwe2  10136  pwfseqlem1  10151  pwfseqlem3  10153  hargch  10166  addnidpi  10394  pinq  10420  nqereu  10422  ltsonq  10462  prlem934  10526  ltexprlem7  10535  addcanpr  10539  prlem936  10540  reclem2pr  10541  reclem3pr  10542  supexpr  10547  ltsosr  10587  supsrlem  10604  axpre-lttri  10658  axpre-sup  10662  xrlenlt  10777  axlttri  10783  axsup  10787  ltne  10808  dedekind  10874  readdcan  10885  leadd1  11179  ltsub1  11207  ltsub2  11208  leord1  11238  lediv1  11576  lemuldiv  11591  lerec  11594  le2msq  11611  infm3  11670  suprnub  11676  infregelb  11695  avgle1  11949  avgle2  11950  znnnlt1  12083  indstr  12391  zsupss  12412  uzsupss  12415  rpneg  12497  xralrple  12674  xleneg  12687  xltadd1  12725  xposdif  12731  xmulneg1  12738  xltmul1  12761  xrsupexmnf  12774  xrinfmexpnf  12775  xrsupsslem  12776  xrinfmsslem  12777  xrub  12781  supxrleub  12795  infxrgelb  12804  difreicc  12951  nn0disj  13107  nelfzo  13127  elfznelfzo  13226  fvinim0ffz  13240  injresinjlem  13241  ssnn0fi  13437  leexp2  13620  hashbnd  13781  hasheni  13793  hashbc  13896  wrdsymb0  13983  swrdnd  14098  swrdnd2  14099  pfxnd0  14132  repswswrd  14228  repswccat  14230  cshwidxmod  14247  cnpart  14682  sqrtlt  14704  limsuplt  14919  rlimrege0  15019  isercoll  15110  efle  15556  odd2np1  15779  sumodd  15826  divalglem7  15837  ndvdsadd  15848  fldivndvdslt  15852  bitsfval  15859  bitsval  15860  bits0  15864  bitsp1  15867  bitsmod  15872  bitscmp  15874  bitsinv1lem  15877  sadadd2lem2  15886  saddisjlem  15900  bitsshft  15911  gcdneg  15958  algcvgblem  16011  lcmneg  16037  isprm3  16117  dvdsnprmd  16124  isprm5  16141  rpexp  16156  phiprmpw  16206  m1dvdsndvds  16228  pythagtrip  16264  pcgcd1  16306  prmpwdvds  16333  prmreclem2  16346  prmreclem3  16347  prmreclem5  16349  prmreclem6  16350  vdwlem6  16415  vdwnnlem2  16425  vdwnnlem3  16426  vdwnn  16427  prmlem0  16535  prmlem1a  16536  divsfval  16916  mrisval  16997  ismri  16998  ismri2dad  17004  cidpropd  17077  cat1lem  17461  plttr  17689  joinval  17724  meetval  17738  acsfiindd  17896  isnsgrp  18014  smndex1n0mnd  18186  mgm2nsgrplem2  18193  sgrp2nmndlem3  18199  symgpssefmnd  18635  symgfix2  18655  pmtrdifellem4  18718  psgnunilem1  18732  psgnunilem5  18733  psgnunilem2  18734  psgnunilem3  18735  pmtrsn  18758  sylow1lem3  18836  sylow2alem2  18854  efgsfo  18976  ablfac1eulem  19306  ablfac1eu  19307  pgpfac1lem1  19308  pgpfac1lem5  19313  islbs  19960  lbsind  19964  lbspss  19966  lbspropd  19983  lspsnne1  20001  islbs2  20038  lbsacsbs  20040  lbsextlem1  20042  lbsextlem3  20044  lbsextlem4  20045  lbsextg  20046  nzrunit  20152  frlmlbs  20606  islindf  20621  islinds2  20622  islindf2  20623  lindfind  20625  lindsind  20626  lindfrn  20630  lindfmm  20636  lsslindf  20639  islindf4  20647  opsrtoslem2  20860  cply1coe0  21067  cply1coe0bi  21068  mdetunilem7  21362  mdetunilem8  21363  mdetunilem9  21364  maducoeval2  21384  pmatcollpw3fi1lem1  21530  fvmptnn04ifa  21594  fvmptnn04ifc  21596  fvmptnn04ifd  21597  chfacffsupp  21600  chfacfscmul0  21602  chfacfpmmul0  21606  elcls  21817  maxlp  21891  perfi  21899  ordtbaslem  21932  ordtval  21933  ordtbas2  21935  ordtopn1  21938  ordtopn2  21939  ordtcnv  21945  ordtrest  21946  ordtrest2lem  21947  ordtrest2  21948  pnfnei  21964  mnfnei  21965  isreg2  22121  ordthauslem  22127  cmpfi  22152  cmpfii  22153  bwth  22154  nconnsubb  22167  hausdiag  22389  txkgen  22396  kqdisj  22476  ordthmeolem  22545  fbfinnfr  22585  trfbas  22588  fbunfip  22613  fbasrn  22628  trfil3  22632  ufileu  22663  fin1aufil  22676  hausflim  22725  alexsubALTlem2  22792  alexsubALTlem3  22793  alexsubALTlem4  22794  ptcmplem2  22797  ptcmplem3  22798  stdbdbl  23263  iccntr  23566  reconnlem2  23572  iccpnfcnv  23689  xrhmeo  23691  lebnumlem1  23706  lebnumlem2  23707  lebnumlem3  23708  bcthlem4  24072  minveclem3b  24173  ivthlem2  24197  ivthlem3  24198  mbfmax  24394  mbfposr  24397  i1fd  24426  mbfi1fseqlem4  24463  itg2splitlem  24493  itg2monolem1  24495  itg2cnlem1  24506  dvne0  24755  lhop1lem  24757  deg1nn0clb  24835  dgrle  24984  coemulhi  24995  aaliou3lem9  25090  cos11  25269  logleb  25338  argrege0  25346  logdivle  25357  ellogdm  25374  cxple  25430  cxplt2  25433  cxple3  25436  isosctrlem1  25548  atandm  25606  atans2  25661  atantayl2  25668  eldmgm  25751  ftalem7  25808  isppw2  25844  musum  25920  dchrsum2  25996  bposlem1  26012  lgsmod  26051  lgsdir2lem2  26054  lgsdir2  26058  lgsne0  26063  lgsprme0  26067  gausslemma2dlem4  26097  lgsquadlem1  26108  2lgslem3  26132  2lgsoddprm  26144  2sq2  26161  addsqrexnreu  26170  rpvmasumlem  26215  padicabv  26358  ostth3  26366  ostth  26367  istrkgld  26397  axtgupdim2  26409  tglowdim2l  26588  axlowdimlem16  26895  axlowdim2  26898  axlowdim  26899  numedglnl  27081  usgredg2v  27161  lfuhgr1v0e  27188  cusgrfi  27392  vtxd0nedgb  27422  vtxduhgr0edgnel  27428  1loopgrnb0  27436  1hevtxdg0  27439  vtxdgoddnumeven  27487  wlkp1lem1  27607  wlkp1lem2  27608  wlkp1lem5  27611  crctcsh  27754  clwlkclwwlklem2a4  27926  eupth2eucrct  28146  eupth2lem3lem3  28159  eupth2lem3lem4  28160  eupth2lem3lem6  28162  eupth2lem3lem7  28163  eupth2lems  28167  eupth2  28168  konigsberglem4  28184  nfrgr2v  28201  frgrwopreglem3  28243  fusgr2wsp2nb  28263  frgrreggt1  28322  friendshipgt3  28327  lpni  28407  nmobndseqi  28706  minvecolem5  28808  chpsscon3  29430  chnle  29441  nonbooli  29578  pjnel  29653  specval  29825  nmcfnlbi  29979  stri  30184  hstri  30192  cvbr  30209  cvcon3  30211  chcv1  30282  cvexchlem  30295  chrelat2  30297  nelun  30425  elpreq  30444  nelpr  30445  ifeqeqx  30451  nfpconfp  30533  suppiniseg  30587  isoun  30601  suppss3  30626  xrge0infss  30650  infxrge0gelb  30656  eliccelico  30665  elicoelioo  30666  nndiffz1  30674  hashgt1  30695  nn0min  30701  toslublem  30819  tosglblem  30821  pmtrcnel  30927  cycpmco2  30969  isarchi2  31008  archiabl  31021  0nellinds  31130  lindssn  31137  lindfpropd  31140  ssmxidl  31206  lbslsat  31263  lindsunlem  31269  ordtcnvNEW  31434  ordtrestNEW  31435  ordtrest2NEWlem  31436  ordtrest2NEW  31437  ordtconnlem1  31438  xrge0iifcnv  31447  esumpcvgval  31608  esum2d  31623  ddemeas  31766  omssubadd  31829  oddpwdc  31883  eulerpartlems  31889  eulerpartlemf  31899  eulerpartlemt  31900  eulerpartlemr  31903  eulerpartlemgvv  31905  eulerpartlemn  31910  ballotlemfc0  32021  ballotlemfcc  32022  ballotlem4  32027  ballotlemimin  32034  ballotlem7  32064  plymulx  32089  signsply0  32092  reprinfz1  32164  reprpmtf1o  32168  reprdifc  32169  hgt750lema  32199  hgt750leme  32200  istrkg2d  32208  bnj23  32259  bnj1185  32336  bnj1228  32554  bnj1388  32576  bnj1417  32584  nummin  32626  hashfundm  32637  revwlk  32649  isacycgr  32670  acycgr0v  32673  prclisacycgr  32676  erdszelem10  32725  satf0n0  32903  fmlaomn0  32915  fmlasucdisj  32924  satfv1fvfmla1  32948  satefvfmla1  32950  ismfs  33074  mvtinf  33080  untelirr  33212  untsucf  33214  untangtr  33218  ceqsralv2  33235  dfpo2  33286  dfon2lem3  33325  dfon2lem4  33326  dfon2lem7  33329  dfon2lem9  33331  distel  33343  frpomin  33373  frxp2  33394  frxp3  33400  soseq  33406  naddss1  33474  noextenddif  33504  nodenselem4  33523  nodenselem5  33524  nodenselem7  33526  nolt02o  33531  nogt01o  33532  noresle  33533  nosupprefixmo  33536  noinfprefixmo  33537  nosupcbv  33538  nosupdm  33540  nosupfv  33542  nosupres  33543  nosupbnd1lem1  33544  nosupbnd1lem3  33546  nosupbnd1lem5  33548  nosupbnd1  33550  nosupbnd2lem1  33551  nosupbnd2  33552  noinfcbv  33553  noinfdm  33555  noinffv  33557  noinfres  33558  noinfbnd1lem1  33559  noinfbnd1lem3  33561  noinfbnd1lem5  33563  noinfbnd1  33565  noinfbnd2lem1  33566  noinfbnd2  33567  slenlt  33588  nocvxminlem  33605  slerec  33646  newbday  33712  sltlpss  33717  cofcutr  33722  lrrecfr  33729  no3indslem  33744  addsov  33756  funpartfv  33877  dfrdg4  33883  nn0prpwlem  34141  nn0prpw  34142  limsucncmpi  34264  limsucncmp  34265  ordcmp  34266  unblimceq0  34317  unbdqndv1  34318  bj-hbntbi  34513  bj-cbvexdv  34602  bj-dtru  34619  bj-ru0  34743  bj-nuliota  34840  topdifinffinlem  35130  topdifinffin  35131  icorempo  35134  relowlpssretop  35147  finxpreclem2  35173  finxpreclem6  35179  wl-ax11-lem8  35355  leceifl  35378  lindsadd  35382  lindsenlbs  35384  matunitlindflem1  35385  poimirlem16  35405  poimirlem17  35406  poimirlem18  35407  poimirlem19  35408  poimirlem21  35410  poimirlem23  35412  poimirlem26  35415  poimirlem27  35416  poimirlem28  35417  poimirlem31  35420  poimir  35422  mblfinlem2  35427  mblfinlem3  35428  ismblfin  35430  cnambfre  35437  itg2addnclem  35440  itg2addnclem2  35441  iblabsnclem  35452  ftc1anclem1  35462  areacirc  35482  heibor1lem  35579  heiborlem1  35581  heiborlem6  35586  heiborlem8  35588  heiborlem10  35590  smprngopr  35822  ecin0  36096  ax12inda  36574  riotaclbgBAD  36580  lcvfbr  36646  lcvbr  36647  lsatcv0  36657  l1cvpat  36680  opltcon3b  36830  cvrfval  36894  cvrval  36895  cvrnbtwn  36897  cvrval2  36900  cvrnbtwn2  36901  cvrnbtwn3  36902  cvrcon3b  36903  cvrnbtwn4  36905  atnlt  36939  iscvlat  36949  cvlexch1  36954  hlsuprexch  37007  hlrelat5N  37027  hlrelat2  37029  cvrval5  37041  3dimlem1  37084  3dim1lem5  37092  3dim2  37094  3dim3  37095  llnnlt  37149  islpln5  37161  lplni2  37163  lvolex3N  37164  lplnnle2at  37167  islpln2a  37174  lplnribN  37177  lplnexllnN  37190  lplnnlt  37191  lvoli3  37203  islvol5  37205  lvoli2  37207  lvolnle3at  37208  islvol2aN  37218  4atlem11  37235  lvolnltN  37244  dalawlem15  37511  4atexlemex2  37697  4atex  37702  4atex2-0aOLDN  37704  4atex2-0cOLDN  37706  lautcvr  37718  ltrnfset  37743  ltrnset  37744  ltrnu  37747  trlfset  37786  trlset  37787  trlval2  37789  cdlemd6  37829  cdleme0nex  37916  cdleme18d  37921  cdleme25b  37980  cdleme25cv  37984  cdleme29b  38001  cdleme31fv  38016  cdleme31fv2  38019  cdlemefrs29bpre0  38022  cdlemefr32sn2aw  38030  cdlemefr29bpre0N  38032  cdlemefr29clN  38033  cdlemefr32fvaN  38035  cdlemefr32fva1  38036  cdlemefs32sn1aw  38040  cdleme32fva  38063  cdleme32fvaw  38065  cdleme40v  38095  cdleme42b  38104  cdleme46f2g2  38119  cdleme46f2g1  38120  cdleme48gfv  38163  cdlemg1fvawlemN  38199  cdlemg1cex  38214  cdlemg6d  38247  cdlemm10N  38744  dicffval  38800  dicfval  38801  dicval  38802  dicfnN  38809  dicvalrelN  38811  dihffval  38856  dihfval  38857  dihlsscpre  38860  dvh4dimat  39064  dvh3dimatN  39065  dvh4dimlem  39069  dvh3dim  39072  dvh4dimN  39073  dvh3dim2  39074  dvh3dim3N  39075  mapdcv  39286  mapdh9aOLDN  39416  hdmapfval  39453  hdmapval  39454  hdmapval2  39458  hdmap11lem2  39468  dvrelog2b  39682  metakunt27  39731  metakunt28  39732  metakunt29  39733  oexpreposd  39881  exp11nnd  39885  flt4lem7  40052  nna4b4nsq  40053  ellz1  40145  rencldnfilem  40198  jm2.22  40373  jm2.23  40374  wepwsolem  40423  fnwe2lem2  40432  aomclem8  40442  unxpwdom3  40476  ifpbi12  40633  dfsucon  40668  sqrtcvallem1  40768  ss2iundf  40797  frege124d  40899  clsk3nimkb  41180  clsk1indlem1  41185  clsk1independent  41186  ntrneineine1lem  41224  ntrneicls11  41230  clsneiel1  41248  clsneiel2  41249  neicvgel1  41259  neicvgel2  41260  radcnvrat  41454  rusbcALT  41579  en3lpVD  41987  eliin2f  42176  nssd  42177  wessf1ornlem  42244  limsupre2lem  42791  icccncfext  42954  stoweidlem14  43081  stoweidlem34  43101  stoweidlem59  43126  etransclem24  43325  nnfoctbdjlem  43519  nnfoctbdj  43520  hspmbllem2  43691  nsssmfmbflem  43836  fsetsnprcnex  44071  eu2ndop1stv  44134  afvfv0bi  44161  afvco2  44185  ndmaovg  44193  ndfatafv2nrn  44230  afv2ndefb  44233  afv2fv0  44274  nelbr  44283  otiunsndisjX  44288  fun2dmnopgexmpl  44293  ltnltne  44309  readdcnnred  44313  resubcnnred  44314  recnmulnred  44315  cndivrenred  44316  ichnreuop  44442  fmtnoinf  44506  odz2prm2pw  44533  prmdvdsfmtnof1lem2  44555  lighneallem3  44577  lighneallem4  44580  requad1  44592  isodd3  44622  bits0ALTV  44649  nfermltl8rev  44712  nfermltl2rev  44713  nfermltlrev  44714  lidldomnnring  45006  zrninitoringc  45147  ztprmneprm  45201  lindepsnlininds  45311  islindeps  45312  lindslinindsimp2lem5  45321  lindslinindsimp2  45322  difmodm1lt  45386  line2ylem  45615  line2xlem  45617  elsetrecslem  45841