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  2038  cbvexvw  2070  cbvexdvaw  2072  excomimw  2077  hbe1w  2083  19.8aw  2085  exexw  2086  ru0  2164  cbvexv1  2371  cbvex2v  2373  drex1v  2399  cbvex  2428  cbvex2  2441  drex1  2470  eujustALT  2597  necon3abid  2991  neleq12d  3066  cbvrexdva  3243  cbvrexfw  3303  cbvrexdva2  3337  cbvrexf  3346  cbvexeqsetf  3465  ceqsex  3497  ceqsexv  3498  gencbval  3508  spcegf  3546  spc2gv  3554  spc2d  3556  spc3gv  3558  ceqsralbv  3611  cdeqnot  3726  rru  3737  sbcng  3786  sbcrext  3820  cbvrexcsf  3890  difjust  3901  eldif  3909  dfpss3  4037  difeq2  4068  disjne  4408  pssdifcom1  4445  eldifpr  4619  rexsng  4637  elpwunsn  4645  eldiftp  4648  rexprg  4658  preqsnd  4819  disjxun  5101  exnelv  5270  nalsetOLD  5272  dtruALT2  5335  dtruALT  5353  rexxfrd  5374  rexxfr2d  5376  rexxfrd2  5378  rexxfr  5381  opthneg  5457  snopeqop  5483  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  5736  frinxp  5738  posn  5741  frsn  5743  rexiunxp  5821  rexxpf  5829  intirr  6114  poirr2  6120  cnvpo  6287  dfpo2  6296  predpoirr  6333  predfrirr  6334  frpomin  6340  nordeq  6378  ordtri1  6393  ordtri3  6396  fvmpti  6988  fndmdif  7037  rexrnmptw  7091  rexrnmpt  7093  rexima  7240  f1imapss  7266  f1ounsn  7276  cbvexfo  7294  nf1const  7308  soisoi  7332  isopolem  7349  weniso  7360  canth  7370  riotaclb  7414  rexrnmpo  7556  ndmovg  7600  sorpssuni  7739  sorpssint  7740  fr3nr  7777  dfwe2  7779  ordsucsssuc  7825  nlimsucg  7844  orduninsuc  7845  dfom2  7870  ssnlim  7888  resf1extb  7937  f1oweALT  7975  frxp  8129  poxp  8131  frxp2  8147  frxp3  8154  xpord3inddlem  8157  soseq  8162  suppofssd  8206  suppcoss  8210  smoword  8360  tz7.48lemOLD  8437  oacan  8542  oaword  8543  omlimcl  8572  omeulem1  8576  nnaword  8622  nnmword  8628  nneob  8651  naddss1  8685  brdifun  8734  swoer  8735  undifixp  8948  boxcutc  8955  2dom  9044  php  9208  phpeqd  9213  nndomog  9214  onomeneq  9215  nnsdomo  9220  unxpdomlem2  9234  frfi  9262  unfilem1  9282  tfsnfin2  9337  supeq3  9426  supeq123d  9427  supmo  9429  eqsup  9433  supub  9436  sup0  9444  suppr  9449  supisolem  9451  supisoex  9452  eqinf  9462  infval  9464  infmo  9474  infpr  9482  infempty  9486  oieq1  9491  ordtypecbv  9496  ordtypelem7  9503  wemapsolem  9529  canthwdom  9558  zfregcl  9573  zfregclOLD  9574  elirrv  9576  elirrvOLD  9577  elirrvOLDOLD  9578  elirr  9579  noinfep  9646  cantnfp1lem3  9666  ttrcltr  9702  rankr1clem  9809  carden2b  9997  domtri2  10019  alephord3  10106  alephdom2  10115  alephval3  10138  dfac9  10164  kmlem2  10179  kmlem4  10181  isfin4  10324  isfin7  10328  fin23lem11  10344  isf32lem5  10384  isf34lem4  10404  fin1a2lem6  10432  fin1a2lem7  10433  fin1a2lem12  10438  itunisuc  10446  ac6n  10512  zorn2g  10530  zornn0g  10532  ttukeylem7  10542  infinfg  10599  axpowndlem3  10633  axpowndlem4  10634  axregnd  10638  elgch  10656  engch  10662  fpwwe2lem12  10676  fpwwe2  10677  pwfseqlem1  10692  pwfseqlem3  10694  hargch  10707  addnidpi  10935  pinq  10961  nqereu  10963  ltsonq  11003  prlem934  11067  ltexprlem7  11076  addcanpr  11080  prlem936  11081  reclem2pr  11082  reclem3pr  11083  supexpr  11088  ltsosr  11128  supsrlem  11145  axpre-lttri  11199  axpre-sup  11203  xrlenlt  11323  axlttri  11330  axsup  11334  ltne  11356  dedekind  11422  readdcan  11433  leadd1  11731  ltsub1  11759  ltsub2  11760  leord1  11790  lediv1  12129  lemuldiv  12144  lerec  12147  le2msq  12164  infm3  12223  suprnub  12229  infregelb  12248  avgle1  12533  avgle2  12534  znnnlt1  12670  indstr  12990  zsupss  13011  uzsupss  13014  rpneg  13101  xralrple  13282  xleneg  13295  xltadd1  13333  xposdif  13339  xmulneg1  13346  xltmul1  13369  xrsupexmnf  13382  xrinfmexpnf  13383  xrsupsslem  13384  xrinfmsslem  13385  xrub  13389  supxrleub  13403  infxrgelb  13413  difreicc  13562  nn0disj  13724  nelfzo  13745  elfznelfzo  13854  fvinim0ffz  13870  injresinjlem  13871  ssnn0fi  14074  leexp2  14260  exp11nnd  14350  hashbnd  14425  hasheni  14437  hashfundm  14532  hashbc  14543  wrdsymb0  14639  swrdnd  14749  swrdnd2  14750  pfxnd0  14783  repswswrd  14880  repswccat  14882  cshwidxmod  14899  cnpart  15352  sqrtlt  15373  limsuplt  15591  rlimrege0  15691  isercoll  15780  efle  16231  odd2np1  16456  sumodd  16503  divalglem7  16514  ndvdsadd  16525  fldivndvdslt  16531  bitsfval  16538  bitsval  16539  bits0  16543  bitsp1  16546  bitsmod  16551  bitscmp  16553  bitsinv1lem  16556  sadadd2lem2  16565  saddisjlem  16579  bitsshft  16590  gcdneg  16637  algcvgblem  16692  lcmneg  16718  isprm3  16798  dvdsnprmd  16805  isprm5  16823  rpexp  16838  phiprmpw  16892  m1dvdsndvds  16915  pythagtrip  16951  pcgcd1  16994  prmpwdvds  17021  prmreclem2  17034  prmreclem3  17035  prmreclem5  17037  prmreclem6  17038  vdwlem6  17103  vdwnnlem2  17113  vdwnnlem3  17114  vdwnn  17115  prmlem0  17222  prmlem1a  17223  divsfval  17658  mrisval  17743  ismri  17744  ismri2dad  17750  cidpropd  17823  cat1lem  18210  plttr  18453  joinval  18488  meetval  18502  acsfiindd  18666  isnsgrp  18851  smndex1n0mnd  19050  mgm2nsgrplem2  19057  sgrp2nmndlem3  19063  degenmgm2nfun  19078  symgpssefmnd  19549  symgfix2  19569  pmtrdifellem4  19632  psgnunilem1  19646  psgnunilem5  19647  psgnunilem2  19648  psgnunilem3  19649  pmtrsn  19672  sylow1lem3  19753  sylow2alem2  19771  efgsfo  19892  ablfac1eulem  20227  ablfac1eu  20228  pgpfac1lem1  20229  pgpfac1lem5  20234  nzrunit  20714  zrninitoringc  20867  islbs  21290  lbsind  21294  lbspss  21296  lbspropd  21313  lspsnne1  21334  islbs2  21371  lbsacsbs  21373  lbsextlem1  21375  lbsextlem3  21377  lbsextlem4  21378  lbsextg  21379  ssdifidlprm  21581  frlmlbs  22042  islindf  22057  islinds2  22058  islindf2  22059  lindfind  22061  lindsind  22062  lindfrn  22066  lindfmm  22072  lsslindf  22075  islindf4  22083  lindsenlbs  22096  opsrtoslem2  22304  psdmul  22426  cply1coe0  22558  cply1coe0bi  22559  mdetunilem7  22872  mdetunilem8  22873  mdetunilem9  22874  maducoeval2  22894  matunitlindflem1  22933  pmatcollpw3fi1lem1  23043  fvmptnn04ifa  23107  fvmptnn04ifc  23109  fvmptnn04ifd  23110  chfacffsupp  23113  chfacfscmul0  23115  chfacfpmmul0  23119  elcls  23330  maxlp  23404  perfi  23412  ordtbaslem  23445  ordtval  23446  ordtbas2  23448  ordtopn1  23451  ordtopn2  23452  ordtcnv  23458  ordtrest  23459  ordtrest2lem  23460  ordtrest2  23461  pnfnei  23477  mnfnei  23478  isreg2  23634  ordthauslem  23640  cmpfi  23665  cmpfii  23666  bwth  23667  nconnsubb  23680  hausdiag  23903  txkgen  23910  kqdisj  23990  ordthmeolem  24059  fbfinnfr  24099  trfbas  24102  fbunfip  24127  fbasrn  24142  trfil3  24146  ufileu  24177  fin1aufil  24190  hausflim  24239  alexsubALTlem2  24306  alexsubALTlem3  24307  alexsubALTlem4  24308  ptcmplem2  24311  ptcmplem3  24312  stdbdbl  24775  iccntr  25080  reconnlem2  25086  iccpnfcnv  25204  xrhmeo  25206  lebnumlem1  25221  lebnumlem2  25222  lebnumlem3  25223  bcthlem4  25587  minveclem3b  25688  ivthlem2  25712  ivthlem3  25713  mbfmax  25909  mbfposr  25912  i1fd  25941  mbfi1fseqlem4  25978  itg2splitlem  26008  itg2monolem1  26010  itg2cnlem1  26021  dvne0  26270  lhop1lem  26272  deg1nn0clb  26347  dgrle  26501  coemulhi  26512  plymulidp  26544  aaliou3lem9  26618  cos11  26802  logleb  26872  argrege0  26880  logdivle  26891  ellogdm  26908  cxple  26964  cxplt2  26967  cxple3  26970  isosctrlem1  27087  atandm  27145  atans2  27200  atantayl2  27207  eldmgm  27290  ftalem7  27347  isppw2  27383  musum  27459  dchrsum2  27536  bposlem1  27552  lgsmod  27591  lgsdir2lem2  27594  lgsdir2  27598  lgsne0  27603  lgsprme0  27607  gausslemma2dlem4  27637  lgsquadlem1  27648  2lgslem3  27672  2lgsoddprm  27684  2sq2  27701  addsqrexnreu  27710  rpvmasumlem  27755  padicabv  27898  ostth3  27906  ostth  27907  noextenddif  27936  nodenselem4  27955  nodenselem5  27956  nodenselem7  27958  nolt02o  27963  nogt01o  27964  noresle  27965  nosupprefixmo  27968  noinfprefixmo  27969  nosupcbv  27970  nosupdm  27972  nosupfv  27974  nosupres  27975  nosupbnd1lem1  27976  nosupbnd1lem3  27978  nosupbnd1lem5  27980  nosupbnd1  27982  nosupbnd2lem1  27983  nosupbnd2  27984  noinfcbv  27985  noinfdm  27987  noinffv  27989  noinfres  27990  noinfbnd1lem1  27991  noinfbnd1lem3  27993  noinfbnd1lem5  27995  noinfbnd1  27997  noinfbnd2lem1  27998  noinfbnd2  27999  lenlts  28020  ltsne  28042  nocvxminlem  28051  lesrec  28096  eqcuts3  28101  cuteq1  28114  newbday  28199  ltslpss  28205  cofcutr  28221  lrrecfr  28240  addsval  28259  ltadds2  28288  lenegs  28343  lesubsubsbd  28383  lesubsubs2bd  28384  lesubsubs3bd  28385  lesubaddsd  28390  ltmuls2  28468  lemuls2d  28471  lemuls1d  28472  oncutlt  28561  onles  28565  pw2cut2  28759  bdaypw2bnd  28762  bdayfinbndlem1  28764  istrkgld  28832  axtgupdim2  28844  tglowdim2l  29030  axlowdimlem16  29446  axlowdim2  29449  axlowdim  29450  numedglnl  29633  usgredg2v  29719  lfuhgr1v0e  29746  cusgrfi  29950  vtxd0nedgb  29980  vtxduhgr0edgnel  29986  1loopgrnb0  29994  1hevtxdg0  29997  vtxdgoddnumeven  30045  wlkp1lem1  30163  wlkp1lem2  30164  wlkp1lem5  30167  revwlk  30178  dfpth2  30225  crctcsh  30324  clwlkclwwlklem2a4  30499  isacycgr  30662  eupth2eucrct  30729  eupth2lem3lem3  30742  eupth2lem3lem4  30743  eupth2lem3lem6  30745  eupth2lem3lem7  30746  eupth2lems  30750  eupth2  30751  konigsberglem4  30767  nfrgr2v  30784  frgrwopreglem3  30826  fusgr2wsp2nb  30846  frgrreggt1  30905  friendshipgt3  30910  lpni  30993  nmobndseqi  31292  minvecolem5  31394  chpsscon3  32016  chnle  32027  nonbooli  32164  pjnel  32239  specval  32411  nmcfnlbi  32565  stri  32770  hstri  32778  cvbr  32795  cvcon3  32797  chcv1  32868  cvexchlem  32881  chrelat2  32883  nelun  33020  elpreq  33035  nelpr  33038  ifeqeqx  33049  nfpconfp  33137  suppiniseg  33190  isoun  33206  suppss3  33226  xrge0infss  33263  infxrge0gelb  33269  eliccelico  33280  elicoelioo  33281  nndiffz1  33289  hashgt1  33311  expgt0b  33319  nn0min  33323  ccatws1f1o  33425  toslublem  33444  tosglblem  33446  pmtrcnel  33561  cycpmco2  33605  isarchi2  33657  archiabl  33670  elrgspnlem2  33715  elrgspnlem3  33716  0nellinds  33837  lindssn  33844  lindfpropd  33848  mxidlirred  33908  ssmxidl  33910  dflringlem  33937  esplyind  34118  lbslsat  34159  lindsunlem  34167  rtelextdg2lem  34269  constrsqrtcl  34322  ordtcnvNEW  34463  ordtrestNEW  34464  ordtrest2NEWlem  34465  ordtrest2NEW  34466  ordtconnlem1  34467  xrge0iifcnv  34476  esumpcvgval  34621  esum2d  34636  ddemeas  34780  omssubadd  34844  oddpwdc  34898  eulerpartlems  34904  eulerpartlemf  34914  eulerpartlemt  34915  eulerpartlemr  34918  eulerpartlemgvv  34920  eulerpartlemn  34925  ballotlemfc0  35037  ballotlemfcc  35038  ballotlem4  35043  ballotlemimin  35050  ballotlem7  35080  signsply0  35092  reprinfz1  35163  reprpmtf1o  35167  reprdifc  35168  hgt750lema  35198  hgt750leme  35199  istrkg2d  35207  bnj23  35261  bnj1185  35335  bnj1228  35553  bnj1388  35575  bnj1417  35583  ordtypeon  35628  nummin  35631  axprALT2  35650  fineqvnttrclselem1  35690  axnulg  35714  onvf1odlem2  35784  onvf1odlem3  35785  acycgr0v  35810  prclisacycgr  35813  erdszelem10  35862  satf0n0  36040  fmlaomn0  36052  fmlasucdisj  36061  satfv1fvfmla1  36085  satefvfmla1  36087  ismfs  36211  mvtinf  36217  untelirr  36370  untsucf  36372  untangtr  36376  dfon2lem3  36445  dfon2lem4  36446  dfon2lem7  36449  dfon2lem9  36451  distel  36463  funpartfv  36607  dfrdg4  36613  nmulprop  36837  naddle  36866  nn0prpwlem  37008  nn0prpw  37009  limsucncmpi  37131  limsucncmp  37132  ordcmp  37133  weiunlem  37149  weiunfrlem  37150  weiunfr  37153  axtcond  37164  regsfromregtco  37224  regsfromsetind  37225  unblimceq0  37271  unbdqndv1  37272  bj-hbntbi  37504  bj-equsexvwd  37573  bj-cbvexdv  37610  bj-ru1  37754  bj-nuliota  37868  topdifinffinlem  38166  topdifinffin  38167  icorempo  38170  relowlpssretop  38183  finxpreclem2  38209  finxpreclem6  38215  wl-issetft  38410  wl-eujustlem1  38416  leceifl  38428  lindsadd  38432  poimirlem16  38450  poimirlem17  38451  poimirlem18  38452  poimirlem19  38453  poimirlem21  38455  poimirlem23  38457  poimirlem26  38460  poimirlem27  38461  poimirlem28  38462  poimirlem31  38465  poimir  38467  mblfinlem2  38472  mblfinlem3  38473  ismblfin  38475  cnambfre  38482  itg2addnclem  38485  itg2addnclem2  38486  iblabsnclem  38497  ftc1anclem1  38507  areacirc  38527  heibor1lem  38624  heiborlem1  38626  heiborlem6  38631  heiborlem8  38633  heiborlem10  38635  smprngopr  38867  ecin0  39165  ax12inda  39886  riotaclbgBAD  39892  lcvfbr  39958  lcvbr  39959  lsatcv0  39969  l1cvpat  39992  opltcon3b  40142  cvrfval  40206  cvrval  40207  cvrnbtwn  40209  cvrval2  40212  cvrnbtwn2  40213  cvrnbtwn3  40214  cvrcon3b  40215  cvrnbtwn4  40217  atnlt  40251  iscvlat  40261  cvlexch1  40266  hlsuprexch  40319  hlrelat5N  40339  hlrelat2  40341  cvrval5  40353  3dimlem1  40396  3dim1lem5  40404  3dim2  40406  3dim3  40407  llnnlt  40461  islpln5  40473  lplni2  40475  lvolex3N  40476  lplnnle2at  40479  islpln2a  40486  lplnribN  40489  lplnexllnN  40502  lplnnlt  40503  lvoli3  40515  islvol5  40517  lvoli2  40519  lvolnle3at  40520  islvol2aN  40530  4atlem11  40547  lvolnltN  40556  dalawlem15  40823  4atexlemex2  41009  4atex  41014  4atex2-0aOLDN  41016  4atex2-0cOLDN  41018  lautcvr  41030  ltrnfset  41055  ltrnset  41056  ltrnu  41059  trlfset  41098  trlset  41099  trlval2  41101  cdlemd6  41141  cdleme0nex  41228  cdleme18d  41233  cdleme25b  41292  cdleme25cv  41296  cdleme29b  41313  cdleme31fv  41328  cdleme31fv2  41331  cdlemefrs29bpre0  41334  cdlemefr32sn2aw  41342  cdlemefr29bpre0N  41344  cdlemefr29clN  41345  cdlemefr32fvaN  41347  cdlemefr32fva1  41348  cdlemefs32sn1aw  41352  cdleme32fva  41375  cdleme32fvaw  41377  cdleme40v  41407  cdleme42b  41416  cdleme46f2g2  41431  cdleme46f2g1  41432  cdleme48gfv  41475  cdlemg1fvawlemN  41511  cdlemg1cex  41526  cdlemg6d  41559  cdlemm10N  42056  dicffval  42112  dicfval  42113  dicval  42114  dicfnN  42121  dicvalrelN  42123  dihffval  42168  dihfval  42169  dihlsscpre  42172  dvh4dimat  42376  dvh3dimatN  42377  dvh4dimlem  42381  dvh3dim  42384  dvh4dimN  42385  dvh3dim2  42386  dvh3dim3N  42387  mapdcv  42598  mapdh9aOLDN  42728  hdmapfval  42765  hdmapval  42766  hdmapval2  42770  hdmap11lem2  42780  dvrelog2b  42997  aks4d1p4  43010  aks4d1p5  43011  aks4d1p7  43014  aks4d1p8d2  43016  aks4d1p8  43018  aks4d1  43020  aks6d1c2p2  43050  hashnexinj  43059  rspcsbnea  43062  aks6d1c5  43070  aks6d1c6lem3  43103  aks6d1c7  43115  supinf  43174  oexpreposd  43262  mullt0b2d  43437  flt4lem7  43570  nna4b4nsq  43571  ellz1  43677  rencldnfilem  43726  jm2.22  43901  jm2.23  43902  wepwsolem  43948  fnwe2lem2  43957  aomclem8  43967  unxpwdom3  44001  onsupmaxb  44145  onexlimgt  44149  onsupeqnmax  44153  onov0suclim  44180  oaordnr  44202  omnord1  44211  oenord1  44222  oaomoencom  44223  oenass  44225  cantnfresb  44230  tfsnfin  44258  ralopabb  44316  nlimsuc  44346  ifpbi12  44393  dfsucon  44428  sqrtcvallem1  44536  ss2iundf  44564  frege124d  44666  clsk3nimkb  44945  clsk1indlem1  44950  clsk1independent  44951  ntrneineine1lem  44989  ntrneicls11  44995  clsneiel1  45013  clsneiel2  45014  neicvgel1  45024  neicvgel2  45025  radcnvrat  45203  rusbcALT  45327  en3lpVD  45732  0elaxnul  45871  omssaxinf2  45876  permaxnul  45896  permaxinf2lem  45900  nregmodel  45905  eliin2f  46001  nssd  46002  wessf1ornlem  46082  rexanuz2nf  46385  limsupre2lem  46617  icccncfext  46780  stoweidlem14  46907  stoweidlem34  46927  stoweidlem59  46952  etransclem24  47151  nnfoctbdjlem  47348  nnfoctbdj  47349  hspmbllem2  47520  nsssmfmbflem  47671  fsetsnprcnex  48008  eu2ndop1stv  48078  afvfv0bi  48105  afvco2  48129  ndmaovg  48137  ndfatafv2nrn  48174  afv2ndefb  48177  afv2fv0  48218  nelbr  48227  otiunsndisjX  48232  fun2dmnopgexmpl  48237  ltnltne  48252  readdcnnred  48256  resubcnnred  48257  recnmulnred  48258  cndivrenred  48259  ichnreuop  48437  nprmmul1  48492  fmtnoinf  48504  odz2prm2pw  48531  prmdvdsfmtnof1lem2  48553  lighneallem3  48575  lighneallem4  48578  requad1  48603  isodd3  48633  bits0ALTV  48660  nfermltl8rev  48723  nfermltl2rev  48724  nfermltlrev  48725  upgrimpths  48890  isubgr3stgrlem3  48949  usgrexmpl12ngric  49019  pgnbgreunbgrlem2lem1  49095  pgnbgreunbgrlem2lem2  49096  pgnbgreunbgrlem2lem3  49097  pgnbgreunbgrlem5lem1  49101  pgnbgreunbgrlem5lem2  49102  pgnbgreunbgrlem5lem3  49103  lgricngricex  49110  lidldomnnring  49216  smprngprmrng  49319  ztprmneprm  49342  lindepsnlininds  49447  islindeps  49448  lindslinindsimp2lem5  49457  lindslinindsimp2  49458  line2ylem  49746  line2xlem  49748  map0cor  49848  nelsubc3lem  50061  fulltermc2  50503  setc1onsubc  50593  cnelsubclem  50594  elsetrecslem  50690