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  3645  cdeqnot  3764  rru  3775  ru  3776  sbcng  3827  sbcrext  3867  cbvrexcsf  3939  difjust  3950  eldif  3958  dfpss3  4086  dfdif3  4114  difeq2  4116  ab0OLD  4375  disjne  4454  pssdifcom1  4489  eldifpr  4660  rexsng  4678  elpwunsn  4687  eldiftp  4690  rexprg  4700  preqsnd  4859  disjxun  5146  nalset  5313  dtruALT2  5368  dtruALT  5386  rexxfrd  5407  rexxfr2d  5409  rexxfrd2  5411  rexxfr  5414  dtruOLD  5441  opthneg  5481  snopeqop  5506  otiunsndisj  5520  poeq1  5591  pocl  5595  poclOLD  5596  swopo  5599  sotric  5616  sotrieq  5617  isso2i  5623  somo  5625  freq1  5646  frirr  5653  fr2nr  5654  frminex  5656  tz7.2  5660  wereu2  5673  poinxp  5755  frinxp  5757  posn  5760  frsn  5762  rexiunxp  5839  rexxpf  5846  intirr  6117  poirr2  6123  cnvpo  6284  dfpo2  6293  predpoirr  6332  predfrirr  6333  frpomin  6339  nordeq  6381  ordtri1  6395  ordtri3  6398  fvmpti  6995  fndmdif  7041  rexrnmptw  7094  rexrnmpt  7096  2f1fvneq  7256  f1imapss  7262  cbvexfo  7285  nf1const  7299  soisoi  7322  isopolem  7339  weniso  7348  imaeqsalv  7358  canth  7359  riotaclb  7404  rexrnmpo  7545  ndmovg  7587  sorpssuni  7719  sorpssint  7720  fr3nr  7756  dfwe2  7758  ordsucsssuc  7808  nlimsucg  7828  orduninsuc  7829  dfom2  7854  ssnlim  7872  f1oweALT  7956  frxp  8109  poxp  8111  frxp2  8127  frxp3  8134  xpord3inddlem  8137  soseq  8142  suppofssd  8185  suppcoss  8189  wfrlem10OLD  8315  smoword  8363  tz7.48lem  8438  oacan  8545  oaword  8546  omlimcl  8575  omeulem1  8579  nnaword  8624  nnmword  8630  nneob  8652  naddss1  8685  brdifun  8729  swoer  8730  undifixp  8925  boxcutc  8932  2dom  9027  php  9207  phpeqd  9212  nndomog  9213  phpOLD  9219  nndomogOLD  9223  onomeneq  9225  nnsdomo  9231  unxpdomlem2  9248  frfi  9285  unfilem1  9307  supeq3  9441  supeq123d  9442  supmo  9444  eqsup  9448  supub  9451  sup0  9458  suppr  9463  supisolem  9465  supisoex  9466  eqinf  9476  infval  9478  infmo  9487  infpr  9495  infempty  9499  oieq1  9504  ordtypecbv  9509  ordtypelem7  9516  wemapsolem  9542  canthwdom  9571  zfregcl  9586  elirrv  9588  elirr  9589  noinfep  9652  cantnfp1lem3  9672  ttrcltr  9708  rankr1clem  9812  carden2b  9959  domtri2  9981  alephord3  10070  alephdom2  10079  alephval3  10102  dfac9  10128  kmlem2  10143  kmlem4  10145  isfin4  10289  isfin7  10293  fin23lem11  10309  isf32lem5  10349  isf34lem4  10369  fin1a2lem6  10397  fin1a2lem7  10398  fin1a2lem12  10403  itunisuc  10411  ac6n  10477  zorn2g  10495  zornn0g  10497  ttukeylem7  10507  axpowndlem3  10591  axpowndlem4  10592  axregnd  10596  elgch  10614  engch  10620  fpwwe2lem12  10634  fpwwe2  10635  pwfseqlem1  10650  pwfseqlem3  10652  hargch  10665  addnidpi  10893  pinq  10919  nqereu  10921  ltsonq  10961  prlem934  11025  ltexprlem7  11034  addcanpr  11038  prlem936  11039  reclem2pr  11040  reclem3pr  11041  supexpr  11046  ltsosr  11086  supsrlem  11103  axpre-lttri  11157  axpre-sup  11161  xrlenlt  11276  axlttri  11282  axsup  11286  ltne  11308  dedekind  11374  readdcan  11385  leadd1  11679  ltsub1  11707  ltsub2  11708  leord1  11738  lediv1  12076  lemuldiv  12091  lerec  12094  le2msq  12111  infm3  12170  suprnub  12176  infregelb  12195  avgle1  12449  avgle2  12450  znnnlt1  12586  indstr  12897  zsupss  12918  uzsupss  12921  rpneg  13003  xralrple  13181  xleneg  13194  xltadd1  13232  xposdif  13238  xmulneg1  13245  xltmul1  13268  xrsupexmnf  13281  xrinfmexpnf  13282  xrsupsslem  13283  xrinfmsslem  13284  xrub  13288  supxrleub  13302  infxrgelb  13311  difreicc  13458  nn0disj  13614  nelfzo  13634  elfznelfzo  13734  fvinim0ffz  13748  injresinjlem  13749  ssnn0fi  13947  leexp2  14133  hashbnd  14293  hasheni  14305  hashfundm  14399  hashbc  14409  wrdsymb0  14496  swrdnd  14601  swrdnd2  14602  pfxnd0  14635  repswswrd  14731  repswccat  14733  cshwidxmod  14750  cnpart  15184  sqrtlt  15205  limsuplt  15420  rlimrege0  15520  isercoll  15611  efle  16058  odd2np1  16281  sumodd  16328  divalglem7  16339  ndvdsadd  16350  fldivndvdslt  16354  bitsfval  16361  bitsval  16362  bits0  16366  bitsp1  16369  bitsmod  16374  bitscmp  16376  bitsinv1lem  16379  sadadd2lem2  16388  saddisjlem  16402  bitsshft  16413  gcdneg  16460  algcvgblem  16511  lcmneg  16537  isprm3  16617  dvdsnprmd  16624  isprm5  16641  rpexp  16656  phiprmpw  16706  m1dvdsndvds  16728  pythagtrip  16764  pcgcd1  16807  prmpwdvds  16834  prmreclem2  16847  prmreclem3  16848  prmreclem5  16850  prmreclem6  16851  vdwlem6  16916  vdwnnlem2  16926  vdwnnlem3  16927  vdwnn  16928  prmlem0  17036  prmlem1a  17037  divsfval  17490  mrisval  17571  ismri  17572  ismri2dad  17578  cidpropd  17651  cat1lem  18043  plttr  18292  joinval  18327  meetval  18341  acsfiindd  18503  isnsgrp  18611  smndex1n0mnd  18790  mgm2nsgrplem2  18797  sgrp2nmndlem3  18803  symgpssefmnd  19258  symgfix2  19279  pmtrdifellem4  19342  psgnunilem1  19356  psgnunilem5  19357  psgnunilem2  19358  psgnunilem3  19359  pmtrsn  19382  sylow1lem3  19463  sylow2alem2  19481  efgsfo  19602  ablfac1eulem  19937  ablfac1eu  19938  pgpfac1lem1  19939  pgpfac1lem5  19944  nzrunit  20294  islbs  20680  lbsind  20684  lbspss  20686  lbspropd  20703  lspsnne1  20723  islbs2  20760  lbsacsbs  20762  lbsextlem1  20764  lbsextlem3  20766  lbsextlem4  20767  lbsextg  20768  frlmlbs  21344  islindf  21359  islinds2  21360  islindf2  21361  lindfind  21363  lindsind  21364  lindfrn  21368  lindfmm  21374  lsslindf  21377  islindf4  21385  opsrtoslem2  21609  cply1coe0  21815  cply1coe0bi  21816  mdetunilem7  22112  mdetunilem8  22113  mdetunilem9  22114  maducoeval2  22134  pmatcollpw3fi1lem1  22280  fvmptnn04ifa  22344  fvmptnn04ifc  22346  fvmptnn04ifd  22347  chfacffsupp  22350  chfacfscmul0  22352  chfacfpmmul0  22356  elcls  22569  maxlp  22643  perfi  22651  ordtbaslem  22684  ordtval  22685  ordtbas2  22687  ordtopn1  22690  ordtopn2  22691  ordtcnv  22697  ordtrest  22698  ordtrest2lem  22699  ordtrest2  22700  pnfnei  22716  mnfnei  22717  isreg2  22873  ordthauslem  22879  cmpfi  22904  cmpfii  22905  bwth  22906  nconnsubb  22919  hausdiag  23141  txkgen  23148  kqdisj  23228  ordthmeolem  23297  fbfinnfr  23337  trfbas  23340  fbunfip  23365  fbasrn  23380  trfil3  23384  ufileu  23415  fin1aufil  23428  hausflim  23477  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALTlem4  23546  ptcmplem2  23549  ptcmplem3  23550  stdbdbl  24018  iccntr  24329  reconnlem2  24335  iccpnfcnv  24452  xrhmeo  24454  lebnumlem1  24469  lebnumlem2  24470  lebnumlem3  24471  bcthlem4  24836  minveclem3b  24937  ivthlem2  24961  ivthlem3  24962  mbfmax  25158  mbfposr  25161  i1fd  25190  mbfi1fseqlem4  25228  itg2splitlem  25258  itg2monolem1  25260  itg2cnlem1  25271  dvne0  25520  lhop1lem  25522  deg1nn0clb  25600  dgrle  25749  coemulhi  25760  aaliou3lem9  25855  cos11  26034  logleb  26103  argrege0  26111  logdivle  26122  ellogdm  26139  cxple  26195  cxplt2  26198  cxple3  26201  isosctrlem1  26313  atandm  26371  atans2  26426  atantayl2  26433  eldmgm  26516  ftalem7  26573  isppw2  26609  musum  26685  dchrsum2  26761  bposlem1  26777  lgsmod  26816  lgsdir2lem2  26819  lgsdir2  26823  lgsne0  26828  lgsprme0  26832  gausslemma2dlem4  26862  lgsquadlem1  26873  2lgslem3  26897  2lgsoddprm  26909  2sq2  26926  addsqrexnreu  26935  rpvmasumlem  26980  padicabv  27123  ostth3  27131  ostth  27132  noextenddif  27161  nodenselem4  27180  nodenselem5  27181  nodenselem7  27183  nolt02o  27188  nogt01o  27189  noresle  27190  nosupprefixmo  27193  noinfprefixmo  27194  nosupcbv  27195  nosupdm  27197  nosupfv  27199  nosupres  27200  nosupbnd1lem1  27201  nosupbnd1lem3  27203  nosupbnd1lem5  27205  nosupbnd1  27207  nosupbnd2lem1  27208  nosupbnd2  27209  noinfcbv  27210  noinfdm  27212  noinffv  27214  noinfres  27215  noinfbnd1lem1  27216  noinfbnd1lem3  27218  noinfbnd1lem5  27220  noinfbnd1  27222  noinfbnd2lem1  27223  noinfbnd2  27224  slenlt  27245  sltne  27263  nocvxminlem  27269  slerec  27310  cuteq1  27324  newbday  27386  sltlpss  27391  cofcutr  27401  lrrecfr  27417  addsval  27436  sltadd2  27464  sleneg  27510  slesubsubbd  27543  slesubsub2bd  27544  slesubsub3bd  27545  sltmul2  27613  slemul2d  27616  slemul1d  27617  istrkgld  27700  axtgupdim2  27712  tglowdim2l  27891  axlowdimlem16  28205  axlowdim2  28208  axlowdim  28209  numedglnl  28394  usgredg2v  28474  lfuhgr1v0e  28501  cusgrfi  28705  vtxd0nedgb  28735  vtxduhgr0edgnel  28741  1loopgrnb0  28749  1hevtxdg0  28752  vtxdgoddnumeven  28800  wlkp1lem1  28920  wlkp1lem2  28921  wlkp1lem5  28924  crctcsh  29068  clwlkclwwlklem2a4  29240  eupth2eucrct  29460  eupth2lem3lem3  29473  eupth2lem3lem4  29474  eupth2lem3lem6  29476  eupth2lem3lem7  29477  eupth2lems  29481  eupth2  29482  konigsberglem4  29498  nfrgr2v  29515  frgrwopreglem3  29557  fusgr2wsp2nb  29577  frgrreggt1  29636  friendshipgt3  29641  lpni  29721  nmobndseqi  30020  minvecolem5  30122  chpsscon3  30744  chnle  30755  nonbooli  30892  pjnel  30967  specval  31139  nmcfnlbi  31293  stri  31498  hstri  31506  cvbr  31523  cvcon3  31525  chcv1  31596  cvexchlem  31609  chrelat2  31611  nelun  31739  elpreq  31755  nelpr  31756  ifeqeqx  31762  nfpconfp  31844  suppiniseg  31896  isoun  31911  suppss3  31937  xrge0infss  31961  infxrge0gelb  31967  eliccelico  31976  elicoelioo  31977  nndiffz1  31985  hashgt1  32008  nn0min  32014  toslublem  32130  tosglblem  32132  pmtrcnel  32238  cycpmco2  32280  isarchi2  32319  archiabl  32332  0nellinds  32472  lindssn  32483  lindfpropd  32487  mxidlirred  32577  ssmxidl  32579  lbslsat  32690  lindsunlem  32698  ordtcnvNEW  32889  ordtrestNEW  32890  ordtrest2NEWlem  32891  ordtrest2NEW  32892  ordtconnlem1  32893  xrge0iifcnv  32902  esumpcvgval  33065  esum2d  33080  ddemeas  33223  omssubadd  33288  oddpwdc  33342  eulerpartlems  33348  eulerpartlemf  33358  eulerpartlemt  33359  eulerpartlemr  33362  eulerpartlemgvv  33364  eulerpartlemn  33369  ballotlemfc0  33480  ballotlemfcc  33481  ballotlem4  33486  ballotlemimin  33493  ballotlem7  33523  plymulx  33548  signsply0  33551  reprinfz1  33623  reprpmtf1o  33627  reprdifc  33628  hgt750lema  33658  hgt750leme  33659  istrkg2d  33667  bnj23  33718  bnj1185  33793  bnj1228  34011  bnj1388  34033  bnj1417  34041  nummin  34083  revwlk  34104  isacycgr  34125  acycgr0v  34128  prclisacycgr  34131  erdszelem10  34180  satf0n0  34358  fmlaomn0  34370  fmlasucdisj  34379  satfv1fvfmla1  34403  satefvfmla1  34405  ismfs  34529  mvtinf  34535  untelirr  34666  untsucf  34668  untangtr  34672  dfon2lem3  34746  dfon2lem4  34747  dfon2lem7  34750  dfon2lem9  34752  distel  34764  funpartfv  34906  dfrdg4  34912  nn0prpwlem  35196  nn0prpw  35197  limsucncmpi  35319  limsucncmp  35320  ordcmp  35321  unblimceq0  35372  unbdqndv1  35373  bj-hbntbi  35571  bj-equsexvwd  35648  bj-cbvexdv  35667  bj-ru0  35812  bj-nuliota  35927  topdifinffinlem  36217  topdifinffin  36218  icorempo  36221  relowlpssretop  36234  finxpreclem2  36260  finxpreclem6  36266  wl-issetft  36433  wl-ax11-lem8  36443  leceifl  36466  lindsadd  36470  lindsenlbs  36472  matunitlindflem1  36473  poimirlem16  36493  poimirlem17  36494  poimirlem18  36495  poimirlem19  36496  poimirlem21  36498  poimirlem23  36500  poimirlem26  36503  poimirlem27  36504  poimirlem28  36505  poimirlem31  36508  poimir  36510  mblfinlem2  36515  mblfinlem3  36516  ismblfin  36518  cnambfre  36525  itg2addnclem  36528  itg2addnclem2  36529  iblabsnclem  36540  ftc1anclem1  36550  areacirc  36570  heibor1lem  36666  heiborlem1  36668  heiborlem6  36673  heiborlem8  36675  heiborlem10  36677  smprngopr  36909  ecin0  37210  ax12inda  37807  riotaclbgBAD  37813  lcvfbr  37879  lcvbr  37880  lsatcv0  37890  l1cvpat  37913  opltcon3b  38063  cvrfval  38127  cvrval  38128  cvrnbtwn  38130  cvrval2  38133  cvrnbtwn2  38134  cvrnbtwn3  38135  cvrcon3b  38136  cvrnbtwn4  38138  atnlt  38172  iscvlat  38182  cvlexch1  38187  hlsuprexch  38241  hlrelat5N  38261  hlrelat2  38263  cvrval5  38275  3dimlem1  38318  3dim1lem5  38326  3dim2  38328  3dim3  38329  llnnlt  38383  islpln5  38395  lplni2  38397  lvolex3N  38398  lplnnle2at  38401  islpln2a  38408  lplnribN  38411  lplnexllnN  38424  lplnnlt  38425  lvoli3  38437  islvol5  38439  lvoli2  38441  lvolnle3at  38442  islvol2aN  38452  4atlem11  38469  lvolnltN  38478  dalawlem15  38745  4atexlemex2  38931  4atex  38936  4atex2-0aOLDN  38938  4atex2-0cOLDN  38940  lautcvr  38952  ltrnfset  38977  ltrnset  38978  ltrnu  38981  trlfset  39020  trlset  39021  trlval2  39023  cdlemd6  39063  cdleme0nex  39150  cdleme18d  39155  cdleme25b  39214  cdleme25cv  39218  cdleme29b  39235  cdleme31fv  39250  cdleme31fv2  39253  cdlemefrs29bpre0  39256  cdlemefr32sn2aw  39264  cdlemefr29bpre0N  39266  cdlemefr29clN  39267  cdlemefr32fvaN  39269  cdlemefr32fva1  39270  cdlemefs32sn1aw  39274  cdleme32fva  39297  cdleme32fvaw  39299  cdleme40v  39329  cdleme42b  39338  cdleme46f2g2  39353  cdleme46f2g1  39354  cdleme48gfv  39397  cdlemg1fvawlemN  39433  cdlemg1cex  39448  cdlemg6d  39481  cdlemm10N  39978  dicffval  40034  dicfval  40035  dicval  40036  dicfnN  40043  dicvalrelN  40045  dihffval  40090  dihfval  40091  dihlsscpre  40094  dvh4dimat  40298  dvh3dimatN  40299  dvh4dimlem  40303  dvh3dim  40306  dvh4dimN  40307  dvh3dim2  40308  dvh3dim3N  40309  mapdcv  40520  mapdh9aOLDN  40650  hdmapfval  40687  hdmapval  40688  hdmapval2  40692  hdmap11lem2  40702  dvrelog2b  40920  aks4d1p4  40933  aks4d1p5  40934  aks4d1p7  40937  aks4d1p8d2  40939  aks4d1p8  40941  aks4d1  40943  aks6d1c2p2  40946  metakunt27  41000  metakunt28  41001  metakunt29  41002  oexpreposd  41208  exp11nnd  41211  flt4lem7  41398  nna4b4nsq  41399  ellz1  41491  rencldnfilem  41544  jm2.22  41720  jm2.23  41721  wepwsolem  41770  fnwe2lem2  41779  aomclem8  41789  unxpwdom3  41823  onsupmaxb  41974  onexlimgt  41978  onsupeqnmax  41982  onov0suclim  42010  oaordnr  42032  omnord1  42041  oenord1  42052  oaomoencom  42053  oenass  42055  cantnfresb  42060  tfsnfin  42088  ralopabb  42148  nlimsuc  42178  ifpbi12  42225  dfsucon  42260  sqrtcvallem1  42368  ss2iundf  42396  frege124d  42498  clsk3nimkb  42777  clsk1indlem1  42782  clsk1independent  42783  ntrneineine1lem  42821  ntrneicls11  42827  clsneiel1  42845  clsneiel2  42846  neicvgel1  42856  neicvgel2  42857  radcnvrat  43059  rusbcALT  43184  en3lpVD  43592  eliin2f  43779  nssd  43780  wessf1ornlem  43868  rexanuz2nf  44190  limsupre2lem  44427  icccncfext  44590  stoweidlem14  44717  stoweidlem34  44737  stoweidlem59  44762  etransclem24  44961  nnfoctbdjlem  45158  nnfoctbdj  45159  hspmbllem2  45330  nsssmfmbflem  45481  fsetsnprcnex  45752  eu2ndop1stv  45820  afvfv0bi  45847  afvco2  45871  ndmaovg  45879  ndfatafv2nrn  45916  afv2ndefb  45919  afv2fv0  45960  nelbr  45969  otiunsndisjX  45974  fun2dmnopgexmpl  45979  ltnltne  45994  readdcnnred  45998  resubcnnred  45999  recnmulnred  46000  cndivrenred  46001  ichnreuop  46127  fmtnoinf  46191  odz2prm2pw  46218  prmdvdsfmtnof1lem2  46240  lighneallem3  46262  lighneallem4  46265  requad1  46277  isodd3  46307  bits0ALTV  46334  nfermltl8rev  46397  nfermltl2rev  46398  nfermltlrev  46399  lidldomnnring  46782  zrninitoringc  46923  ztprmneprm  46977  lindepsnlininds  47087  islindeps  47088  lindslinindsimp2lem5  47097  lindslinindsimp2  47098  difmodm1lt  47162  line2ylem  47391  line2xlem  47393  map0cor  47475  elsetrecslem  47698