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  847  con3ALT  1100  xorbi12d  1554  equsexvw  2034  cbvexvw  2066  cbvexdvaw  2068  excomimw  2073  hbe1w  2079  19.8aw  2081  exexw  2082  ru0  2161  cbvexv1  2373  cbvex2v  2375  drex1v  2401  cbvex  2430  cbvex2  2443  drex1  2472  eujustALT  2599  necon3abid  2993  neleq12d  3068  cbvrexdva  3245  cbvrexfw  3305  cbvrexdva2  3340  cbvrexf  3349  cbvexeqsetf  3469  ceqsex  3501  ceqsexv  3502  gencbval  3512  spcegf  3550  spc2gv  3558  spc2d  3560  spc3gv  3562  ceqsralbv  3615  cdeqnot  3730  rru  3741  sbcng  3790  sbcrext  3825  cbvrexcsf  3895  difjust  3906  eldif  3914  dfpss3  4042  dfdif3OLD  4072  difeq2  4074  disjne  4414  pssdifcom1  4449  eldifpr  4623  rexsng  4641  elpwunsn  4649  eldiftp  4652  rexprg  4662  preqsnd  4823  disjxun  5106  exnelv  5275  nalsetOLD  5277  dtruALT2  5340  dtruALT  5358  rexxfrd  5379  rexxfr2d  5381  rexxfrd2  5383  rexxfr  5386  opthneg  5462  snopeqop  5488  otiunsndisj  5502  poeq1  5571  pocl  5576  swopo  5579  sotric  5598  sotrieq  5599  isso2i  5605  somo  5607  freq1  5627  frirr  5636  fr2nr  5637  frminex  5639  tz7.2  5643  wereu2  5657  poinxp  5741  frinxp  5743  posn  5746  frsn  5748  rexiunxp  5825  rexxpf  5832  intirr  6117  poirr2  6123  cnvpo  6288  dfpo2  6297  predpoirr  6334  predfrirr  6335  frpomin  6341  nordeq  6379  ordtri1  6394  ordtri3  6397  fvmpti  6988  fndmdif  7037  rexrnmptw  7090  rexrnmpt  7092  rexima  7236  f1imapss  7264  f1ounsn  7270  cbvexfo  7288  nf1const  7302  soisoi  7326  isopolem  7343  weniso  7354  imaeqsalvOLD  7364  canth  7366  riotaclb  7410  rexrnmpo  7552  ndmovg  7595  sorpssuni  7731  sorpssint  7732  fr3nr  7769  dfwe2  7771  ordsucsssuc  7817  nlimsucg  7836  orduninsuc  7837  dfom2  7862  ssnlim  7880  resf1extb  7929  f1oweALT  7967  frxp  8120  poxp  8122  frxp2  8138  frxp3  8145  xpord3inddlem  8148  soseq  8153  suppofssd  8197  suppcoss  8201  smoword  8351  tz7.48lem  8426  oacan  8531  oaword  8532  omlimcl  8561  omeulem1  8565  nnaword  8611  nnmword  8617  nneob  8640  naddss1  8674  brdifun  8723  swoer  8724  undifixp  8930  boxcutc  8937  2dom  9025  php  9189  phpeqd  9194  nndomog  9195  onomeneq  9196  nnsdomo  9201  unxpdomlem2  9215  frfi  9243  unfilem1  9263  tfsnfin2  9318  supeq3  9407  supeq123d  9408  supmo  9410  eqsup  9414  supub  9417  sup0  9425  suppr  9430  supisolem  9432  supisoex  9433  eqinf  9443  infval  9445  infmo  9455  infpr  9463  infempty  9467  oieq1  9472  ordtypecbv  9477  ordtypelem7  9484  wemapsolem  9510  canthwdom  9539  zfregcl  9554  zfregclOLD  9555  elirrv  9557  elirrvOLD  9558  elirrvOLDOLD  9559  elirr  9560  noinfep  9627  cantnfp1lem3  9647  ttrcltr  9683  rankr1clem  9790  carden2b  9960  domtri2  9982  alephord3  10069  alephdom2  10078  alephval3  10101  dfac9  10127  kmlem2  10142  kmlem4  10144  isfin4  10287  isfin7  10291  fin23lem11  10307  isf32lem5  10347  isf34lem4  10367  fin1a2lem6  10395  fin1a2lem7  10396  fin1a2lem12  10401  itunisuc  10409  ac6n  10475  zorn2g  10493  zornn0g  10495  ttukeylem7  10505  infinfg  10556  axpowndlem3  10590  axpowndlem4  10591  axregnd  10595  elgch  10613  engch  10619  fpwwe2lem12  10633  fpwwe2  10634  pwfseqlem1  10649  pwfseqlem3  10651  hargch  10664  addnidpi  10892  pinq  10918  nqereu  10920  ltsonq  10960  prlem934  11024  ltexprlem7  11033  addcanpr  11037  prlem936  11038  reclem2pr  11039  reclem3pr  11040  supexpr  11045  ltsosr  11085  supsrlem  11102  axpre-lttri  11156  axpre-sup  11160  xrlenlt  11280  axlttri  11287  axsup  11291  ltne  11313  dedekind  11379  readdcan  11390  leadd1  11688  ltsub1  11716  ltsub2  11717  leord1  11747  lediv1  12086  lemuldiv  12101  lerec  12104  le2msq  12121  infm3  12180  suprnub  12186  infregelb  12205  avgle1  12490  avgle2  12491  znnnlt1  12627  indstr  12946  zsupss  12967  uzsupss  12970  rpneg  13056  xralrple  13237  xleneg  13250  xltadd1  13288  xposdif  13294  xmulneg1  13301  xltmul1  13324  xrsupexmnf  13337  xrinfmexpnf  13338  xrsupsslem  13339  xrinfmsslem  13340  xrub  13344  supxrleub  13358  infxrgelb  13368  difreicc  13517  nn0disj  13679  nelfzo  13700  elfznelfzo  13809  fvinim0ffz  13825  injresinjlem  13826  ssnn0fi  14028  leexp2  14214  exp11nnd  14304  hashbnd  14379  hasheni  14391  hashfundm  14486  hashbc  14497  wrdsymb0  14593  swrdnd  14699  swrdnd2  14700  pfxnd0  14733  repswswrd  14828  repswccat  14830  cshwidxmod  14847  cnpart  15298  sqrtlt  15319  limsuplt  15537  rlimrege0  15637  isercoll  15726  efle  16180  odd2np1  16405  sumodd  16452  divalglem7  16463  ndvdsadd  16474  fldivndvdslt  16480  bitsfval  16487  bitsval  16488  bits0  16492  bitsp1  16495  bitsmod  16500  bitscmp  16502  bitsinv1lem  16505  sadadd2lem2  16514  saddisjlem  16528  bitsshft  16539  gcdneg  16586  algcvgblem  16641  lcmneg  16667  isprm3  16747  dvdsnprmd  16754  isprm5  16772  rpexp  16787  phiprmpw  16841  m1dvdsndvds  16864  pythagtrip  16900  pcgcd1  16943  prmpwdvds  16970  prmreclem2  16983  prmreclem3  16984  prmreclem5  16986  prmreclem6  16987  vdwlem6  17052  vdwnnlem2  17062  vdwnnlem3  17063  vdwnn  17064  prmlem0  17171  prmlem1a  17172  divsfval  17607  mrisval  17692  ismri  17693  ismri2dad  17699  cidpropd  17772  cat1lem  18159  plttr  18402  joinval  18437  meetval  18451  acsfiindd  18615  isnsgrp  18787  smndex1n0mnd  18980  mgm2nsgrplem2  18987  sgrp2nmndlem3  18993  symgpssefmnd  19472  symgfix2  19492  pmtrdifellem4  19555  psgnunilem1  19569  psgnunilem5  19570  psgnunilem2  19571  psgnunilem3  19572  pmtrsn  19595  sylow1lem3  19676  sylow2alem2  19694  efgsfo  19815  ablfac1eulem  20150  ablfac1eu  20151  pgpfac1lem1  20152  pgpfac1lem5  20157  nzrunit  20633  zrninitoringc  20786  islbs  21208  lbsind  21212  lbspss  21214  lbspropd  21231  lspsnne1  21252  islbs2  21289  lbsacsbs  21291  lbsextlem1  21293  lbsextlem3  21295  lbsextlem4  21296  lbsextg  21297  ssdifidlprm  21497  frlmlbs  21958  islindf  21973  islinds2  21974  islindf2  21975  lindfind  21977  lindsind  21978  lindfrn  21982  lindfmm  21988  lsslindf  21991  islindf4  21999  opsrtoslem2  22218  psdmul  22340  cply1coe0  22472  cply1coe0bi  22473  mdetunilem7  22786  mdetunilem8  22787  mdetunilem9  22788  maducoeval2  22808  pmatcollpw3fi1lem1  22954  fvmptnn04ifa  23018  fvmptnn04ifc  23020  fvmptnn04ifd  23021  chfacffsupp  23024  chfacfscmul0  23026  chfacfpmmul0  23030  elcls  23241  maxlp  23315  perfi  23323  ordtbaslem  23356  ordtval  23357  ordtbas2  23359  ordtopn1  23362  ordtopn2  23363  ordtcnv  23369  ordtrest  23370  ordtrest2lem  23371  ordtrest2  23372  pnfnei  23388  mnfnei  23389  isreg2  23545  ordthauslem  23551  cmpfi  23576  cmpfii  23577  bwth  23578  nconnsubb  23591  hausdiag  23813  txkgen  23820  kqdisj  23900  ordthmeolem  23969  fbfinnfr  24009  trfbas  24012  fbunfip  24037  fbasrn  24052  trfil3  24056  ufileu  24087  fin1aufil  24100  hausflim  24149  alexsubALTlem2  24216  alexsubALTlem3  24217  alexsubALTlem4  24218  ptcmplem2  24221  ptcmplem3  24222  stdbdbl  24685  iccntr  24990  reconnlem2  24996  iccpnfcnv  25114  xrhmeo  25116  lebnumlem1  25131  lebnumlem2  25132  lebnumlem3  25133  bcthlem4  25497  minveclem3b  25598  ivthlem2  25622  ivthlem3  25623  mbfmax  25819  mbfposr  25822  i1fd  25851  mbfi1fseqlem4  25888  itg2splitlem  25918  itg2monolem1  25920  itg2cnlem1  25931  dvne0  26181  lhop1lem  26183  deg1nn0clb  26258  dgrle  26411  coemulhi  26422  plymulidp  26454  aaliou3lem9  26524  cos11  26709  logleb  26779  argrege0  26787  logdivle  26798  ellogdm  26815  cxple  26871  cxplt2  26874  cxple3  26877  isosctrlem1  26994  atandm  27052  atans2  27107  atantayl2  27114  eldmgm  27197  ftalem7  27254  isppw2  27290  musum  27366  dchrsum2  27443  bposlem1  27459  lgsmod  27498  lgsdir2lem2  27501  lgsdir2  27505  lgsne0  27510  lgsprme0  27514  gausslemma2dlem4  27544  lgsquadlem1  27555  2lgslem3  27579  2lgsoddprm  27591  2sq2  27608  addsqrexnreu  27617  rpvmasumlem  27662  padicabv  27805  ostth3  27813  ostth  27814  noextenddif  27843  nodenselem4  27862  nodenselem5  27863  nodenselem7  27865  nolt02o  27870  nogt01o  27871  noresle  27872  nosupprefixmo  27875  noinfprefixmo  27876  nosupcbv  27877  nosupdm  27879  nosupfv  27881  nosupres  27882  nosupbnd1lem1  27883  nosupbnd1lem3  27885  nosupbnd1lem5  27887  nosupbnd1  27889  nosupbnd2lem1  27890  nosupbnd2  27891  noinfcbv  27892  noinfdm  27894  noinffv  27896  noinfres  27897  noinfbnd1lem1  27898  noinfbnd1lem3  27900  noinfbnd1lem5  27902  noinfbnd1  27904  noinfbnd2lem1  27905  noinfbnd2  27906  lenlts  27927  ltsne  27949  nocvxminlem  27958  lesrec  28003  eqcuts3  28008  cuteq1  28021  newbday  28106  ltslpss  28112  cofcutr  28128  lrrecfr  28147  addsval  28166  ltadds2  28195  lenegs  28250  lesubsubsbd  28290  lesubsubs2bd  28291  lesubsubs3bd  28292  lesubaddsd  28297  ltmuls2  28375  lemuls2d  28378  lemuls1d  28379  oncutlt  28468  onles  28472  pw2cut2  28666  bdaypw2bnd  28669  bdayfinbndlem1  28671  istrkgld  28739  axtgupdim2  28751  tglowdim2l  28935  axlowdimlem16  29318  axlowdim2  29321  axlowdim  29322  numedglnl  29505  usgredg2v  29588  lfuhgr1v0e  29615  cusgrfi  29819  vtxd0nedgb  29849  vtxduhgr0edgnel  29855  1loopgrnb0  29863  1hevtxdg0  29866  vtxdgoddnumeven  29914  wlkp1lem1  30032  wlkp1lem2  30033  wlkp1lem5  30036  dfpth2  30089  crctcsh  30184  clwlkclwwlklem2a4  30359  eupth2eucrct  30579  eupth2lem3lem3  30592  eupth2lem3lem4  30593  eupth2lem3lem6  30595  eupth2lem3lem7  30596  eupth2lems  30600  eupth2  30601  konigsberglem4  30617  nfrgr2v  30634  frgrwopreglem3  30676  fusgr2wsp2nb  30696  frgrreggt1  30755  friendshipgt3  30760  lpni  30843  nmobndseqi  31142  minvecolem5  31244  chpsscon3  31866  chnle  31877  nonbooli  32014  pjnel  32089  specval  32261  nmcfnlbi  32415  stri  32620  hstri  32628  cvbr  32645  cvcon3  32647  chcv1  32718  cvexchlem  32731  chrelat2  32733  nelun  32870  elpreq  32885  nelpr  32888  ifeqeqx  32899  nfpconfp  32988  suppiniseg  33042  isoun  33058  suppss3  33079  xrge0infss  33116  infxrge0gelb  33122  eliccelico  33133  elicoelioo  33134  nndiffz1  33142  hashgt1  33164  expgt0b  33172  nn0min  33176  ccatws1f1o  33280  toslublem  33301  tosglblem  33303  pmtrcnel  33418  cycpmco2  33462  isarchi2  33514  archiabl  33527  elrgspnlem2  33572  elrgspnlem3  33573  0nellinds  33694  lindssn  33700  lindfpropd  33704  mxidlirred  33764  ssmxidl  33766  dflringlem  33793  esplyind  33974  lbslsat  34015  lindsunlem  34023  rtelextdg2lem  34125  constrsqrtcl  34178  ordtcnvNEW  34319  ordtrestNEW  34320  ordtrest2NEWlem  34321  ordtrest2NEW  34322  ordtconnlem1  34323  xrge0iifcnv  34332  esumpcvgval  34477  esum2d  34492  ddemeas  34635  omssubadd  34699  oddpwdc  34753  eulerpartlems  34759  eulerpartlemf  34769  eulerpartlemt  34770  eulerpartlemr  34773  eulerpartlemgvv  34775  eulerpartlemn  34780  ballotlemfc0  34892  ballotlemfcc  34893  ballotlem4  34898  ballotlemimin  34905  ballotlem7  34935  signsply0  34947  reprinfz1  35018  reprpmtf1o  35022  reprdifc  35023  hgt750lema  35053  hgt750leme  35054  istrkg2d  35062  bnj23  35116  bnj1185  35190  bnj1228  35408  bnj1388  35430  bnj1417  35438  ordtypeon  35490  nummin  35493  axprALT2  35512  fineqvnttrclselem1  35542  axnulg  35566  onvf1odlem2  35596  onvf1odlem3  35597  revwlk  35625  isacycgr  35645  acycgr0v  35648  prclisacycgr  35651  erdszelem10  35700  satf0n0  35878  fmlaomn0  35890  fmlasucdisj  35899  satfv1fvfmla1  35923  satefvfmla1  35925  ismfs  36049  mvtinf  36055  untelirr  36208  untsucf  36210  untangtr  36214  dfon2lem3  36283  dfon2lem4  36284  dfon2lem7  36287  dfon2lem9  36289  distel  36301  funpartfv  36445  dfrdg4  36451  nmulprop  36690  naddle  36719  nn0prpwlem  36861  nn0prpw  36862  limsucncmpi  36984  limsucncmp  36985  ordcmp  36986  weiunlem  37002  weiunfrlem  37003  weiunfr  37006  axtcond  37017  regsfromregtco  37077  regsfromsetind  37078  unblimceq0  37124  unbdqndv1  37125  bj-hbntbi  37357  bj-equsexvwd  37426  bj-cbvexdv  37463  bj-ru1  37607  bj-nuliota  37721  topdifinffinlem  38021  topdifinffin  38022  icorempo  38025  relowlpssretop  38038  finxpreclem2  38064  finxpreclem6  38070  wl-issetft  38265  wl-eujustlem1  38271  leceifl  38288  lindsadd  38292  lindsenlbs  38294  matunitlindflem1  38295  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem21  38320  poimirlem23  38322  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  poimirlem31  38330  poimir  38332  mblfinlem2  38337  mblfinlem3  38338  ismblfin  38340  cnambfre  38347  itg2addnclem  38350  itg2addnclem2  38351  iblabsnclem  38362  ftc1anclem1  38372  areacirc  38392  heibor1lem  38488  heiborlem1  38490  heiborlem6  38495  heiborlem8  38497  heiborlem10  38499  smprngopr  38731  ecin0  39029  ax12inda  39750  riotaclbgBAD  39756  lcvfbr  39822  lcvbr  39823  lsatcv0  39833  l1cvpat  39856  opltcon3b  40006  cvrfval  40070  cvrval  40071  cvrnbtwn  40073  cvrval2  40076  cvrnbtwn2  40077  cvrnbtwn3  40078  cvrcon3b  40079  cvrnbtwn4  40081  atnlt  40115  iscvlat  40125  cvlexch1  40130  hlsuprexch  40183  hlrelat5N  40203  hlrelat2  40205  cvrval5  40217  3dimlem1  40260  3dim1lem5  40268  3dim2  40270  3dim3  40271  llnnlt  40325  islpln5  40337  lplni2  40339  lvolex3N  40340  lplnnle2at  40343  islpln2a  40350  lplnribN  40353  lplnexllnN  40366  lplnnlt  40367  lvoli3  40379  islvol5  40381  lvoli2  40383  lvolnle3at  40384  islvol2aN  40394  4atlem11  40411  lvolnltN  40420  dalawlem15  40687  4atexlemex2  40873  4atex  40878  4atex2-0aOLDN  40880  4atex2-0cOLDN  40882  lautcvr  40894  ltrnfset  40919  ltrnset  40920  ltrnu  40923  trlfset  40962  trlset  40963  trlval2  40965  cdlemd6  41005  cdleme0nex  41092  cdleme18d  41097  cdleme25b  41156  cdleme25cv  41160  cdleme29b  41177  cdleme31fv  41192  cdleme31fv2  41195  cdlemefrs29bpre0  41198  cdlemefr32sn2aw  41206  cdlemefr29bpre0N  41208  cdlemefr29clN  41209  cdlemefr32fvaN  41211  cdlemefr32fva1  41212  cdlemefs32sn1aw  41216  cdleme32fva  41239  cdleme32fvaw  41241  cdleme40v  41271  cdleme42b  41280  cdleme46f2g2  41295  cdleme46f2g1  41296  cdleme48gfv  41339  cdlemg1fvawlemN  41375  cdlemg1cex  41390  cdlemg6d  41423  cdlemm10N  41920  dicffval  41976  dicfval  41977  dicval  41978  dicfnN  41985  dicvalrelN  41987  dihffval  42032  dihfval  42033  dihlsscpre  42036  dvh4dimat  42240  dvh3dimatN  42241  dvh4dimlem  42245  dvh3dim  42248  dvh4dimN  42249  dvh3dim2  42250  dvh3dim3N  42251  mapdcv  42462  mapdh9aOLDN  42592  hdmapfval  42629  hdmapval  42630  hdmapval2  42634  hdmap11lem2  42644  dvrelog2b  42861  aks4d1p4  42874  aks4d1p5  42875  aks4d1p7  42878  aks4d1p8d2  42880  aks4d1p8  42882  aks4d1  42884  aks6d1c2p2  42914  hashnexinj  42923  rspcsbnea  42926  aks6d1c5  42934  aks6d1c6lem3  42967  aks6d1c7  42979  supinf  43038  oexpreposd  43111  mullt0b2d  43286  flt4lem7  43419  nna4b4nsq  43420  ellz1  43526  rencldnfilem  43575  jm2.22  43750  jm2.23  43751  wepwsolem  43797  fnwe2lem2  43806  aomclem8  43816  unxpwdom3  43850  onsupmaxb  43994  onexlimgt  43998  onsupeqnmax  44002  onov0suclim  44029  oaordnr  44051  omnord1  44060  oenord1  44071  oaomoencom  44072  oenass  44074  cantnfresb  44079  tfsnfin  44107  ralopabb  44165  nlimsuc  44195  ifpbi12  44242  dfsucon  44277  sqrtcvallem1  44385  ss2iundf  44413  frege124d  44515  clsk3nimkb  44794  clsk1indlem1  44799  clsk1independent  44800  ntrneineine1lem  44838  ntrneicls11  44844  clsneiel1  44862  clsneiel2  44863  neicvgel1  44873  neicvgel2  44874  radcnvrat  45052  rusbcALT  45176  en3lpVD  45581  0elaxnul  45720  omssaxinf2  45725  permaxnul  45745  permaxinf2lem  45749  nregmodel  45754  eliin2f  45850  nssd  45851  wessf1ornlem  45931  rexanuz2nf  46234  limsupre2lem  46466  icccncfext  46629  stoweidlem14  46756  stoweidlem34  46776  stoweidlem59  46801  etransclem24  47000  nnfoctbdjlem  47197  nnfoctbdj  47198  hspmbllem2  47369  nsssmfmbflem  47520  fsetsnprcnex  47820  eu2ndop1stv  47890  afvfv0bi  47917  afvco2  47941  ndmaovg  47949  ndfatafv2nrn  47986  afv2ndefb  47989  afv2fv0  48030  nelbr  48039  otiunsndisjX  48044  fun2dmnopgexmpl  48049  ltnltne  48064  readdcnnred  48068  resubcnnred  48069  recnmulnred  48070  cndivrenred  48071  ichnreuop  48249  nprmmul1  48304  fmtnoinf  48316  odz2prm2pw  48343  prmdvdsfmtnof1lem2  48365  lighneallem3  48387  lighneallem4  48390  requad1  48415  isodd3  48445  bits0ALTV  48472  nfermltl8rev  48535  nfermltl2rev  48536  nfermltlrev  48537  upgrimpths  48702  isubgr3stgrlem3  48761  usgrexmpl12ngric  48831  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  pgnbgreunbgrlem5lem1  48913  pgnbgreunbgrlem5lem2  48914  pgnbgreunbgrlem5lem3  48915  lgricngricex  48922  lidldomnnring  49029  smprngprmrng  49132  ztprmneprm  49155  lindepsnlininds  49260  islindeps  49261  lindslinindsimp2lem5  49270  lindslinindsimp2  49271  line2ylem  49559  line2xlem  49561  map0cor  49661  nelsubc3lem  49876  fulltermc2  50318  setc1onsubc  50408  cnelsubclem  50409  elsetrecslem  50505