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 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbi  322  annotanannot  848  con3ALT  1101  xorbi12d  1555  equsexvw  2040  cbvexvw  2072  cbvexdvaw  2074  excomimw  2079  hbe1w  2085  19.8aw  2087  exexw  2088  ru0  2166  cbvexv1  2375  cbvex2v  2377  drex1v  2402  cbvex  2431  cbvex2  2444  drex1  2473  eujustALT  2600  necon3abid  2995  neleq12d  3070  cbvrexdva  3247  cbvrexfw  3307  cbvrexdva2  3341  cbvrexf  3350  cbvexeqsetf  3469  ceqsex  3501  ceqsexv  3502  gencbval  3512  spcegf  3550  spc2gv  3558  spc2d  3560  spc3gv  3562  ceqsralbv  3614  cdeqnot  3729  rru  3740  sbcng  3789  sbcrext  3824  cbvrexcsf  3894  dfpss3  4019  difjust  4049  eldif  4052  difeq2  4060  disjne  4411  pssdifcom1  4448  eldifpr  4619  rexsng  4637  elpwunsn  4645  eldiftp  4648  rexprg  4658  preqsnd  4817  disjxun  5104  exnelv  5270  nalsetOLD  5272  dtruALT2  5336  dtruALT  5354  rexxfrd  5375  rexxfr2d  5377  rexxfrd2  5379  rexxfr  5382  opthneg  5454  snopeqop  5482  otiunsndisj  5497  poeq1  5566  pocl  5571  swopo  5574  sotric  5593  sotrieq  5594  isso2i  5600  somo  5602  freq1  5622  frirr  5631  fr2nr  5632  frminex  5634  tz7.2  5638  wereu2  5652  poinxp  5737  frinxp  5739  posn  5742  frsn  5744  rexiunxp  5822  rexxpf  5830  intirr  6123  poirr2  6129  cnvpo  6305  dfpo2  6314  predpoirr  6351  predfrirr  6352  frpomin  6358  nordeq  6396  ordtri1  6411  ordtri3  6414  fvmpti  7012  fndmdif  7061  rexrnmptw  7116  rexrnmpt  7118  rexima  7264  f1imapss  7290  f1ounsn  7300  cbvexfo  7318  nf1const  7332  soisoi  7356  isopolem  7373  weniso  7384  canth  7394  riotaclb  7438  rexrnmpo  7581  ndmovg  7625  sorpssuni  7769  sorpssint  7770  fr3nr  7807  dfwe2  7809  ordsucsssuc  7855  nlimsucg  7874  orduninsuc  7875  dfom2  7900  ssnlim  7918  resf1extb  7967  f1oweALT  8005  frxp  8162  poxp  8164  fnwe2lem3  8171  frxp2  8185  frxp3  8192  xpord3inddlem  8195  soseq  8200  suppofssd  8245  suppcoss  8249  smoword  8399  tz7.48lemOLD  8476  oacan  8581  oaword  8582  omlimcl  8611  omeulem1  8615  nnaword  8661  nnmword  8667  nneob  8690  naddss1  8724  brdifun  8773  swoer  8774  undifixp  8987  boxcutc  8994  2dom  9083  php  9247  phpeqd  9252  nndomog  9253  onomeneq  9254  nnsdomo  9259  unxpdomlem2  9273  frfi  9301  unfilem1  9322  tfsnfin2  9377  supeq3  9465  supeq123d  9466  supmo  9468  eqsup  9472  supub  9475  sup0  9483  suppr  9488  supisolem  9490  supisoex  9491  eqinf  9501  infval  9503  infmo  9513  infpr  9521  infempty  9525  oieq1  9530  ordtypecbv  9535  ordtypelem7  9542  wemapsolem  9568  canthwdom  9597  zfregcl  9612  zfregclOLD  9613  elirrv  9615  elirrvOLD  9616  elirrvOLDOLD  9617  elirr  9618  noinfep  9685  cantnfp1lem3  9705  ttrcltr  9741  rankr1clem  9853  carden2b  10072  domtri2  10094  alephord3  10181  alephdom2  10190  alephval3  10213  dfac9  10239  kmlem2  10254  kmlem4  10256  isfin4  10399  isfin7  10403  fin23lem11  10419  isf32lem5  10459  isf34lem4  10479  fin1a2lem6  10507  fin1a2lem7  10508  fin1a2lem12  10513  itunisuc  10521  ac6n  10587  zorn2g  10605  zornn0g  10607  ttukeylem7  10617  infinfg  10674  axpowndlem3  10708  axpowndlem4  10709  axregnd  10713  elgch  10731  engch  10737  fpwwe2lem12  10751  fpwwe2  10752  pwfseqlem1  10767  pwfseqlem3  10769  hargch  10782  addnidpi  11010  pinq  11036  nqereu  11038  ltsonq  11078  prlem934  11142  ltexprlem7  11151  addcanpr  11155  prlem936  11156  reclem2pr  11157  reclem3pr  11158  supexpr  11163  ltsosr  11203  supsrlem  11220  axpre-lttri  11274  axpre-sup  11278  xrlenlt  11398  axlttri  11405  axsup  11409  ltne  11431  dedekind  11497  readdcan  11508  leadd1  11808  ltsub1  11836  ltsub2  11837  leord1  11867  lediv1  12206  lemuldiv  12221  lerec  12224  le2msq  12241  infm3  12300  suprnub  12306  infregelb  12325  avgle1  12610  avgle2  12611  znnnlt1  12747  indstr  13067  zsupss  13088  uzsupss  13091  rpneg  13178  xralrple  13359  xleneg  13372  xltadd1  13410  xposdif  13416  xmulneg1  13423  xltmul1  13446  xrsupexmnf  13459  xrinfmexpnf  13460  xrsupsslem  13461  xrinfmsslem  13462  xrub  13466  supxrleub  13480  infxrgelb  13490  difreicc  13639  nn0disj  13802  nelfzo  13823  elfznelfzo  13932  fvinim0ffz  13948  injresinjlem  13949  ssnn0fi  14152  leexp2  14338  exp11nnd  14429  hashbnd  14504  hasheni  14516  hashfundm  14611  hashbc  14622  wrdsymb0  14718  swrdnd  14829  swrdnd2  14830  pfxnd0  14863  repswswrd  14960  repswccat  14962  cshwidxmod  14979  cnpart  15433  sqrtlt  15454  limsuplt  15672  rlimrege0  15772  isercoll  15861  efle  16312  odd2np1  16537  sumodd  16584  divalglem7  16595  ndvdsadd  16606  fldivndvdslt  16612  bitsfval  16619  bitsval  16620  bits0  16624  bitsp1  16627  bitsmod  16632  bitscmp  16634  bitsinv1lem  16637  sadadd2lem2  16646  saddisjlem  16660  bitsshft  16671  gcdneg  16720  algcvgblem  16778  lcmneg  16804  isprm3  16884  dvdsnprmd  16891  isprm5  16909  rpexp  16924  phiprmpw  16979  m1dvdsndvds  17002  pythagtrip  17038  pcgcd1  17081  prmpwdvds  17108  prmreclem2  17121  prmreclem3  17122  prmreclem5  17124  prmreclem6  17125  vdwlem6  17190  vdwnnlem2  17200  vdwnnlem3  17201  vdwnn  17202  prmlem0  17309  prmlem1a  17310  divsfval  17745  mrisval  17830  ismri  17831  ismri2dad  17837  cidpropd  17910  cat1lem  18297  plttr  18540  joinval  18575  meetval  18589  acsfiindd  18753  isnsgrp  18938  smndex1n0mnd  19137  mgm2nsgrplem2  19144  sgrp2nmndlem3  19150  degenmgm2nfun  19165  symgpssefmnd  19637  symgfix2  19657  pmtrdifellem4  19720  psgnunilem1  19734  psgnunilem5  19735  psgnunilem2  19736  psgnunilem3  19737  pmtrsn  19760  sylow1lem3  19841  sylow2alem2  19859  efgsfo  19980  ablfac1eulem  20315  ablfac1eu  20316  pgpfac1lem1  20317  pgpfac1lem5  20322  nzrunit  20802  zrninitoringc  20955  islbs  21378  lbsind  21382  lbspss  21384  lbspropd  21401  lspsnne1  21422  islbs2  21459  lbsacsbs  21461  lbsextlem1  21463  lbsextlem3  21465  lbsextlem4  21466  lbsextg  21467  ssdifidlprm  21669  frlmlbs  22130  islindf  22145  islinds2  22146  islindf2  22147  lindfind  22149  lindsind  22150  lindfrn  22154  lindfmm  22160  lsslindf  22163  islindf4  22171  lindsenlbs  22184  opsrtoslem2  22392  psdmul  22514  cply1coe0  22646  cply1coe0bi  22647  mdetunilem7  22960  mdetunilem8  22961  mdetunilem9  22962  maducoeval2  22982  matunitlindflem1  23021  pmatcollpw3fi1lem1  23131  fvmptnn04ifa  23195  fvmptnn04ifc  23197  fvmptnn04ifd  23198  chfacffsupp  23201  chfacfscmul0  23203  chfacfpmmul0  23207  elcls  23418  maxlp  23492  perfi  23500  ordtbaslem  23533  ordtval  23534  ordtbas2  23536  ordtopn1  23539  ordtopn2  23540  ordtcnv  23546  ordtrest  23547  ordtrest2lem  23548  ordtrest2  23549  pnfnei  23565  mnfnei  23566  isreg2  23722  ordthauslem  23728  cmpfi  23753  cmpfii  23754  bwth  23755  nconnsubb  23768  hausdiag  23991  txkgen  23998  kqdisj  24078  ordthmeolem  24147  fbfinnfr  24187  trfbas  24190  fbunfip  24215  fbasrn  24230  trfil3  24234  ufileu  24265  fin1aufil  24278  hausflim  24327  alexsubALTlem2  24394  alexsubALTlem3  24395  alexsubALTlem4  24396  ptcmplem2  24399  ptcmplem3  24400  stdbdbl  24863  iccntr  25168  reconnlem2  25174  iccpnfcnv  25292  xrhmeo  25294  lebnumlem1  25309  lebnumlem2  25310  lebnumlem3  25311  bcthlem4  25675  minveclem3b  25776  ivthlem2  25800  ivthlem3  25801  mbfmax  25997  mbfposr  26000  i1fd  26029  mbfi1fseqlem4  26066  itg2splitlem  26096  itg2monolem1  26098  itg2cnlem1  26109  dvne0  26358  lhop1lem  26360  deg1nn0clb  26435  dgrle  26589  coemulhi  26600  plymulidp  26630  aaliou3lem9  26704  cos11  26888  logleb  26958  argrege0  26966  logdivle  26977  ellogdm  26994  cxple  27050  cxplt2  27053  cxple3  27056  isosctrlem1  27173  atandm  27231  atans2  27286  atantayl2  27293  eldmgm  27376  ftalem7  27433  isppw2  27469  musum  27545  dchrsum2  27622  bposlem1  27638  lgsmod  27677  lgsdir2lem2  27680  lgsdir2  27684  lgsne0  27689  lgsprme0  27693  gausslemma2dlem4  27723  lgsquadlem1  27734  2lgslem3  27758  2lgsoddprm  27770  2sq2  27787  addsqrexnreu  27796  rpvmasumlem  27841  padicabv  27984  ostth3  27992  ostth  27993  flt4lem7  28016  nna4b4nsq  28017  noextenddif  28052  nodenselem4  28071  nodenselem5  28072  nodenselem7  28074  nolt02o  28079  nogt01o  28080  noresle  28081  nosupprefixmo  28084  noinfprefixmo  28085  nosupcbv  28086  nosupdm  28088  nosupfv  28090  nosupres  28091  nosupbnd1lem1  28092  nosupbnd1lem3  28094  nosupbnd1lem5  28096  nosupbnd1  28098  nosupbnd2lem1  28099  nosupbnd2  28100  noinfcbv  28101  noinfdm  28103  noinffv  28105  noinfres  28106  noinfbnd1lem1  28107  noinfbnd1lem3  28109  noinfbnd1lem5  28111  noinfbnd1  28113  noinfbnd2lem1  28114  noinfbnd2  28115  lenlts  28136  ltsne  28158  nocvxminlem  28167  lesrec  28212  eqcuts3  28217  cuteq1  28230  newbday  28315  ltslpss  28321  cofcutr  28337  lrrecfr  28356  addsval  28375  ltadds2  28404  lenegs  28459  lesubsubsbd  28499  lesubsubs2bd  28500  lesubsubs3bd  28501  lesubaddsd  28506  ltmuls2  28584  lemuls2d  28587  lemuls1d  28588  oncutlt  28677  onles  28681  pw2cut2  28875  bdaypw2bnd  28878  bdayfinbndlem1  28880  istrkgld  28948  axtgupdim2  28960  tglowdim2l  29146  axlowdimlem16  29562  axlowdim2  29565  axlowdim  29566  numedglnl  29749  usgredg2v  29835  lfuhgr1v0e  29862  cusgrfi  30066  vtxd0nedgb  30096  vtxduhgr0edgnel  30102  1loopgrnb0  30110  1hevtxdg0  30113  vtxdgoddnumeven  30161  wlkp1lem1  30279  wlkp1lem2  30280  wlkp1lem5  30283  revwlk  30294  dfpth2  30341  crctcsh  30440  clwlkclwwlklem2a4  30615  isacycgr  30778  eupth2eucrct  30845  eupth2lem3lem3  30858  eupth2lem3lem4  30859  eupth2lem3lem6  30861  eupth2lem3lem7  30862  eupth2lems  30866  eupth2  30867  konigsberglem4  30883  nfrgr2v  30900  frgrwopreglem3  30942  fusgr2wsp2nb  30962  frgrreggt1  31021  friendshipgt3  31026  lpni  31109  nmobndseqi  31408  minvecolem5  31510  chpsscon3  32132  chnle  32143  nonbooli  32280  pjnel  32355  specval  32527  nmcfnlbi  32681  stri  32886  hstri  32894  cvbr  32911  cvcon3  32913  chcv1  32984  cvexchlem  32997  chrelat2  32999  nelun  33178  elpreq  33193  nelpr  33196  ifeqeqx  33207  nfpconfp  33295  suppiniseg  33347  isoun  33363  suppss3  33382  xrge0infss  33419  infxrge0gelb  33425  eliccelico  33436  elicoelioo  33437  nndiffz1  33445  hashgt1  33467  expgt0b  33475  nn0min  33479  ccatws1f1o  33581  toslublem  33600  tosglblem  33602  pmtrcnel  33717  cycpmco2  33761  isarchi2  33813  archiabl  33826  elrgspnlem2  33871  elrgspnlem3  33872  0nellinds  33993  lindssn  34000  lindfpropd  34004  mxidlirred  34064  ssmxidl  34066  dflringlem  34093  esplyind  34274  lbslsat  34315  lindsunlem  34323  rtelextdg2lem  34425  constrsqrtcl  34478  ordtcnvNEW  34619  ordtrestNEW  34620  ordtrest2NEWlem  34621  ordtrest2NEW  34622  ordtconnlem1  34623  xrge0iifcnv  34632  esumpcvgval  34777  esum2d  34792  ddemeas  34936  omssubadd  34999  oddpwdc  35053  eulerpartlems  35059  eulerpartlemf  35069  eulerpartlemt  35070  eulerpartlemr  35073  eulerpartlemgvv  35075  eulerpartlemn  35080  ballotlemfc0  35192  ballotlemfcc  35193  ballotlem4  35198  ballotlemimin  35205  ballotlem7  35235  signsply0  35247  reprinfz1  35318  reprpmtf1o  35322  reprdifc  35323  hgt750lema  35353  hgt750leme  35354  istrkg2d  35362  bnj23  35416  bnj1185  35490  bnj1228  35708  bnj1388  35730  bnj1417  35738  ordtypeon  35799  nummin  35803  axprALT2  35815  ecscottd  35843  infinfnum  35848  fineqvnttrclselem1  35888  axnulg  35912  jltaleph  36025  onvf1odlem2  36031  onvf1odlem3  36032  acycgr0v  36069  prclisacycgr  36072  erdszelem10  36131  satf0n0  36309  fmlaomn0  36321  fmlasucdisj  36330  satfv1fvfmla1  36354  satefvfmla1  36356  ismfs  36480  mvtinf  36486  mirimanoffr  36626  mirimanofffr  36628  elpssmo  36635  untelirr  36650  untsucf  36652  untangtr  36656  dfon2lem3  36724  dfon2lem4  36725  dfon2lem7  36728  dfon2lem9  36730  distel  36742  funpartfv  36886  dfrdg4  36892  nmulprop  37116  naddle  37145  nn0prpwlem  37287  nn0prpw  37288  limsucncmpi  37410  limsucncmp  37411  ordcmp  37412  weiunlem  37428  weiunfrlem  37429  weiunfr  37432  axtcond  37443  regsfromregtco  37503  regsfromsetind  37504  unblimceq0  37550  unbdqndv1  37551  bj-hbntbi  37783  bj-equsexvwd  37852  bj-cbvexdv  37889  bj-ru1  38033  bj-nuliota  38162  topdifinffinlem  38461  topdifinffin  38462  icorempo  38465  relowlpssretop  38478  finxpreclem2  38504  finxpreclem6  38510  wl-issetft  38705  wl-eujustlem1  38711  leceifl  38723  lindsadd  38727  poimirlem16  38745  poimirlem17  38746  poimirlem18  38747  poimirlem19  38748  poimirlem21  38750  poimirlem23  38752  poimirlem26  38755  poimirlem27  38756  poimirlem28  38757  poimirlem31  38760  poimir  38762  mblfinlem2  38767  mblfinlem3  38768  ismblfin  38770  cnambfre  38777  itg2addnclem  38780  itg2addnclem2  38781  iblabsnclem  38792  ftc1anclem1  38802  areacirc  38822  heibor1lem  38934  heiborlem1  38936  heiborlem6  38941  heiborlem8  38943  heiborlem10  38945  smprngopr  39177  ecin0  39475  ax12inda  40196  riotaclbgBAD  40202  lcvfbr  40268  lcvbr  40269  lsatcv0  40279  l1cvpat  40302  opltcon3b  40452  cvrfval  40516  cvrval  40517  cvrnbtwn  40519  cvrval2  40522  cvrnbtwn2  40523  cvrnbtwn3  40524  cvrcon3b  40525  cvrnbtwn4  40527  atnlt  40561  iscvlat  40571  cvlexch1  40576  hlsuprexch  40629  hlrelat5N  40649  hlrelat2  40651  cvrval5  40663  3dimlem1  40706  3dim1lem5  40714  3dim2  40716  3dim3  40717  llnnlt  40771  islpln5  40783  lplni2  40785  lvolex3N  40786  lplnnle2at  40789  islpln2a  40796  lplnribN  40799  lplnexllnN  40812  lplnnlt  40813  lvoli3  40825  islvol5  40827  lvoli2  40829  lvolnle3at  40830  islvol2aN  40840  4atlem11  40857  lvolnltN  40866  dalawlem15  41133  4atexlemex2  41319  4atex  41324  4atex2-0aOLDN  41326  4atex2-0cOLDN  41328  lautcvr  41340  ltrnfset  41365  ltrnset  41366  ltrnu  41369  trlfset  41408  trlset  41409  trlval2  41411  cdlemd6  41451  cdleme0nex  41538  cdleme18d  41543  cdleme25b  41602  cdleme25cv  41606  cdleme29b  41623  cdleme31fv  41638  cdleme31fv2  41641  cdlemefrs29bpre0  41644  cdlemefr32sn2aw  41652  cdlemefr29bpre0N  41654  cdlemefr29clN  41655  cdlemefr32fvaN  41657  cdlemefr32fva1  41658  cdlemefs32sn1aw  41662  cdleme32fva  41685  cdleme32fvaw  41687  cdleme40v  41717  cdleme42b  41726  cdleme46f2g2  41741  cdleme46f2g1  41742  cdleme48gfv  41785  cdlemg1fvawlemN  41821  cdlemg1cex  41836  cdlemg6d  41869  cdlemm10N  42366  dicffval  42422  dicfval  42423  dicval  42424  dicfnN  42431  dicvalrelN  42433  dihffval  42478  dihfval  42479  dihlsscpre  42482  dvh4dimat  42686  dvh3dimatN  42687  dvh4dimlem  42691  dvh3dim  42694  dvh4dimN  42695  dvh3dim2  42696  dvh3dim3N  42697  mapdcv  42908  mapdh9aOLDN  43038  hdmapfval  43075  hdmapval  43076  hdmapval2  43080  hdmap11lem2  43090  dvrelog2b  43307  aks4d1p4  43320  aks4d1p5  43321  aks4d1p7  43324  aks4d1p8d2  43326  aks4d1p8  43328  aks4d1  43330  aks6d1c2p2  43360  hashnexinj  43369  rspcsbnea  43372  aks6d1c5  43380  aks6d1c6lem3  43413  aks6d1c7  43425  supinf  43484  oexpreposd  43570  mullt0b2d  43739  ellz1  43969  rencldnfilem  44018  jm2.22  44193  jm2.23  44194  wepwsolem  44240  aomclem8  44254  unxpwdom3  44288  onsupmaxb  44431  onexlimgt  44435  onsupeqnmax  44439  onov0suclim  44466  oaordnr  44488  omnord1  44497  oenord1  44508  oaomoencom  44509  oenass  44511  cantnfresb  44516  tfsnfin  44544  ralopabb  44602  nlimsuc  44632  ifpbi12  44679  dfsucon  44714  sqrtcvallem1  44821  ss2iundf  44849  frege124d  44951  clsk3nimkb  45230  clsk1indlem1  45235  clsk1independent  45236  ntrneineine1lem  45274  ntrneicls11  45280  clsneiel1  45298  clsneiel2  45299  neicvgel1  45309  neicvgel2  45310  radcnvrat  45488  rusbcALT  45611  en3lpVD  46016  0elaxnul  46166  omssaxinf2  46171  permaxnul  46191  permaxinf2lem  46195  nregmodel  46200  eliin2f  46322  nssd  46323  wessf1ornlem  46403  rexanuz2nf  46705  limsupre2lem  46937  icccncfext  47100  stoweidlem14  47227  stoweidlem34  47247  stoweidlem59  47272  etransclem24  47471  nnfoctbdjlem  47668  nnfoctbdj  47669  hspmbllem2  47840  nsssmfmbflem  47991  fsetsnprcnex  48328  eu2ndop1stv  48398  afvfv0bi  48425  afvco2  48449  ndmaovg  48457  ndfatafv2nrn  48494  afv2ndefb  48497  afv2fv0  48538  nelbr  48547  otiunsndisjX  48552  fun2dmnopgexmpl  48557  ltnltne  48572  readdcnnred  48576  resubcnnred  48577  recnmulnred  48578  cndivrenred  48579  ichnreuop  48757  nprmmul1  48812  fmtnoinf  48824  odz2prm2pw  48851  prmdvdsfmtnof1lem2  48873  lighneallem3  48895  lighneallem4  48898  requad1  48923  isodd3  48953  bits0ALTV  48980  nfermltl8rev  49043  nfermltl2rev  49044  nfermltlrev  49045  upgrimpths  49210  isubgr3stgrlem3  49269  usgrexmpl12ngric  49339  pgnbgreunbgrlem2lem1  49415  pgnbgreunbgrlem2lem2  49416  pgnbgreunbgrlem2lem3  49417  pgnbgreunbgrlem5lem1  49421  pgnbgreunbgrlem5lem2  49422  pgnbgreunbgrlem5lem3  49423  lgricngricex  49430  lidldomnnring  49536  smprngprmrng  49639  ztprmneprm  49662  lindepsnlininds  49767  islindeps  49768  lindslinindsimp2lem5  49777  lindslinindsimp2  49778  line2ylem  50066  line2xlem  50068  map0cor  50169  nelsubc3lem  50387  fulltermc2  50850  setc1onsubc  50943  cnelsubcw  50944  elsetrecslem  51070