MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syldan Unicode version

Theorem syldan 470
Description: A syllogism deduction with conjoined antecedents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
Hypotheses
Ref Expression
syldan.1
syldan.2
Assertion
Ref Expression
syldan

Proof of Theorem syldan
StepHypRef Expression
1 syldan.1 . 2
2 syldan.2 . . . 4
32expcom 435 . . 3
43adantrd 468 . 2
51, 4mpcom 36 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  sylan2  474  stoic2a  1607  sbcied2  3365  csbied2  3462  elpwunsn  4070  elpw2g  4615  pofun  4821  fnbr  5688  dffv2  5946  grprinvlem  6513  caofid0l  6568  caofid0r  6569  caofid1  6570  caofid2  6571  caofcom  6572  fnexALT  6766  frxp  6910  fnse  6917  brovex  6969  tfr3  7087  tz7.48-2  7126  oaf1o  7231  omlimcl  7246  oeeulem  7269  ixpexg  7513  f1domg  7555  domdifsn  7620  unxpdom2  7748  xpfir  7762  fofinf1o  7821  fofi  7826  imafi  7833  intrnfi  7896  ordtypelem6  7969  oiexg  7981  cantnfp1lem3  8120  cantnflem1  8129  cantnfp1lem3OLD  8146  cantnflem1OLD  8152  infxpenlem  8412  fseqenlem2  8427  ssnum  8441  acni2  8448  finacn  8452  fonum  8460  infpwfien  8464  inffien  8465  infunsdom1  8614  infunsdom  8615  ackbij1lem12  8632  cfslb2n  8669  fin23lem28  8741  compssiso  8775  isf34lem5  8779  fin56  8794  axcc3  8839  axdc3lem2  8852  ttukeylem6  8915  ttukeylem7  8916  brdom3  8927  gchdomtri  9028  fpwwe2lem13  9041  gchxpidm  9068  tsken  9153  tsksn  9159  tsk1  9163  tsk2  9164  2domtsk  9165  tskcard  9180  r1tskina  9181  gruss  9195  gruxp  9206  gruina  9217  grur1a  9218  ltaddpr  9433  ltexprlem7  9441  1idsr  9496  addgt0sr  9502  recexsr  9505  msqgt0  10098  mulgt1  10426  gt0div  10433  ge0div  10434  ltdiv2  10455  ltrec1  10457  lerec2  10458  lediv2  10460  lediv12a  10463  recreclt  10469  creur  10555  nn2ge  10586  avgle1  10803  recnz  10963  suprzcl  10967  uzwo2  11175  rpnnen1lem5  11241  xrrege0  11404  xlemul1a  11509  xrsupsslem  11527  xrinfmsslem  11528  supxr2  11534  supxrpnf  11539  supxrunb1  11540  supxrunb2  11541  ixxun  11574  peano2fzor  11917  ioopnfsup  11991  modcl  12000  modge0  12005  zmodcl  12015  seqcl  12127  seqf  12128  seqfveq  12131  sermono  12139  seqsplit  12140  seqcaopr2  12143  seqf1olem2  12147  seqf1o  12148  seqhomo  12154  seqz  12155  le2sq2  12243  faclbnd4lem3  12373  bcpasc  12399  hashgt0  12456  seqcoll  12512  seqcoll2  12513  hashge2el2dif  12521  wrdnval  12571  wrdsymb1  12578  ccatlid  12603  ccatass  12605  swrdtrcfvl  12675  swrdlsw  12677  2swrd1eqwrdeq  12679  ccatswrd  12681  swrd0swrd  12686  swrdccatwrd  12693  wrdeqcats1  12699  wrdeqs1cat  12700  swrdccatin2  12712  revccat  12740  revrev  12741  sqrlem7  13082  resqrex  13084  sqrtgt0  13092  leabs  13132  absmax  13162  r19.2uz  13184  lo1bdd2  13347  o1lo12  13361  rlimclim1  13368  lo1eq  13391  rlimeq  13392  rlimcn1  13411  rlimcn2  13413  rlimdiv  13468  rlimsqzlem  13471  clim2ser  13477  clim2ser2  13478  climub  13484  isercolllem1  13487  isercolllem3  13489  isercoll2  13491  climsup  13492  serf0  13503  iseraltlem1  13504  fsumf1o  13545  fsumss  13547  fsumsplit  13562  fsummsnunz  13569  fsum2dlem  13585  fsumless  13610  fsumabs  13615  telfsumo  13616  fsumparts  13620  fsumrlim  13625  fsumo1  13626  o1fsum  13627  cvgcmp  13630  cvgcmpce  13632  fsumiun  13635  binom1dif  13645  incexclem  13648  incexc  13649  isumsplit  13652  isumrpcl  13655  isumless  13657  isumsup2  13658  isumltss  13660  climcnds  13663  supcvg  13667  expcnv  13675  explecnv  13676  geomulcvg  13685  cvgrat  13692  mertenslem1  13693  clim2prod  13697  clim2div  13698  ntrivcvgfvn0  13708  ntrivcvgmullem  13710  fprodf1o  13753  prodss  13754  fprodss  13755  fprodser  13756  fprodsplit  13770  fprodeq0  13779  fprod2dlem  13784  efcllem  13813  ef0lem  13814  eftlub  13844  tanval3  13869  tanneg  13883  rpnnen2lem7  13954  rpnnen2lem9  13956  rpnnen2lem11  13958  ruclem9  13971  dvdssubr  14027  divalgmod  14064  bitsf1  14096  algfx  14209  eucalgcvga  14215  isprm6  14250  phimullem  14309  eulerthlem2  14312  pcid  14396  pcgcd  14401  unbenlem  14426  prmreclem4  14437  prmreclem5  14438  4sqlem9  14464  4sqlem15  14477  4sqlem16  14478  vdwlem2  14500  vdwlem6  14504  vdwlem10  14508  vdwlem11  14509  vdwlem13  14511  ramval  14526  ressabs  14695  imasaddflem  14927  imasvscaf  14936  mrcid  15010  mrcidb  15012  mrcidm  15016  fucidcl  15334  setcmon  15414  setcepi  15415  catccatid  15429  xpccatid  15457  yonedalem4c  15546  yonedainv  15550  pospo  15603  latjlej1  15695  latmlem1  15711  latledi  15719  latj32  15727  latjjdi  15733  mrelatlub  15816  mreclatBAD  15817  psss  15844  tsrlemax  15850  grpidd  15895  gsumress  15903  gsumval2  15907  ismndd  15943  issubmnd  15948  subsubm  15988  sgrp2rid2  16044  grpinvid1  16098  grpinvid2  16099  grplcan  16102  grpinvinv  16105  grpinvval2  16121  mulgass  16172  mulgpropd  16175  subginv  16208  subgmulg  16215  issubg2  16216  issubg4  16220  subsubg  16224  eqger  16251  qusinv  16260  resghm  16283  pwsdiagghm  16294  conjsubgen  16299  conjnsg  16302  subgga  16338  gass  16339  gasubg  16340  orbstafun  16349  orbsta  16351  symgextfv  16443  psgnunilem5  16519  gexcl2  16609  gexdvds3  16610  sylow1lem2  16619  sylow2blem1  16640  pj1ghm  16721  frgpup1  16793  frgpup3lem  16795  cntzspan  16850  cyggeninv  16886  lt6abl  16897  cycsubgcyg  16903  gsumval3eu  16907  gsumval3OLD  16908  gsumval3  16911  gsumzres  16914  gsumzresOLD  16918  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumzsplit  16944  gsumzsplitOLD  16945  gsum2d  16999  gsum2dOLD  17000  gsum2d2lem  17001  fsfnn0gsumfsffz  17011  dprdres  17075  dprdz  17077  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  dprdcntz2  17086  dprddisj2  17087  dprddisj2OLD  17088  dprd2dlem1  17090  dmdprdsplit2lem  17094  dmdprdsplit2  17095  dprdsplit  17097  ablfac1c  17122  ablfac1eulem  17123  ablfac1eu  17124  pgpfac1lem2  17126  ablfac2  17140  ringidss  17225  isringd  17233  ringlz  17235  ringrz  17236  gsumdixpOLD  17257  gsumdixp  17258  0unit  17329  unitnegcl  17330  ringinvdv  17343  invrpropd  17347  subrg1  17439  subrginv  17445  issubrg2  17449  subsubrg  17455  abvneg  17483  lmod0vs  17545  lmodvs0  17546  lmodvneg1  17553  islss3  17605  lspsnsubg  17626  lspidm  17632  lspsnneg  17652  lmhmlsp  17695  drngnidl  17877  01eq0ring  17920  psrass1lem  18029  psrlinv  18050  psrlidm  18056  psrlidmOLD  18057  mplsubglem  18093  mplsubglemOLD  18095  mplcoe1  18127  mplcoe5lem  18130  mplcoe5  18131  mplcoe2OLD  18133  mplind  18167  mpfind  18205  cply1coe0bi  18342  evls1val  18357  evls1rhm  18359  evl1sca  18370  xrsdsreval  18463  xrsdsreclb  18465  zringmulg  18496  zrngmulg  18503  mulgrhm  18532  mulgrhmOLD  18535  znfld  18599  cygznlem3  18608  remulg  18643  ocvlsp  18707  pjff  18743  pjf2  18745  pjfo  18746  ocvpj  18748  ishil2  18750  frlmsslsp  18829  frlmsslspOLD  18830  islinds2  18848  f1lindf  18857  mat1rngiso  18988  dmatscmcl  19005  scmatscmiddistr  19010  scmatlss  19027  scmatf  19031  scmatf1  19033  mdet0pr  19094  m2detleib  19133  mply1topmatval  19305  tgcl  19471  tgclb  19472  tgss2  19489  tgfiss  19493  opncld  19534  ntrval2  19552  ntrss3  19561  clsidm  19568  ntridm  19569  opnssneib  19616  ssnei2  19617  neindisj  19618  opnnei  19621  innei  19626  resttopon  19662  restcld  19673  restcls  19682  restntr  19683  perfopn  19686  cnpnei  19765  cncls2i  19771  cnntri  19772  cnclsi  19773  lmss  19799  pnrmopn  19844  lpcls  19865  perfcls  19866  cncmp  19892  cmpsublem  19899  cmpsub  19900  consuba  19921  clscon  19931  1stcrest  19954  lly1stc  19997  hauspwdom  20002  lfinpfin  20025  llycmpkgen2  20051  ptclsg  20116  txcnp  20121  txcmplem1  20142  xkococnlem  20160  qtoptopon  20205  qtopid  20206  kqopn  20235  ptunhmeo  20309  trfbas2  20344  trfbas  20345  filin  20355  filintn0  20362  trfil2  20388  fgtr  20391  trufil  20411  cfinufil  20429  elfm3  20451  fmfnfmlem4  20458  neiflim  20475  flfval  20491  flfnei  20492  fclsbas  20522  ptcmplem5  20556  cnextf  20566  cnextfres  20568  tgplacthmeo  20602  tgpconcompeqg  20610  tgpconcomp  20611  tsmssubm  20644  tsmssplit  20654  tsmsxplem1  20655  restutopopn  20741  isucn2  20782  cnextucn  20806  blpnfctr  20939  mopni2  20996  stdbdmopn  21021  met1stc  21024  metutopOLD  21085  psmetutop  21086  nrmmetd  21095  tngngp2  21166  xrsxmet  21314  metdsle  21356  climcncf  21404  icoopnst  21439  iocopnst  21440  cnheibor  21455  bndth  21458  htpyco1  21478  htpyco2  21479  phtpyco2  21490  pi1xfr  21555  pi1coghm  21561  lmmbrf  21701  lmnn  21702  caucfil  21722  cmetcaulem  21727  iscmet3  21732  cfilresi  21734  caussi  21736  causs  21737  lmle  21740  lmclimf  21742  bcthlem4  21766  bcth3  21770  rrxnm  21823  rrxcph  21824  rrxmval  21832  rrxmetlem  21834  rrxmet  21835  rrxdstprj1  21836  minveclem4  21847  ivth2  21867  ivthicc  21870  cniccbdd  21873  ovollb2  21900  ovolctb  21901  ovolunlem1a  21907  ovolunlem1  21908  ovolshftlem1  21920  ovolicc2lem1  21928  ovolicc2lem2  21929  ovolicc2lem4  21931  ovolicc2lem5  21932  uniioombllem2  21992  uniioombllem3  21994  volivth  22016  mbfss  22053  mbflimsup  22073  itg1val2  22091  i1fadd  22102  i1fmul  22103  itg1addlem4  22106  i1fmulc  22110  itg1mulc  22111  mbfi1fseqlem4  22125  itg2const2  22148  itg2seq  22149  itg2splitlem  22155  itg2split  22156  itg2addlem  22165  itg2gt0  22167  itg2cnlem2  22169  iblss  22211  iblss2  22212  itgss3  22221  itgless  22223  itgfsum  22233  itgsplit  22242  itgsplitioo  22244  itgcn  22249  ditgcl  22262  ditgswap  22263  ditgsplitlem  22264  dvconst  22320  dvaddbr  22341  dvmulbr  22342  dvef  22381  rolle  22391  dvlip  22394  dvlipcn  22395  dvlip2  22396  dveq0  22401  dv11cn  22402  dvivthlem1  22409  dvne0  22412  lhop1lem  22414  lhop2  22416  lhop  22417  dvcnvre  22420  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumrlimge0  22431  dvfsumrlim  22432  ftc1lem1  22436  ftc1lem4  22440  ftc1lem5  22441  itgsubstlem  22449  deg1sclle  22513  uc1pmon1p  22552  plymullem  22613  coeeulem  22621  dgrlem  22626  dgrlb  22633  coemulhi  22651  dgrcolem2  22671  plydiveu  22694  vieta1lem2  22707  vieta1  22708  taylplem1  22758  taylplem2  22759  dvtaylp  22765  taylthlem1  22768  taylthlem2  22769  ulmdvlem1  22795  mtest  22799  radcnv0  22811  pserulm  22817  pserdvlem2  22823  abelthlem3  22828  abelthlem5  22830  abelthlem7  22833  efcvx  22844  sineq0  22914  tanord  22925  tanregt0  22926  logne0  22987  argregt0  22995  argimgt0  22997  argimlt0  22998  logneg2  23000  logcnlem3  23025  cxpsqrt  23084  loglesqrt  23132  ang180lem2  23142  isosctrlem1  23152  dcubic  23177  atanlogaddlem  23244  atanlogsub  23247  atantan  23254  atans2  23262  log2tlbnd  23276  birthdaylem2  23282  rlimcnp  23295  efrlim  23299  jensenlem1  23316  jensenlem2  23317  jensen  23318  fsumharmonic  23341  wilthlem2  23343  ftalem4  23349  ftalem5  23350  basellem3  23356  basellem4  23357  ppisval  23377  chtdif  23432  dvdsflsumcom  23464  musumsum  23468  muinv  23469  sgmmul  23476  chtleppi  23485  chtublem  23486  fsumvma  23488  chpval2  23493  chpub  23495  bposlem3  23561  lgsvalmod  23590  lgsdir2  23603  lgsdchr  23623  lgsquadlem2  23630  lgsquad2lem2  23634  chebbnd1lem1  23654  chebbnd1lem3  23656  dchrisumlem1  23674  dchrisumlem2  23675  dchrisumlem3  23676  dchrisum0fno1  23696  rpvmasum2  23697  dchrisum0lem1b  23700  dchrisum0lem1  23701  mulog2sumlem2  23720  chpdifbndlem1  23738  pntrsumbnd2  23752  pntrlog2bndlem6  23768  pntpbnd1  23771  pntlemj  23788  pntlemf  23790  qabvle  23810  padicabv  23815  padicabvcxp  23817  ostth2lem3  23820  lmiisolem  24161  ttgval  24178  colinearalg  24213  axcontlem2  24268  axcontlem7  24273  usgraedg3  24386  usgrarnedg1  24389  fargshiftfo  24638  wwlkm1edg  24735  clwlkisclwwlklem2a  24785  clwlkisclwwlk  24789  wlklenvclwlk  24839  frgrareg  25117  grpoidinvlem2  25207  grpoidinvlem3  25208  grpoideu  25211  grpoinvid1  25232  grpoinvid2  25233  grpolcan  25235  grpo2inv  25241  grpoinvop  25243  grpomuldivass  25251  grpopnpcan2  25255  grponnncan2  25256  grponpncan  25257  gxinv  25272  gxid  25275  ablo4  25289  ablomuldiv  25291  ablodivdiv4  25293  ablonnncan  25295  ablonnncan1  25297  ghgrplem1OLD  25368  ghgrpOLD  25370  ghabloOLD  25371  ghsubgolemOLD  25372  rngolz  25403  rngorz  25404  vc0  25462  vcz  25463  nvzs  25540  nvmdi  25545  nvnegneg  25546  nvsubadd  25550  nvnpcan  25555  nvmeq0  25559  nvabs  25576  nvelbl2  25600  sspmval  25646  sspz  25648  sspival  25651  sspimsval  25653  nmoub3i  25688  nmblolbii  25714  dipsubdir  25763  sspph  25770  ubthlem1  25786  minvecolem3  25792  minvecolem4  25796  htthlem  25834  hvaddsub4  25995  hi2eq  26022  shsel3  26233  pjpreeq  26316  pjeq  26317  chabs1  26434  pjspansn  26495  chscllem1  26555  chscllem2  26556  chscllem4  26558  5oalem2  26573  3oalem2  26581  pjoi0  26635  nmopub2tALT  26828  nmfnleub2  26845  eigvalcl  26880  eighmre  26882  leopmul  27053  nmopleid  27058  opsqrlem4  27062  spansncv2  27212  chcv1  27274  atcv0eq  27298  atexch  27300  chirredi  27313  cdj1i  27352  elabreximd  27408  fpwrelmap  27556  iocinif  27592  toslublem  27655  tosglblem  27657  ressmulgnn  27671  archirngz  27733  slmdvs0  27768  dvrdir  27780  rhmunitinv  27812  kerunit  27813  qtopt1  27838  metider  27873  tpr2rico  27894  fsumcvg4  27932  lmdvg  27935  rezh  27952  qqhvq  27968  logbrec  28021  indsum  28036  indpreima  28038  indf1ofs  28039  esummono  28066  esumpcvgval  28084  esumpmono  28085  esumcvg  28092  sigaclfu2  28121  cldssbrsiga  28158  eulerpartlems  28299  eulerpartlemb  28307  eulerpartlemgvv  28315  eulerpartlemgs2  28319  fibp1  28340  probun  28358  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemsel1i  28451  ballotlemsima  28454  ballotlemfrceq  28467  ballotlemirc  28470  sgnneg  28479  sgnmulrp2  28482  signsply0  28508  signstf0  28525  signsvfn  28539  signsvfpn  28542  signsvfnn  28543  signshf  28545  dmlogdmgm  28566  subfacp1lem4  28627  subfacp1lem5  28628  erdszelem8  28642  ptpcon  28678  cvmliftmolem1  28726  cvmliftmolem2  28727  cvmliftlem6  28735  cvmliftlem7  28736  cvmliftlem10  28739  cvmlift2lem9  28756  cvmlift2lem11  28758  cvmlift2lem12  28759  ghomgsg  29033  ghomf1olem  29034  sinccvglem  29038  lediv2aALT  29043  rtrclreclem.trans  29069  binomfallfaclem2  29162  dfon2lem9  29223  sltval2  29416  outsideofeq  29780  lineelsb2  29798  bpolysum  29815  bpolydiflem  29816  onsuct0  29906  fin2so  30040  mblfinlem2  30052  voliunnfl  30058  volsupnfl  30059  dvtanlem  30064  itg2gt0cn  30070  itgaddnclem2  30074  bddiblnc  30085  ftc1cnnclem  30088  ftc1cnnc  30089  ftc1anclem2  30091  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  ftc2nc  30099  areacirc  30112  opnregcld  30148  isfne  30157  sdclem1  30236  fdc  30238  metf1o  30248  mettrifi  30250  equivtotbnd  30274  isbnd2  30279  bndss  30282  equivbnd2  30288  ismtyima  30299  ismtybndlem  30302  heiborlem1  30307  heiborlem8  30314  ismrer1  30334  ablo4pnp  30342  ghomdiv  30346  rngoneglmul  30354  rngonegrmul  30355  rngosubdi  30356  rngosubdir  30357  isdrngo2  30361  rngohomco  30377  rngoisoco  30385  iscringd  30396  crngm4  30400  idlsubcl  30420  divrngidl  30425  unichnidl  30428  keridl  30429  maxidln1  30441  maxidln0  30442  igenidl  30460  igenidl2  30462  ispridlc  30467  dmncan1  30473  elrfirn2  30628  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  elnn0rabdioph  30736  irrapxlem5  30762  pell14qrre  30793  pell14qrne0  30794  pell14qrmulcl  30799  pellfundex  30822  monotoddzzfi  30878  jm2.17c  30900  fnwe2lem2  30997  flcidc  31123  itgpowd  31182  dvgrat  31193  cvgdvgrat  31194  radcnvrat  31195  lcmcllem  31202  lcmneg  31209  expgrowthi  31238  bccbc  31250  binomcxplemnn0  31254  binomcxplemdvbinom  31258  binomcxplemnotnn0  31261  rfcnpre1  31394  rfcnpre2  31406  monoords  31496  fsumnncl  31572  fmulcl  31575  fmul01lt1lem1  31578  fmul01lt1lem2  31579  climinf  31612  sumnnodd  31636  limcleqr  31650  cncfiooicclem1  31696  cncfioobd  31700  fprodcncf  31704  dvcosax  31723  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnmul  31740  dvmptfprodlem  31741  itgcoscmulx  31768  itgsubsticclem  31774  itgspltprt  31778  stoweidlem11  31793  stoweidlem14  31796  stoweidlem20  31802  stoweidlem26  31808  stoweidlem27  31809  stoweidlem31  31813  stoweidlem48  31830  stoweidlem51  31833  dirkercncflem2  31886  fourierdlem10  31899  fourierdlem11  31900  fourierdlem12  31901  fourierdlem16  31905  fourierdlem20  31909  fourierdlem21  31910  fourierdlem22  31911  fourierdlem31  31920  fourierdlem39  31928  fourierdlem40  31929  fourierdlem42  31931  fourierdlem47  31936  fourierdlem50  31939  fourierdlem64  31953  fourierdlem65  31954  fourierdlem70  31959  fourierdlem73  31962  fourierdlem76  31965  fourierdlem83  31972  fourierdlem93  31982  fourierdlem95  31984  fourierdlem97  31986  fourierdlem101  31990  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem111  32000  fourierdlem114  32003  sqwvfoura  32011  elaa2lem  32016  etransclem32  32049  etransclem35  32052  etransclem46  32063  subsubmgm  32485  equivestrcsetc  32658  setc1strwun  32659  pgrpgt2nabl  32959  invginvrid  32960  lincsumscmcl  33034  onetansqsecsq  33155  bnj594  33970  riotasv3d  34691  lssats  34737  lfl0  34790  lfladdcl  34796  lflvscl  34802  lkr0f  34819  olm11  34952  latm12  34955  cvrle  35003  cvrnle  35005  cvrne  35006  cvrval3  35137  atcvrj0  35152  atltcvr  35159  atbtwnexOLDN  35171  atbtwnex  35172  3at  35214  2atneat  35239  llncvrlpln2  35281  lplncvrlvol2  35339  dalemdnee  35390  linepsubN  35476  isline2  35498  paddasslem17  35560  pmodN  35574  pmapjlln1  35579  pclidN  35620  polval2N  35630  polssatN  35632  polpmapN  35636  2polpmapN  35637  2polvalN  35638  2polssN  35639  3polN  35640  pclss2polN  35645  2pmaplubN  35650  polatN  35655  2polatN  35656  psubclsubN  35664  pmapidclN  35666  ispsubcl2N  35671  linepsubclN  35675  polsubclN  35676  lhpoc2N  35739  ltrnlaut  35847  ltrncnv  35870  cdlemc3  35918  cdleme3b  35954  cdleme42ke  36211  trlcoat  36449  tendoid  36499  tendoex  36701  dvalveclem  36752  diaintclN  36785  diasslssN  36786  dvhgrp  36834  dvhlveclem  36835  docaclN  36851  diaocN  36852  doca2N  36853  doca3N  36854  dvadiaN  36855  djaclN  36863  djajN  36864  dibval2  36871  dibvalrel  36890  dibintclN  36894  dicvalrelN  36912  xihopellsmN  36981  dihopellsm  36982  dihsslss  37003  dih1  37013  dih1dimatlem  37056  dihlspsnat  37060  dihintcl  37071  dihmeetcl  37072  dochval2  37079  dochcl  37080  dochlss  37081  dochssv  37082  dochvalr  37084  dochvalr2  37089  dochocss  37093  dochoc  37094  dochnoncon  37118  djhcl  37127  djhlj  37128  djhexmid  37138  dvh3dim3N  37176  lcfrlem21  37290  hlhilhillem  37690
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 185  df-an 371
  Copyright terms: Public domain W3C validator