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

Theorem syldan 458
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  |-  ( (
ph  /\  ps )  ->  ch )
syldan.2  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
syldan  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem syldan
StepHypRef Expression
1 syldan.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 syldan.2 . . . 4  |-  ( (
ph  /\  ch )  ->  th )
32expcom 426 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 456 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 35 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  sylan2  462  sbcied2  3200  csbied2  3296  elpw2g  4366  pofun  4522  elpwunsn  4760  fnbr  5550  dffv2  5799  fnexALT  5965  grprinvlem  6288  caofid0l  6335  caofid0r  6336  caofid1  6337  caofid2  6338  caofcom  6339  frxp  6459  fnse  6466  brovex  6477  riotasv3d  6601  tfr3  6663  tz7.48-2  6702  oaf1o  6809  omlimcl  6824  oeeulem  6847  ixpexg  7089  f1domg  7130  domdifsn  7194  unxpdom2  7320  xpfir  7334  fofinf1o  7390  fofi  7395  imafi  7402  intrnfi  7424  ordtypelem6  7495  oiexg  7507  cantnfp1lem3  7639  cantnflem1  7648  infxpenlem  7900  fseqenlem2  7911  ssnum  7925  acni2  7932  finacn  7936  fonum  7944  infpwfien  7948  inffien  7949  infunsdom1  8098  infunsdom  8099  ackbij1lem12  8116  cfslb2n  8153  fin23lem28  8225  compssiso  8259  isf34lem5  8263  fin56  8278  axcc3  8323  axdc3lem2  8336  ttukeylem6  8399  ttukeylem7  8400  brdom3  8411  gchdomtri  8509  fpwwe2lem13  8522  gchxpidm  8549  tsken  8634  tsksn  8640  tsk1  8644  tsk2  8645  2domtsk  8646  tskcard  8661  r1tskina  8662  gruss  8676  gruxp  8687  gruina  8698  grur1a  8699  ltaddpr  8916  ltexprlem7  8924  1idsr  8978  addgt0sr  8984  recexsr  8987  msqgt0  9553  mulgt1  9874  gt0div  9881  ge0div  9882  ltdiv2  9900  ltrec1  9902  lerec2  9903  lediv2  9905  lediv12a  9908  recreclt  9914  creur  9999  nn2ge  10030  avgle1  10212  recnz  10350  suprzcl  10354  uzwo2  10546  rpnnen1lem5  10609  xrrege0  10767  xlemul1a  10872  xrsupsslem  10890  xrinfmsslem  10891  supxr2  10897  supxrpnf  10902  supxrunb1  10903  supxrunb2  10904  ixxun  10937  peano2fzor  11199  ioopnfsup  11250  modcl  11258  modge0  11262  zmodcl  11271  seqcl  11348  seqf  11349  seqfveq  11352  sermono  11360  seqsplit  11361  seqcaopr2  11364  seqf1olem2  11368  seqf1o  11369  seqhomo  11375  seqz  11376  le2sq2  11462  faclbnd4lem3  11591  bcpasc  11617  hashgt0  11667  seqcoll  11717  seqcoll2  11718  ccatlid  11753  ccatass  11755  ccatswrd  11778  wrdeqcats1  11793  wrdeqs1cat  11794  revccat  11803  revrev  11804  sqrlem7  12059  resqrex  12061  sqrgt0  12069  leabs  12109  absmax  12138  r19.2uz  12160  lo1bdd2  12323  o1lo12  12337  rlimclim1  12344  lo1eq  12367  rlimeq  12368  rlimcn1  12387  rlimcn2  12389  rlimdiv  12444  rlimsqzlem  12447  clim2ser  12453  clim2ser2  12454  climub  12460  isercolllem1  12463  isercolllem3  12465  isercoll2  12467  climsup  12468  serf0  12479  iseraltlem1  12480  fsumf1o  12522  fsumss  12524  fsumsplit  12538  fsum2dlem  12559  fsumless  12580  fsumabs  12585  fsumtscopo  12586  fsumparts  12590  fsumrlim  12595  fsumo1  12596  o1fsum  12597  cvgcmp  12600  cvgcmpce  12602  fsumiun  12605  binom1dif  12617  incexclem  12621  incexc  12622  isumsplit  12625  isumrpcl  12628  isumless  12630  isumsup2  12631  isumltss  12633  climcnds  12636  supcvg  12640  expcnv  12648  explecnv  12649  geomulcvg  12658  cvgrat  12665  mertenslem1  12666  efcllem  12685  ef0lem  12686  eftlub  12715  tanval3  12740  tanneg  12754  rpnnen2lem7  12825  rpnnen2lem9  12827  rpnnen2lem11  12829  ruclem9  12842  dvdssubr  12896  divalgmod  12931  bitsf1  12963  algfx  13076  eucalgcvga  13082  isprm6  13114  phimullem  13173  eulerthlem2  13176  pcid  13251  pcgcd  13256  unbenlem  13281  prmreclem4  13292  prmreclem5  13293  4sqlem9  13319  4sqlem15  13332  4sqlem16  13333  vdwlem2  13355  vdwlem6  13359  vdwlem10  13363  vdwlem11  13364  vdwlem13  13366  ramval  13381  ressabs  13532  imasaddflem  13760  imasvscaf  13769  mrcid  13843  mrcidb  13845  mrcidm  13849  fucidcl  14167  setcmon  14247  setcepi  14248  catccatid  14262  xpccatid  14290  yonedalem4c  14379  yonedainv  14383  pospo  14435  latjlej1  14499  latmlem1  14515  latledi  14523  latj32  14531  latjjdi  14537  mrelatlub  14617  mreclat  14618  psss  14651  tsrlemax  14657  spwpr4c  14669  grpidd  14723  ismndd  14724  issubmnd  14729  subsubm  14762  gsumress  14782  gsumval2  14788  grpinvid1  14858  grpinvid2  14859  grplcan  14862  grpinvinv  14863  grpinvval2  14877  mulgass  14925  mulgpropd  14928  subginv  14956  subgmulg  14963  issubg2  14964  issubg4  14966  subsubg  14968  eqger  14995  divsinv  15004  resghm  15027  pwsdiagghm  15038  conjsubgen  15043  conjnsg  15046  subgga  15082  gass  15083  gasubg  15084  orbstafun  15093  orbsta  15095  gexcl2  15228  gexdvds3  15229  sylow1lem2  15238  sylow2blem1  15259  pj1ghm  15340  frgpup1  15412  frgpup3lem  15414  cntzspan  15465  cyggeninv  15498  lt6abl  15509  cycsubgcyg  15515  gsumval3eu  15518  gsumval3  15519  gsumzres  15522  gsumzaddlem  15531  gsumzsplit  15534  gsum2d  15551  gsum2d2lem  15552  dprdres  15591  dprdz  15593  dmdprdsplitlem  15600  dprdcntz2  15601  dprddisj2  15602  dprd2dlem1  15604  dmdprdsplit2lem  15608  dmdprdsplit2  15609  dprdsplit  15611  ablfac1c  15634  ablfac1eulem  15635  ablfac1eu  15636  pgpfac1lem2  15638  ablfac2  15652  rngidss  15695  isrngd  15703  rnglz  15705  rngrz  15706  gsumdixp  15720  0unit  15790  unitnegcl  15791  rnginvdv  15804  invrpropd  15808  subrg1  15883  subrginv  15889  issubrg2  15893  subsubrg  15899  abvneg  15927  lmod0vs  15988  lmodvs0  15989  lmodvneg1  15992  islss3  16040  lspsnsubg  16061  lspidm  16067  lspsnneg  16087  lmhmlsp  16130  drngnidl  16305  psrass1lem  16447  psrlinv  16466  psrlidm  16472  mplsubglem  16503  mplcoe1  16533  mplcoe2  16535  mplind  16567  xrsdsreval  16748  xrsdsreclb  16750  mulgrhm  16792  znfld  16846  cygznlem3  16855  ocvlsp  16908  pjff  16944  pjf2  16946  pjfo  16947  ocvpj  16949  ishil2  16951  tgcl  17039  tgclb  17040  tgss2  17057  tgfiss  17061  opncld  17102  ntrval2  17120  ntrss3  17129  clsidm  17136  ntridm  17137  opnssneib  17184  ssnei2  17185  neindisj  17186  opnnei  17189  innei  17194  resttopon  17230  restcld  17241  restcls  17250  restntr  17251  perfopn  17254  cnpnei  17333  cncls2i  17339  cnntri  17340  cnclsi  17341  lmss  17367  pnrmopn  17412  lpcls  17433  perfcls  17434  cncmp  17460  cmpsublem  17467  cmpsub  17468  consuba  17488  clscon  17498  1stcrest  17521  lly1stc  17564  hauspwdom  17569  llycmpkgen2  17587  ptclsg  17652  txcnp  17657  txcmplem1  17678  xkococnlem  17696  qtoptopon  17741  qtopid  17742  kqopn  17771  ptunhmeo  17845  trfbas2  17880  trfbas  17881  filin  17891  filintn0  17898  trfil2  17924  fgtr  17927  trufil  17947  cfinufil  17965  elfm3  17987  fmfnfmlem4  17994  neiflim  18011  flfval  18027  flfnei  18028  fclsbas  18058  ptcmplem5  18092  cnextf  18102  cnextfres  18104  tgplacthmeo  18138  tgpconcompeqg  18146  tgpconcomp  18147  tsmssubm  18177  tsmssplit  18186  tsmsxplem1  18187  restutopopn  18273  isucn2  18314  cnextucn  18338  blpnfctr  18471  mopni2  18528  stdbdmopn  18553  met1stc  18556  metutopOLD  18617  psmetutop  18618  nrmmetd  18627  tngngp2  18698  xrsxmet  18845  metdsle  18887  climcncf  18935  icoopnst  18969  iocopnst  18970  cnheibor  18985  bndth  18988  htpyco1  19008  htpyco2  19009  phtpyco2  19020  pi1xfr  19085  pi1coghm  19091  lmmbrf  19220  lmnn  19221  caucfil  19241  cmetcaulem  19246  iscmet3  19251  cfilresi  19253  caussi  19255  causs  19256  lmle  19259  lmclimf  19261  bcthlem4  19285  bcth3  19289  minveclem4  19338  ivth2  19357  ivthicc  19360  cniccbdd  19363  ovollb2  19390  ovolctb  19391  ovolunlem1a  19397  ovolunlem1  19398  ovolshftlem1  19410  ovolicc2lem1  19418  ovolicc2lem2  19419  ovolicc2lem4  19421  ovolicc2lem5  19422  uniioombllem2  19480  uniioombllem3  19482  volivth  19504  mbfss  19541  mbflimsup  19561  itg1val2  19579  i1fadd  19590  i1fmul  19591  itg1addlem4  19594  i1fmulc  19598  itg1mulc  19599  mbfi1fseqlem4  19613  itg2const2  19636  itg2seq  19637  itg2splitlem  19643  itg2split  19644  itg2addlem  19653  itg2gt0  19655  itg2cnlem2  19657  iblss  19699  iblss2  19700  itgss3  19709  itgless  19711  itgfsum  19721  itgsplit  19730  itgsplitioo  19732  itgcn  19737  ditgcl  19750  ditgswap  19751  ditgsplitlem  19752  dvconst  19808  dvaddbr  19829  dvmulbr  19830  rolle  19879  dvlip  19882  dvlipcn  19883  dvlip2  19884  dveq0  19889  dv11cn  19890  dvivthlem1  19897  dvne0  19900  lhop1lem  19902  lhop2  19904  lhop  19905  dvcnvre  19908  dvfsumle  19910  dvfsumge  19911  dvfsumabs  19912  dvfsumlem2  19916  dvfsumlem3  19917  dvfsumrlimge0  19919  dvfsumrlim  19920  ftc1lem1  19924  ftc1lem4  19928  ftc1lem5  19929  itgsubstlem  19937  evl1sca  19955  mpfind  19970  deg1sclle  20040  uc1pmon1p  20079  plymullem  20140  coeeulem  20148  dgrlem  20153  dgrlb  20160  coemulhi  20177  dgrcolem2  20197  plydiveu  20220  vieta1lem2  20233  vieta1  20234  taylplem1  20284  taylplem2  20285  dvtaylp  20291  taylthlem1  20294  taylthlem2  20295  ulmdvlem1  20321  mtest  20325  radcnv0  20337  pserulm  20343  pserdvlem2  20349  abelthlem3  20354  abelthlem5  20356  abelthlem7  20359  efcvx  20370  sineq0  20434  tanord  20445  tanregt0  20446  logne0  20502  argregt0  20510  argimgt0  20512  argimlt0  20513  logneg2  20515  logcnlem3  20540  cxpsqr  20599  loglesqr  20647  ang180lem2  20657  isosctrlem1  20667  dcubic  20691  atanlogaddlem  20758  atanlogsub  20761  atantan  20768  atans2  20776  log2tlbnd  20790  birthdaylem2  20796  rlimcnp  20809  efrlim  20813  jensenlem1  20830  jensenlem2  20831  jensen  20832  fsumharmonic  20855  wilthlem2  20857  ftalem4  20863  ftalem5  20864  basellem3  20870  basellem4  20871  ppisval  20891  chtdif  20946  dvdsflsumcom  20978  musumsum  20982  muinv  20983  sgmmul  20990  chtleppi  20999  chtublem  21000  fsumvma  21002  chpval2  21007  chpub  21009  bposlem3  21075  lgsvalmod  21104  lgsdir2  21117  lgsdchr  21137  lgsquadlem2  21144  lgsquad2lem2  21148  chebbnd1lem1  21168  chebbnd1lem3  21170  dchrisumlem1  21188  dchrisumlem2  21189  dchrisumlem3  21190  dchrisum0fno1  21210  rpvmasum2  21211  dchrisum0lem1b  21214  dchrisum0lem1  21215  mulog2sumlem2  21234  chpdifbndlem1  21252  pntrsumbnd2  21266  pntrlog2bndlem6  21282  pntpbnd1  21285  pntlemj  21302  pntlemf  21304  qabvle  21324  padicabv  21329  padicabvcxp  21331  ostth2lem3  21334  usgraedg3  21410  usgrarnedg1  21413  fargshiftfo  21630  grpoidinvlem2  21798  grpoidinvlem3  21799  grpoideu  21802  grpoinvid1  21823  grpoinvid2  21824  grpolcan  21826  grpo2inv  21832  grpoinvop  21834  grpomuldivass  21842  grpopnpcan2  21846  grponnncan2  21847  grponpncan  21848  gxinv  21863  gxid  21866  ablo4  21880  ablomuldiv  21882  ablodivdiv4  21884  ablonnncan  21886  ablonnncan1  21888  ghgrplem1  21959  ghgrp  21961  ghablo  21962  ghsubgolem  21963  rngolz  21994  rngorz  21995  vc0  22053  vcz  22054  nvzs  22131  nvmdi  22136  nvnegneg  22137  nvsubadd  22141  nvnpcan  22146  nvmeq0  22150  nvabs  22167  nvelbl2  22191  sspmval  22237  sspz  22239  sspival  22242  sspimsval  22244  nmoub3i  22279  nmblolbii  22305  dipsubdir  22354  sspph  22361  ubthlem1  22377  minvecolem3  22383  minvecolem4  22387  htthlem  22425  hvaddsub4  22585  hi2eq  22612  shsel3  22822  pjpreeq  22905  pjeq  22906  chabs1  23023  pjspansn  23084  chscllem1  23144  chscllem2  23145  chscllem4  23147  5oalem2  23162  3oalem2  23170  pjoi0  23224  nmopub2tALT  23417  nmfnleub2  23434  eigvalcl  23469  eighmre  23471  leopmul  23642  nmopleid  23647  opsqrlem4  23651  spansncv2  23801  chcv1  23863  atcv0eq  23887  atexch  23889  chirredi  23902  cdj1i  23941  elabreximd  23996  abfmpeld  24071  iocinif  24149  ressmulgnn  24210  dvrdir  24231  rhmunitinv  24265  kerunit  24266  zzsmulg  24270  remulg  24275  metider  24294  tpr2rico  24315  lmdvg  24343  rezh  24360  qqhvq  24376  logbrec  24410  indsum  24425  indpreima  24427  indf1ofs  24428  esummono  24455  esumpcvgval  24473  esumpmono  24474  esumcvg  24481  sigaclfu2  24509  cldssbrsiga  24546  probun  24682  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemsel1i  24775  ballotlemsima  24778  ballotlemfrceq  24791  ballotlemirc  24794  dmlogdmgm  24813  subfacp1lem4  24874  subfacp1lem5  24875  erdszelem8  24889  ptpcon  24925  cvmliftmolem1  24973  cvmliftmolem2  24974  cvmliftlem6  24982  cvmliftlem7  24983  cvmliftlem10  24986  cvmlift2lem9  25003  cvmlift2lem11  25005  cvmlift2lem12  25006  ghomgsg  25109  ghomf1olem  25110  sinccvglem  25114  lediv2aALT  25122  rtrclreclem.trans  25151  clim2prod  25221  clim2div  25222  ntrivcvgfvn0  25232  ntrivcvgmullem  25234  fprodf1o  25277  prodss  25278  fprodss  25279  fprodser  25280  fprodsplit  25294  fprodeq0  25304  fprod2dlem  25309  binomfallfaclem2  25361  dfon2lem9  25423  sltval2  25616  colinearalg  25854  axcontlem2  25909  axcontlem7  25914  outsideofeq  26069  lineelsb2  26087  bpolysum  26104  bpolydiflem  26105  onsuct0  26196  mblfinlem2  26256  voliunnfl  26262  volsupnfl  26263  dvtanlem  26268  itg2gt0cn  26274  itgaddnclem2  26278  bddiblnc  26289  ftc1cnnclem  26292  ftc1cnnc  26293  ftc1anclem2  26295  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  ftc2nc  26303  areacirc  26311  opnregcld  26347  isfne  26362  lfinpfin  26397  sdclem1  26461  fdc  26463  metf1o  26475  mettrifi  26477  equivtotbnd  26501  isbnd2  26506  bndss  26509  equivbnd2  26515  ismtyima  26526  ismtybndlem  26529  heiborlem1  26534  heiborlem8  26541  ismrer1  26561  ablo4pnp  26569  ghomdiv  26573  rngoneglmul  26581  rngonegrmul  26582  rngosubdi  26583  rngosubdir  26584  isdrngo2  26588  rngohomco  26604  rngoisoco  26612  iscringd  26623  crngm4  26627  idlsubcl  26647  divrngidl  26652  unichnidl  26655  keridl  26656  maxidln1  26668  maxidln0  26669  igenidl  26687  igenidl2  26689  ispridlc  26694  dmncan1  26700  elrfirn2  26764  2rexfrabdioph  26870  3rexfrabdioph  26871  4rexfrabdioph  26872  6rexfrabdioph  26873  7rexfrabdioph  26874  elnn0rabdioph  26877  irrapxlem5  26903  pell14qrre  26934  pell14qrne0  26935  pell14qrmulcl  26940  pellfundex  26963  monotoddzzfi  27019  jm2.17c  27041  fnwe2lem2  27140  frlmsslsp  27239  islinds2  27274  f1lindf  27283  flcidc  27370  psgnunilem5  27408  expgrowthi  27541  rfcnpre1  27680  rfcnpre2  27692  fmulcl  27701  fmul01lt1lem1  27704  fmul01lt1lem2  27705  climinf  27722  stoweidlem11  27750  stoweidlem14  27753  stoweidlem20  27759  stoweidlem26  27765  stoweidlem27  27766  stoweidlem31  27770  stoweidlem48  27787  stoweidlem51  27790  wrdsymb1  28206  wrdlenccats1lenm1  28212  ccats1swrdid  28225  swrdccatin2  28244  2cshwmod  28291  lstccats1fst  28297  swrdtrcfvl  28299  onetansqsecsq  28578  bnj594  29357  lssats  29884  lfl0  29937  lfladdcl  29943  lflvscl  29949  lkr0f  29966  olm11  30099  latm12  30102  cvrle  30150  cvrnle  30152  cvrne  30153  cvrval3  30284  atcvrj0  30299  atltcvr  30306  atbtwnexOLDN  30318  atbtwnex  30319  3at  30361  2atneat  30386  llncvrlpln2  30428  lplncvrlvol2  30486  dalemdnee  30537  linepsubN  30623  isline2  30645  paddasslem17  30707  pmodN  30721  pmapjlln1  30726  pclidN  30767  polval2N  30777  polssatN  30779  polpmapN  30783  2polpmapN  30784  2polvalN  30785  2polssN  30786  3polN  30787  pclss2polN  30792  2pmaplubN  30797  polatN  30802  2polatN  30803  psubclsubN  30811  pmapidclN  30813  ispsubcl2N  30818  linepsubclN  30822  polsubclN  30823  lhpoc2N  30886  ltrnlaut  30994  ltrncnv  31017  cdlemc3  31064  cdleme3b  31100  cdleme42ke  31356  trlcoat  31594  tendoid  31644  tendoex  31846  dvalveclem  31897  diaintclN  31930  diasslssN  31931  dvhgrp  31979  dvhlveclem  31980  docaclN  31996  diaocN  31997  doca2N  31998  doca3N  31999  dvadiaN  32000  djaclN  32008  djajN  32009  dibval2  32016  dibvalrel  32035  dibintclN  32039  dicvalrelN  32057  xihopellsmN  32126  dihopellsm  32127  dihsslss  32148  dih1  32158  dih1dimatlem  32201  dihlspsnat  32205  dihintcl  32216  dihmeetcl  32217  dochval2  32224  dochcl  32225  dochlss  32226  dochssv  32227  dochvalr  32229  dochvalr2  32234  dochocss  32238  dochoc  32239  dochnoncon  32263  djhcl  32272  djhlj  32273  djhexmid  32283  dvh3dim3N  32321  lcfrlem21  32435  hlhilhillem  32835
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 179  df-an 362
  Copyright terms: Public domain W3C validator