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 206

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 207

This theorem is referenced by:  notbi  319  annotanannot  835  con3ALT  1084  xorbi12d  1521  equsexvw  2001  cbvexvw  2033  cbvexdvaw  2035  excomimw  2040  hbe1w  2045  19.8aw  2047  exexw  2048  ru0  2124  cbvexv1  2342  cbvex2v  2344  drex1v  2371  cbvex  2401  cbvex2  2414  drex1  2443  eujustALT  2569  necon3abid  2974  neleq12d  3048  rexbiOLD  3102  cbvrexdva  3237  cbvrexfw  3302  rexeqbidvvOLD  3334  cbvrexdva2  3346  cbvrexf  3358  cbvexeqsetf  3492  cgsex4gOLD  3526  ceqsex  3527  ceqsexv  3529  gencbval  3542  spcegf  3591  spc2gv  3599  spc2d  3601  spc3gv  3603  ceqsralbv  3656  cdeqnot  3776  rru  3787  ruOLD  3789  sbcng  3841  sbcrext  3881  cbvrexcsf  3953  difjust  3964  eldif  3972  dfpss3  4098  dfdif3OLD  4127  difeq2  4129  disjne  4460  pssdifcom1  4495  eldifpr  4662  rexsng  4680  elpwunsn  4688  eldiftp  4691  rexprg  4701  preqsnd  4863  disjxun  5145  nalset  5318  dtruALT2  5375  dtruALT  5393  rexxfrd  5414  rexxfr2d  5416  rexxfrd2  5418  rexxfr  5421  dtruOLD  5451  opthneg  5491  snopeqop  5515  otiunsndisj  5529  poeq1  5599  pocl  5604  swopo  5607  sotric  5625  sotrieq  5626  isso2i  5632  somo  5634  freq1  5655  frirr  5664  fr2nr  5665  frminex  5667  tz7.2  5671  wereu2  5685  poinxp  5768  frinxp  5770  posn  5773  frsn  5775  rexiunxp  5853  rexxpf  5860  intirr  6140  poirr2  6146  cnvpo  6308  dfpo2  6317  predpoirr  6355  predfrirr  6356  frpomin  6362  nordeq  6404  ordtri1  6418  ordtri3  6421  fvmpti  7014  fndmdif  7061  rexrnmptw  7114  rexrnmpt  7116  rexima  7257  2f1fvneq  7279  f1imapss  7285  f1ounsn  7291  cbvexfo  7309  nf1const  7323  soisoi  7347  isopolem  7364  weniso  7373  imaeqsalvOLD  7383  canth  7384  riotaclb  7428  rexrnmpo  7572  ndmovg  7615  sorpssuni  7750  sorpssint  7751  fr3nr  7790  dfwe2  7792  ordsucsssuc  7842  nlimsucg  7862  orduninsuc  7863  dfom2  7888  ssnlim  7906  f1oweALT  7995  frxp  8149  poxp  8151  frxp2  8167  frxp3  8174  xpord3inddlem  8177  soseq  8182  suppofssd  8226  suppcoss  8230  wfrlem10OLD  8356  smoword  8404  tz7.48lem  8479  oacan  8584  oaword  8585  omlimcl  8614  omeulem1  8618  nnaword  8663  nnmword  8669  nneob  8692  naddss1  8725  brdifun  8773  swoer  8774  undifixp  8972  boxcutc  8979  2dom  9068  php  9244  phpeqd  9249  nndomog  9250  phpOLD  9256  nndomogOLD  9260  onomeneq  9262  nnsdomo  9267  unxpdomlem2  9284  frfi  9318  unfilem1  9340  supeq3  9486  supeq123d  9487  supmo  9489  eqsup  9493  supub  9496  sup0  9503  suppr  9508  supisolem  9510  supisoex  9511  eqinf  9521  infval  9523  infmo  9532  infpr  9540  infempty  9544  oieq1  9549  ordtypecbv  9554  ordtypelem7  9561  wemapsolem  9587  canthwdom  9616  zfregcl  9631  elirrv  9633  elirr  9634  noinfep  9697  cantnfp1lem3  9717  ttrcltr  9753  rankr1clem  9857  carden2b  10004  domtri2  10026  alephord3  10115  alephdom2  10124  alephval3  10147  dfac9  10174  kmlem2  10189  kmlem4  10191  isfin4  10334  isfin7  10338  fin23lem11  10354  isf32lem5  10394  isf34lem4  10414  fin1a2lem6  10442  fin1a2lem7  10443  fin1a2lem12  10448  itunisuc  10456  ac6n  10522  zorn2g  10540  zornn0g  10542  ttukeylem7  10552  axpowndlem3  10636  axpowndlem4  10637  axregnd  10641  elgch  10659  engch  10665  fpwwe2lem12  10679  fpwwe2  10680  pwfseqlem1  10695  pwfseqlem3  10697  hargch  10710  addnidpi  10938  pinq  10964  nqereu  10966  ltsonq  11006  prlem934  11070  ltexprlem7  11079  addcanpr  11083  prlem936  11084  reclem2pr  11085  reclem3pr  11086  supexpr  11091  ltsosr  11131  supsrlem  11148  axpre-lttri  11202  axpre-sup  11206  xrlenlt  11323  axlttri  11329  axsup  11333  ltne  11355  dedekind  11421  readdcan  11432  leadd1  11728  ltsub1  11756  ltsub2  11757  leord1  11787  lediv1  12130  lemuldiv  12145  lerec  12148  le2msq  12165  infm3  12224  suprnub  12230  infregelb  12249  avgle1  12503  avgle2  12504  znnnlt1  12641  indstr  12955  zsupss  12976  uzsupss  12979  rpneg  13064  xralrple  13243  xleneg  13256  xltadd1  13294  xposdif  13300  xmulneg1  13307  xltmul1  13330  xrsupexmnf  13343  xrinfmexpnf  13344  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  supxrleub  13364  infxrgelb  13373  difreicc  13520  nn0disj  13680  nelfzo  13700  elfznelfzo  13807  fvinim0ffz  13821  injresinjlem  13822  ssnn0fi  14022  leexp2  14207  exp11nnd  14296  hashbnd  14371  hasheni  14383  hashfundm  14477  hashbc  14488  wrdsymb0  14583  swrdnd  14688  swrdnd2  14689  pfxnd0  14722  repswswrd  14818  repswccat  14820  cshwidxmod  14837  cnpart  15275  sqrtlt  15296  limsuplt  15511  rlimrege0  15611  isercoll  15700  efle  16150  odd2np1  16374  sumodd  16421  divalglem7  16432  ndvdsadd  16443  fldivndvdslt  16449  bitsfval  16456  bitsval  16457  bits0  16461  bitsp1  16464  bitsmod  16469  bitscmp  16471  bitsinv1lem  16474  sadadd2lem2  16483  saddisjlem  16497  bitsshft  16508  gcdneg  16555  algcvgblem  16610  lcmneg  16636  isprm3  16716  dvdsnprmd  16723  isprm5  16740  rpexp  16755  phiprmpw  16809  m1dvdsndvds  16831  pythagtrip  16867  pcgcd1  16910  prmpwdvds  16937  prmreclem2  16950  prmreclem3  16951  prmreclem5  16953  prmreclem6  16954  vdwlem6  17019  vdwnnlem2  17029  vdwnnlem3  17030  vdwnn  17031  prmlem0  17139  prmlem1a  17140  divsfval  17593  mrisval  17674  ismri  17675  ismri2dad  17681  cidpropd  17754  cat1lem  18149  plttr  18399  joinval  18434  meetval  18448  acsfiindd  18610  isnsgrp  18748  smndex1n0mnd  18937  mgm2nsgrplem2  18944  sgrp2nmndlem3  18950  symgpssefmnd  19427  symgfix2  19448  pmtrdifellem4  19511  psgnunilem1  19525  psgnunilem5  19526  psgnunilem2  19527  psgnunilem3  19528  pmtrsn  19551  sylow1lem3  19632  sylow2alem2  19650  efgsfo  19771  ablfac1eulem  20106  ablfac1eu  20107  pgpfac1lem1  20108  pgpfac1lem5  20113  nzrunit  20540  zrninitoringc  20692  islbs  21092  lbsind  21096  lbspss  21098  lbspropd  21115  lspsnne1  21136  islbs2  21173  lbsacsbs  21175  lbsextlem1  21177  lbsextlem3  21179  lbsextlem4  21180  lbsextg  21181  frlmlbs  21834  islindf  21849  islinds2  21850  islindf2  21851  lindfind  21853  lindsind  21854  lindfrn  21858  lindfmm  21864  lsslindf  21867  islindf4  21875  opsrtoslem2  22097  psdmul  22187  cply1coe0  22320  cply1coe0bi  22321  mdetunilem7  22639  mdetunilem8  22640  mdetunilem9  22641  maducoeval2  22661  pmatcollpw3fi1lem1  22807  fvmptnn04ifa  22871  fvmptnn04ifc  22873  fvmptnn04ifd  22874  chfacffsupp  22877  chfacfscmul0  22879  chfacfpmmul0  22883  elcls  23096  maxlp  23170  perfi  23178  ordtbaslem  23211  ordtval  23212  ordtbas2  23214  ordtopn1  23217  ordtopn2  23218  ordtcnv  23224  ordtrest  23225  ordtrest2lem  23226  ordtrest2  23227  pnfnei  23243  mnfnei  23244  isreg2  23400  ordthauslem  23406  cmpfi  23431  cmpfii  23432  bwth  23433  nconnsubb  23446  hausdiag  23668  txkgen  23675  kqdisj  23755  ordthmeolem  23824  fbfinnfr  23864  trfbas  23867  fbunfip  23892  fbasrn  23907  trfil3  23911  ufileu  23942  fin1aufil  23955  hausflim  24004  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  ptcmplem2  24076  ptcmplem3  24077  stdbdbl  24545  iccntr  24856  reconnlem2  24862  iccpnfcnv  24988  xrhmeo  24990  lebnumlem1  25006  lebnumlem2  25007  lebnumlem3  25008  bcthlem4  25374  minveclem3b  25475  ivthlem2  25500  ivthlem3  25501  mbfmax  25697  mbfposr  25700  i1fd  25729  mbfi1fseqlem4  25767  itg2splitlem  25797  itg2monolem1  25799  itg2cnlem1  25810  dvne0  26064  lhop1lem  26066  deg1nn0clb  26143  dgrle  26296  coemulhi  26307  aaliou3lem9  26406  cos11  26589  logleb  26659  argrege0  26667  logdivle  26678  ellogdm  26695  cxple  26751  cxplt2  26754  cxple3  26757  isosctrlem1  26875  atandm  26933  atans2  26988  atantayl2  26995  eldmgm  27079  ftalem7  27136  isppw2  27172  musum  27248  dchrsum2  27326  bposlem1  27342  lgsmod  27381  lgsdir2lem2  27384  lgsdir2  27388  lgsne0  27393  lgsprme0  27397  gausslemma2dlem4  27427  lgsquadlem1  27438  2lgslem3  27462  2lgsoddprm  27474  2sq2  27491  addsqrexnreu  27500  rpvmasumlem  27545  padicabv  27688  ostth3  27696  ostth  27697  noextenddif  27727  nodenselem4  27746  nodenselem5  27747  nodenselem7  27749  nolt02o  27754  nogt01o  27755  noresle  27756  nosupprefixmo  27759  noinfprefixmo  27760  nosupcbv  27761  nosupdm  27763  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd1  27773  nosupbnd2lem1  27774  nosupbnd2  27775  noinfcbv  27776  noinfdm  27778  noinffv  27780  noinfres  27781  noinfbnd1lem1  27782  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd1  27788  noinfbnd2lem1  27789  noinfbnd2  27790  slenlt  27811  sltne  27829  nocvxminlem  27836  slerec  27878  cuteq1  27892  newbday  27954  sltlpss  27959  cofcutr  27972  lrrecfr  27990  addsval  28009  sltadd2  28038  sleneg  28092  slesubsubbd  28130  slesubsub2bd  28131  slesubsub3bd  28132  slesubaddd  28137  sltmul2  28211  slemul2d  28214  slemul1d  28215  istrkgld  28481  axtgupdim2  28493  tglowdim2l  28672  axlowdimlem16  28986  axlowdim2  28989  axlowdim  28990  numedglnl  29175  usgredg2v  29258  lfuhgr1v0e  29285  cusgrfi  29490  vtxd0nedgb  29520  vtxduhgr0edgnel  29526  1loopgrnb0  29534  1hevtxdg0  29537  vtxdgoddnumeven  29585  wlkp1lem1  29705  wlkp1lem2  29706  wlkp1lem5  29709  crctcsh  29853  clwlkclwwlklem2a4  30025  eupth2eucrct  30245  eupth2lem3lem3  30258  eupth2lem3lem4  30259  eupth2lem3lem6  30261  eupth2lem3lem7  30262  eupth2lems  30266  eupth2  30267  konigsberglem4  30283  nfrgr2v  30300  frgrwopreglem3  30342  fusgr2wsp2nb  30362  frgrreggt1  30421  friendshipgt3  30426  lpni  30508  nmobndseqi  30807  minvecolem5  30909  chpsscon3  31531  chnle  31542  nonbooli  31679  pjnel  31754  specval  31926  nmcfnlbi  32080  stri  32285  hstri  32293  cvbr  32310  cvcon3  32312  chcv1  32383  cvexchlem  32396  chrelat2  32398  nelun  32540  elpreq  32555  nelpr  32556  ifeqeqx  32562  nfpconfp  32648  suppiniseg  32700  isoun  32716  suppss3  32741  xrge0infss  32770  infxrge0gelb  32776  eliccelico  32785  elicoelioo  32786  nndiffz1  32794  hashgt1  32817  expgt0b  32822  nn0min  32826  ccatws1f1o  32920  toslublem  32946  tosglblem  32948  pmtrcnel  33091  cycpmco2  33135  isarchi2  33174  archiabl  33187  elrgspnlem2  33232  elrgspnlem3  33233  0nellinds  33377  lindssn  33385  lindfpropd  33389  ssdifidlprm  33465  mxidlirred  33479  ssmxidl  33481  lbslsat  33643  lindsunlem  33651  rtelextdg2lem  33731  ordtcnvNEW  33880  ordtrestNEW  33881  ordtrest2NEWlem  33882  ordtrest2NEW  33883  ordtconnlem1  33884  xrge0iifcnv  33893  esumpcvgval  34058  esum2d  34073  ddemeas  34216  omssubadd  34281  oddpwdc  34335  eulerpartlems  34341  eulerpartlemf  34351  eulerpartlemt  34352  eulerpartlemr  34355  eulerpartlemgvv  34357  eulerpartlemn  34362  ballotlemfc0  34473  ballotlemfcc  34474  ballotlem4  34479  ballotlemimin  34486  ballotlem7  34516  plymulx  34541  signsply0  34544  reprinfz1  34615  reprpmtf1o  34619  reprdifc  34620  hgt750lema  34650  hgt750leme  34651  istrkg2d  34659  bnj23  34710  bnj1185  34785  bnj1228  35003  bnj1388  35025  bnj1417  35033  nummin  35083  axnulg  35084  revwlk  35108  isacycgr  35129  acycgr0v  35132  prclisacycgr  35135  erdszelem10  35184  satf0n0  35362  fmlaomn0  35374  fmlasucdisj  35383  satfv1fvfmla1  35407  satefvfmla1  35409  ismfs  35533  mvtinf  35539  untelirr  35687  untsucf  35689  untangtr  35693  dfon2lem3  35766  dfon2lem4  35767  dfon2lem7  35770  dfon2lem9  35772  distel  35784  funpartfv  35926  dfrdg4  35932  nn0prpwlem  36304  nn0prpw  36305  limsucncmpi  36427  limsucncmp  36428  ordcmp  36429  weiunlem2  36445  weiunfrlem  36446  weiunfr  36449  unblimceq0  36489  unbdqndv1  36490  bj-hbntbi  36686  bj-equsexvwd  36763  bj-cbvexdv  36782  bj-ru1  36925  bj-nuliota  37039  topdifinffinlem  37329  topdifinffin  37330  icorempo  37333  relowlpssretop  37346  finxpreclem2  37372  finxpreclem6  37378  wl-issetft  37562  wl-ax11-lem8  37572  leceifl  37595  lindsadd  37599  lindsenlbs  37601  matunitlindflem1  37602  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem21  37627  poimirlem23  37629  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem31  37637  poimir  37639  mblfinlem2  37644  mblfinlem3  37645  ismblfin  37647  cnambfre  37654  itg2addnclem  37657  itg2addnclem2  37658  iblabsnclem  37669  ftc1anclem1  37679  areacirc  37699  heibor1lem  37795  heiborlem1  37797  heiborlem6  37802  heiborlem8  37804  heiborlem10  37806  smprngopr  38038  ecin0  38333  ax12inda  38929  riotaclbgBAD  38935  lcvfbr  39001  lcvbr  39002  lsatcv0  39012  l1cvpat  39035  opltcon3b  39185  cvrfval  39249  cvrval  39250  cvrnbtwn  39252  cvrval2  39255  cvrnbtwn2  39256  cvrnbtwn3  39257  cvrcon3b  39258  cvrnbtwn4  39260  atnlt  39294  iscvlat  39304  cvlexch1  39309  hlsuprexch  39363  hlrelat5N  39383  hlrelat2  39385  cvrval5  39397  3dimlem1  39440  3dim1lem5  39448  3dim2  39450  3dim3  39451  llnnlt  39505  islpln5  39517  lplni2  39519  lvolex3N  39520  lplnnle2at  39523  islpln2a  39530  lplnribN  39533  lplnexllnN  39546  lplnnlt  39547  lvoli3  39559  islvol5  39561  lvoli2  39563  lvolnle3at  39564  islvol2aN  39574  4atlem11  39591  lvolnltN  39600  dalawlem15  39867  4atexlemex2  40053  4atex  40058  4atex2-0aOLDN  40060  4atex2-0cOLDN  40062  lautcvr  40074  ltrnfset  40099  ltrnset  40100  ltrnu  40103  trlfset  40142  trlset  40143  trlval2  40145  cdlemd6  40185  cdleme0nex  40272  cdleme18d  40277  cdleme25b  40336  cdleme25cv  40340  cdleme29b  40357  cdleme31fv  40372  cdleme31fv2  40375  cdlemefrs29bpre0  40378  cdlemefr32sn2aw  40386  cdlemefr29bpre0N  40388  cdlemefr29clN  40389  cdlemefr32fvaN  40391  cdlemefr32fva1  40392  cdlemefs32sn1aw  40396  cdleme32fva  40419  cdleme32fvaw  40421  cdleme40v  40451  cdleme42b  40460  cdleme46f2g2  40475  cdleme46f2g1  40476  cdleme48gfv  40519  cdlemg1fvawlemN  40555  cdlemg1cex  40570  cdlemg6d  40603  cdlemm10N  41100  dicffval  41156  dicfval  41157  dicval  41158  dicfnN  41165  dicvalrelN  41167  dihffval  41212  dihfval  41213  dihlsscpre  41216  dvh4dimat  41420  dvh3dimatN  41421  dvh4dimlem  41425  dvh3dim  41428  dvh4dimN  41429  dvh3dim2  41430  dvh3dim3N  41431  mapdcv  41642  mapdh9aOLDN  41772  hdmapfval  41809  hdmapval  41810  hdmapval2  41814  hdmap11lem2  41824  dvrelog2b  42047  aks4d1p4  42060  aks4d1p5  42061  aks4d1p7  42064  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1  42070  aks6d1c2p2  42100  hashnexinj  42109  rspcsbnea  42112  aks6d1c5  42120  aks6d1c6lem3  42153  aks6d1c7  42165  metakunt27  42212  metakunt28  42213  metakunt29  42214  supinf  42261  oexpreposd  42335  flt4lem7  42645  nna4b4nsq  42646  ellz1  42754  rencldnfilem  42807  jm2.22  42983  jm2.23  42984  wepwsolem  43030  fnwe2lem2  43039  aomclem8  43049  unxpwdom3  43083  onsupmaxb  43227  onexlimgt  43231  onsupeqnmax  43235  onov0suclim  43263  oaordnr  43285  omnord1  43294  oenord1  43305  oaomoencom  43306  oenass  43308  cantnfresb  43313  tfsnfin  43341  ralopabb  43400  nlimsuc  43430  ifpbi12  43477  dfsucon  43512  sqrtcvallem1  43620  ss2iundf  43648  frege124d  43750  clsk3nimkb  44029  clsk1indlem1  44034  clsk1independent  44035  ntrneineine1lem  44073  ntrneicls11  44079  clsneiel1  44097  clsneiel2  44098  neicvgel1  44108  neicvgel2  44109  radcnvrat  44309  rusbcALT  44434  en3lpVD  44842  eliin2f  45043  nssd  45044  wessf1ornlem  45127  rexanuz2nf  45442  limsupre2lem  45679  icccncfext  45842  stoweidlem14  45969  stoweidlem34  45989  stoweidlem59  46014  etransclem24  46213  nnfoctbdjlem  46410  nnfoctbdj  46411  hspmbllem2  46582  nsssmfmbflem  46733  fsetsnprcnex  47004  eu2ndop1stv  47074  afvfv0bi  47101  afvco2  47125  ndmaovg  47133  ndfatafv2nrn  47170  afv2ndefb  47173  afv2fv0  47214  nelbr  47223  otiunsndisjX  47228  fun2dmnopgexmpl  47233  ltnltne  47248  readdcnnred  47252  resubcnnred  47253  recnmulnred  47254  cndivrenred  47255  ichnreuop  47396  fmtnoinf  47460  odz2prm2pw  47487  prmdvdsfmtnof1lem2  47509  lighneallem3  47531  lighneallem4  47534  requad1  47546  isodd3  47576  bits0ALTV  47603  nfermltl8rev  47666  nfermltl2rev  47667  nfermltlrev  47668  isubgr3stgrlem3  47870  usgrexmpl12ngric  47932  lidldomnnring  48079  ztprmneprm  48191  lindepsnlininds  48297  islindeps  48298  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  difmodm1lt  48371  line2ylem  48600  line2xlem  48602  map0cor  48684  elsetrecslem  48929