MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syldan Structured version   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  |-  ( (
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 435 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 468 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 36 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  sylan2  474  thema2a  1581  sbcied2  3219  csbied2  3310  elpwunsn  3912  elpw2g  4450  pofun  4652  fnbr  5508  dffv2  5759  grprinvlem  6296  caofid0l  6343  caofid0r  6344  caofid1  6345  caofid2  6346  caofcom  6347  fnexALT  6538  frxp  6677  fnse  6684  brovex  6735  tfr3  6850  tz7.48-2  6889  oaf1o  6994  omlimcl  7009  oeeulem  7032  ixpexg  7279  f1domg  7321  domdifsn  7386  unxpdom2  7513  xpfir  7527  fofinf1o  7584  fofi  7589  imafi  7596  intrnfi  7658  ordtypelem6  7729  oiexg  7741  cantnfp1lem3  7880  cantnflem1  7889  cantnfp1lem3OLD  7906  cantnflem1OLD  7912  infxpenlem  8172  fseqenlem2  8187  ssnum  8201  acni2  8208  finacn  8212  fonum  8220  infpwfien  8224  inffien  8225  infunsdom1  8374  infunsdom  8375  ackbij1lem12  8392  cfslb2n  8429  fin23lem28  8501  compssiso  8535  isf34lem5  8539  fin56  8554  axcc3  8599  axdc3lem2  8612  ttukeylem6  8675  ttukeylem7  8676  brdom3  8687  gchdomtri  8788  fpwwe2lem13  8801  gchxpidm  8828  tsken  8913  tsksn  8919  tsk1  8923  tsk2  8924  2domtsk  8925  tskcard  8940  r1tskina  8941  gruss  8955  gruxp  8966  gruina  8977  grur1a  8978  ltaddpr  9195  ltexprlem7  9203  1idsr  9257  addgt0sr  9263  recexsr  9266  msqgt0  9852  mulgt1  10180  gt0div  10187  ge0div  10188  ltdiv2  10209  ltrec1  10211  lerec2  10212  lediv2  10214  lediv12a  10217  recreclt  10223  creur  10308  nn2ge  10339  avgle1  10556  recnz  10709  suprzcl  10713  uzwo2  10911  rpnnen1lem5  10975  xrrege0  11138  xlemul1a  11243  xrsupsslem  11261  xrinfmsslem  11262  supxr2  11268  supxrpnf  11273  supxrunb1  11274  supxrunb2  11275  ixxun  11308  peano2fzor  11624  ioopnfsup  11695  modcl  11704  modge0  11709  zmodcl  11719  seqcl  11818  seqf  11819  seqfveq  11822  sermono  11830  seqsplit  11831  seqcaopr2  11834  seqf1olem2  11838  seqf1o  11839  seqhomo  11845  seqz  11846  le2sq2  11933  faclbnd4lem3  12063  bcpasc  12089  hashgt0  12143  hashge2el2dif  12176  seqcoll  12208  seqcoll2  12209  wrdsymb1  12254  ccatlid  12276  ccatass  12278  swrdtrcfvl  12336  swrdlsw  12338  2swrd1eqwrdeq  12340  ccatswrd  12342  swrd0swrd  12347  swrdccatwrd  12354  wrdeqcats1  12360  wrdeqs1cat  12361  swrdccatin2  12370  revccat  12398  revrev  12399  sqrlem7  12730  resqrex  12732  sqrgt0  12740  leabs  12780  absmax  12809  r19.2uz  12831  lo1bdd2  12994  o1lo12  13008  rlimclim1  13015  lo1eq  13038  rlimeq  13039  rlimcn1  13058  rlimcn2  13060  rlimdiv  13115  rlimsqzlem  13118  clim2ser  13124  clim2ser2  13125  climub  13131  isercolllem1  13134  isercolllem3  13136  isercoll2  13138  climsup  13139  serf0  13150  iseraltlem1  13151  fsumf1o  13192  fsumss  13194  fsumsplit  13208  fsum2dlem  13229  fsumless  13251  fsumabs  13256  fsumtscopo  13257  fsumparts  13261  fsumrlim  13266  fsumo1  13267  o1fsum  13268  cvgcmp  13271  cvgcmpce  13273  fsumiun  13276  binom1dif  13288  incexclem  13291  incexc  13292  isumsplit  13295  isumrpcl  13298  isumless  13300  isumsup2  13301  isumltss  13303  climcnds  13306  supcvg  13310  expcnv  13318  explecnv  13319  geomulcvg  13328  cvgrat  13335  mertenslem1  13336  efcllem  13355  ef0lem  13356  eftlub  13385  tanval3  13410  tanneg  13424  rpnnen2lem7  13495  rpnnen2lem9  13497  rpnnen2lem11  13499  ruclem9  13512  dvdssubr  13566  divalgmod  13602  bitsf1  13634  algfx  13747  eucalgcvga  13753  isprm6  13787  phimullem  13846  eulerthlem2  13849  pcid  13931  pcgcd  13936  unbenlem  13961  prmreclem4  13972  prmreclem5  13973  4sqlem9  13999  4sqlem15  14012  4sqlem16  14013  vdwlem2  14035  vdwlem6  14039  vdwlem10  14043  vdwlem11  14044  vdwlem13  14046  ramval  14061  ressabs  14228  imasaddflem  14460  imasvscaf  14469  mrcid  14543  mrcidb  14545  mrcidm  14549  fucidcl  14867  setcmon  14947  setcepi  14948  catccatid  14962  xpccatid  14990  yonedalem4c  15079  yonedainv  15083  pospo  15135  latjlej1  15227  latmlem1  15243  latledi  15251  latj32  15259  latjjdi  15265  mrelatlub  15348  mreclatBAD  15349  psss  15376  tsrlemax  15382  grpidd  15435  ismndd  15436  issubmnd  15441  subsubm  15476  gsumress  15498  gsumval2  15504  grpinvid1  15577  grpinvid2  15578  grplcan  15581  grpinvinv  15584  grpinvval2  15600  mulgass  15648  mulgpropd  15651  subginv  15679  subgmulg  15686  issubg2  15687  issubg4  15691  subsubg  15695  eqger  15722  divsinv  15731  resghm  15754  pwsdiagghm  15765  conjsubgen  15770  conjnsg  15773  subgga  15809  gass  15810  gasubg  15811  orbstafun  15820  orbsta  15822  symgextfv  15914  psgnunilem5  15991  gexcl2  16079  gexdvds3  16080  sylow1lem2  16089  sylow2blem1  16110  pj1ghm  16191  frgpup1  16263  frgpup3lem  16265  cntzspan  16317  cyggeninv  16351  lt6abl  16362  cycsubgcyg  16368  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumzres  16379  gsumzresOLD  16383  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumzsplit  16409  gsumzsplitOLD  16410  gsum2d  16451  gsum2dOLD  16452  gsum2d2lem  16453  dprdres  16513  dprdz  16515  dmdprdsplitlem  16522  dmdprdsplitlemOLD  16523  dprdcntz2  16524  dprddisj2  16525  dprddisj2OLD  16526  dprd2dlem1  16528  dmdprdsplit2lem  16532  dmdprdsplit2  16533  dprdsplit  16535  ablfac1c  16560  ablfac1eulem  16561  ablfac1eu  16562  pgpfac1lem2  16564  ablfac2  16578  rngidss  16659  isrngd  16667  rnglz  16669  rngrz  16670  gsumdixpOLD  16688  gsumdixp  16689  0unit  16760  unitnegcl  16761  rnginvdv  16774  invrpropd  16778  subrg1  16853  subrginv  16859  issubrg2  16863  subsubrg  16869  abvneg  16897  lmod0vs  16959  lmodvs0  16960  lmodvneg1  16966  islss3  17017  lspsnsubg  17038  lspidm  17044  lspsnneg  17064  lmhmlsp  17107  drngnidl  17288  psrass1lem  17424  psrlinv  17445  psrlidm  17451  psrlidmOLD  17452  mplsubglem  17487  mplsubglemOLD  17489  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  mplind  17559  mpfind  17597  evls1val  17730  evls1rhm  17732  evl1sca  17743  xrsdsreval  17833  xrsdsreclb  17835  zringmulg  17866  zrngmulg  17872  mulgrhm  17901  mulgrhmOLD  17904  znfld  17968  cygznlem3  17977  remulg  18012  ocvlsp  18076  pjff  18112  pjf2  18114  pjfo  18115  ocvpj  18117  ishil2  18119  frlmsslsp  18198  frlmsslspOLD  18199  islinds2  18217  f1lindf  18226  mdet0pr  18378  m2detleib  18412  tgcl  18549  tgclb  18550  tgss2  18567  tgfiss  18571  opncld  18612  ntrval2  18630  ntrss3  18639  clsidm  18646  ntridm  18647  opnssneib  18694  ssnei2  18695  neindisj  18696  opnnei  18699  innei  18704  resttopon  18740  restcld  18751  restcls  18760  restntr  18761  perfopn  18764  cnpnei  18843  cncls2i  18849  cnntri  18850  cnclsi  18851  lmss  18877  pnrmopn  18922  lpcls  18943  perfcls  18944  cncmp  18970  cmpsublem  18977  cmpsub  18978  consuba  18999  clscon  19009  1stcrest  19032  lly1stc  19075  hauspwdom  19080  llycmpkgen2  19098  ptclsg  19163  txcnp  19168  txcmplem1  19189  xkococnlem  19207  qtoptopon  19252  qtopid  19253  kqopn  19282  ptunhmeo  19356  trfbas2  19391  trfbas  19392  filin  19402  filintn0  19409  trfil2  19435  fgtr  19438  trufil  19458  cfinufil  19476  elfm3  19498  fmfnfmlem4  19505  neiflim  19522  flfval  19538  flfnei  19539  fclsbas  19569  ptcmplem5  19603  cnextf  19613  cnextfres  19615  tgplacthmeo  19649  tgpconcompeqg  19657  tgpconcomp  19658  tsmssubm  19691  tsmssplit  19701  tsmsxplem1  19702  restutopopn  19788  isucn2  19829  cnextucn  19853  blpnfctr  19986  mopni2  20043  stdbdmopn  20068  met1stc  20071  metutopOLD  20132  psmetutop  20133  nrmmetd  20142  tngngp2  20213  xrsxmet  20361  metdsle  20403  climcncf  20451  icoopnst  20486  iocopnst  20487  cnheibor  20502  bndth  20505  htpyco1  20525  htpyco2  20526  phtpyco2  20537  pi1xfr  20602  pi1coghm  20608  lmmbrf  20748  lmnn  20749  caucfil  20769  cmetcaulem  20774  iscmet3  20779  cfilresi  20781  caussi  20783  causs  20784  lmle  20787  lmclimf  20789  bcthlem4  20813  bcth3  20817  rrxnm  20870  rrxcph  20871  rrxmval  20879  rrxmetlem  20881  rrxmet  20882  rrxdstprj1  20883  minveclem4  20894  ivth2  20914  ivthicc  20917  cniccbdd  20920  ovollb2  20947  ovolctb  20948  ovolunlem1a  20954  ovolunlem1  20955  ovolshftlem1  20967  ovolicc2lem1  20975  ovolicc2lem2  20976  ovolicc2lem4  20978  ovolicc2lem5  20979  uniioombllem2  21038  uniioombllem3  21040  volivth  21062  mbfss  21099  mbflimsup  21119  itg1val2  21137  i1fadd  21148  i1fmul  21149  itg1addlem4  21152  i1fmulc  21156  itg1mulc  21157  mbfi1fseqlem4  21171  itg2const2  21194  itg2seq  21195  itg2splitlem  21201  itg2split  21202  itg2addlem  21211  itg2gt0  21213  itg2cnlem2  21215  iblss  21257  iblss2  21258  itgss3  21267  itgless  21269  itgfsum  21279  itgsplit  21288  itgsplitioo  21290  itgcn  21295  ditgcl  21308  ditgswap  21309  ditgsplitlem  21310  dvconst  21366  dvaddbr  21387  dvmulbr  21388  rolle  21437  dvlip  21440  dvlipcn  21441  dvlip2  21442  dveq0  21447  dv11cn  21448  dvivthlem1  21455  dvne0  21458  lhop1lem  21460  lhop2  21462  lhop  21463  dvcnvre  21466  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  dvfsumlem2  21474  dvfsumlem3  21475  dvfsumrlimge0  21477  dvfsumrlim  21478  ftc1lem1  21482  ftc1lem4  21486  ftc1lem5  21487  itgsubstlem  21495  deg1sclle  21559  uc1pmon1p  21598  plymullem  21659  coeeulem  21667  dgrlem  21672  dgrlb  21679  coemulhi  21696  dgrcolem2  21716  plydiveu  21739  vieta1lem2  21752  vieta1  21753  taylplem1  21803  taylplem2  21804  dvtaylp  21810  taylthlem1  21813  taylthlem2  21814  ulmdvlem1  21840  mtest  21844  radcnv0  21856  pserulm  21862  pserdvlem2  21868  abelthlem3  21873  abelthlem5  21875  abelthlem7  21878  efcvx  21889  sineq0  21958  tanord  21969  tanregt0  21970  logne0  22026  argregt0  22034  argimgt0  22036  argimlt0  22037  logneg2  22039  logcnlem3  22064  cxpsqr  22123  loglesqr  22171  ang180lem2  22181  isosctrlem1  22191  dcubic  22216  atanlogaddlem  22283  atanlogsub  22286  atantan  22293  atans2  22301  log2tlbnd  22315  birthdaylem2  22321  rlimcnp  22334  efrlim  22338  jensenlem1  22355  jensenlem2  22356  jensen  22357  fsumharmonic  22380  wilthlem2  22382  ftalem4  22388  ftalem5  22389  basellem3  22395  basellem4  22396  ppisval  22416  chtdif  22471  dvdsflsumcom  22503  musumsum  22507  muinv  22508  sgmmul  22515  chtleppi  22524  chtublem  22525  fsumvma  22527  chpval2  22532  chpub  22534  bposlem3  22600  lgsvalmod  22629  lgsdir2  22642  lgsdchr  22662  lgsquadlem2  22669  lgsquad2lem2  22673  chebbnd1lem1  22693  chebbnd1lem3  22695  dchrisumlem1  22713  dchrisumlem2  22714  dchrisumlem3  22715  dchrisum0fno1  22735  rpvmasum2  22736  dchrisum0lem1b  22739  dchrisum0lem1  22740  mulog2sumlem2  22759  chpdifbndlem1  22777  pntrsumbnd2  22791  pntrlog2bndlem6  22807  pntpbnd1  22810  pntlemj  22827  pntlemf  22829  qabvle  22849  padicabv  22854  padicabvcxp  22856  ostth2lem3  22859  ttgval  23072  colinearalg  23107  axcontlem2  23162  axcontlem7  23167  usgraedg3  23255  usgrarnedg1  23258  fargshiftfo  23475  grpoidinvlem2  23643  grpoidinvlem3  23644  grpoideu  23647  grpoinvid1  23668  grpoinvid2  23669  grpolcan  23671  grpo2inv  23677  grpoinvop  23679  grpomuldivass  23687  grpopnpcan2  23691  grponnncan2  23692  grponpncan  23693  gxinv  23708  gxid  23711  ablo4  23725  ablomuldiv  23727  ablodivdiv4  23729  ablonnncan  23731  ablonnncan1  23733  ghgrplem1  23804  ghgrp  23806  ghablo  23807  ghsubgolem  23808  rngolz  23839  rngorz  23840  vc0  23898  vcz  23899  nvzs  23976  nvmdi  23981  nvnegneg  23982  nvsubadd  23986  nvnpcan  23991  nvmeq0  23995  nvabs  24012  nvelbl2  24036  sspmval  24082  sspz  24084  sspival  24087  sspimsval  24089  nmoub3i  24124  nmblolbii  24150  dipsubdir  24199  sspph  24206  ubthlem1  24222  minvecolem3  24228  minvecolem4  24232  htthlem  24270  hvaddsub4  24431  hi2eq  24458  shsel3  24669  pjpreeq  24752  pjeq  24753  chabs1  24870  pjspansn  24931  chscllem1  24991  chscllem2  24992  chscllem4  24994  5oalem2  25009  3oalem2  25017  pjoi0  25071  nmopub2tALT  25264  nmfnleub2  25281  eigvalcl  25316  eighmre  25318  leopmul  25489  nmopleid  25494  opsqrlem4  25498  spansncv2  25648  chcv1  25710  atcv0eq  25734  atexch  25736  chirredi  25749  cdj1i  25788  elabreximd  25842  iocinif  26022  ressmulgnn  26095  archirngz  26157  slmdvs0  26192  dvrdir  26209  rhmunitinv  26241  kerunit  26242  metider  26273  tpr2rico  26294  fsumcvg4  26332  lmdvg  26335  rezh  26352  qqhvq  26368  logbrec  26416  indsum  26431  indpreima  26433  indf1ofs  26434  esummono  26461  esumpcvgval  26479  esumpmono  26480  esumcvg  26487  sigaclfu2  26516  cldssbrsiga  26553  eulerpartlems  26695  eulerpartlemb  26703  eulerpartlemgvv  26711  eulerpartlemgs2  26715  probun  26754  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemsel1i  26847  ballotlemsima  26850  ballotlemfrceq  26863  ballotlemirc  26866  sgnneg  26875  sgnmulrp2  26878  signsply0  26904  signslema  26915  signstf0  26921  signsvfn  26935  signsvfpn  26938  signsvfnn  26939  signshf  26941  dmlogdmgm  26962  subfacp1lem4  27023  subfacp1lem5  27024  erdszelem8  27038  ptpcon  27074  cvmliftmolem1  27122  cvmliftmolem2  27123  cvmliftlem6  27131  cvmliftlem7  27132  cvmliftlem10  27135  cvmlift2lem9  27152  cvmlift2lem11  27154  cvmlift2lem12  27155  ghomgsg  27263  ghomf1olem  27264  sinccvglem  27268  lediv2aALT  27273  rtrclreclem.trans  27299  clim2prod  27354  clim2div  27355  ntrivcvgfvn0  27365  ntrivcvgmullem  27367  fprodf1o  27410  prodss  27411  fprodss  27412  fprodser  27413  fprodsplit  27427  fprodeq0  27437  fprod2dlem  27442  binomfallfaclem2  27494  dfon2lem9  27555  sltval2  27748  outsideofeq  28112  lineelsb2  28130  bpolysum  28147  bpolydiflem  28148  onsuct0  28239  fin2so  28369  mblfinlem2  28382  voliunnfl  28388  volsupnfl  28389  dvtanlem  28394  itg2gt0cn  28400  itgaddnclem2  28404  bddiblnc  28415  ftc1cnnclem  28418  ftc1cnnc  28419  ftc1anclem2  28421  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  ftc2nc  28429  areacirc  28442  opnregcld  28478  isfne  28493  lfinpfin  28528  sdclem1  28592  fdc  28594  metf1o  28604  mettrifi  28606  equivtotbnd  28630  isbnd2  28635  bndss  28638  equivbnd2  28644  ismtyima  28655  ismtybndlem  28658  heiborlem1  28663  heiborlem8  28670  ismrer1  28690  ablo4pnp  28698  ghomdiv  28702  rngoneglmul  28710  rngonegrmul  28711  rngosubdi  28712  rngosubdir  28713  isdrngo2  28717  rngohomco  28733  rngoisoco  28741  iscringd  28752  crngm4  28756  idlsubcl  28776  divrngidl  28781  unichnidl  28784  keridl  28785  maxidln1  28797  maxidln0  28798  igenidl  28816  igenidl2  28818  ispridlc  28823  dmncan1  28829  elrfirn2  28985  2rexfrabdioph  29087  3rexfrabdioph  29088  4rexfrabdioph  29089  6rexfrabdioph  29090  7rexfrabdioph  29091  elnn0rabdioph  29094  irrapxlem5  29120  pell14qrre  29151  pell14qrne0  29152  pell14qrmulcl  29157  pellfundex  29180  monotoddzzfi  29236  jm2.17c  29258  fnwe2lem2  29357  flcidc  29484  itgpowd  29543  expgrowthi  29560  rfcnpre1  29694  rfcnpre2  29706  fmulcl  29715  fmul01lt1lem1  29718  fmul01lt1lem2  29719  climinf  29732  stoweidlem11  29759  stoweidlem14  29762  stoweidlem20  29768  stoweidlem26  29774  stoweidlem27  29775  stoweidlem31  29779  stoweidlem48  29796  stoweidlem51  29799  fsummsnunz  30194  wwlkm1edg  30320  clwlkisclwwlklem2a  30400  clwlkisclwwlk  30404  wrdnval  30427  wlkp1lenfislenp  30465  frgrareg  30663  pgrpgt2nabel  30720  invginvrid  30723  01eq0rng  30728  lincsumscmcl  30856  onetansqsecsq  30985  bnj594  31792  riotasv3d  32451  lssats  32497  lfl0  32550  lfladdcl  32556  lflvscl  32562  lkr0f  32579  olm11  32712  latm12  32715  cvrle  32763  cvrnle  32765  cvrne  32766  cvrval3  32897  atcvrj0  32912  atltcvr  32919  atbtwnexOLDN  32931  atbtwnex  32932  3at  32974  2atneat  32999  llncvrlpln2  33041  lplncvrlvol2  33099  dalemdnee  33150  linepsubN  33236  isline2  33258  paddasslem17  33320  pmodN  33334  pmapjlln1  33339  pclidN  33380  polval2N  33390  polssatN  33392  polpmapN  33396  2polpmapN  33397  2polvalN  33398  2polssN  33399  3polN  33400  pclss2polN  33405  2pmaplubN  33410  polatN  33415  2polatN  33416  psubclsubN  33424  pmapidclN  33426  ispsubcl2N  33431  linepsubclN  33435  polsubclN  33436  lhpoc2N  33499  ltrnlaut  33607  ltrncnv  33630  cdlemc3  33677  cdleme3b  33713  cdleme42ke  33969  trlcoat  34207  tendoid  34257  tendoex  34459  dvalveclem  34510  diaintclN  34543  diasslssN  34544  dvhgrp  34592  dvhlveclem  34593  docaclN  34609  diaocN  34610  doca2N  34611  doca3N  34612  dvadiaN  34613  djaclN  34621  djajN  34622  dibval2  34629  dibvalrel  34648  dibintclN  34652  dicvalrelN  34670  xihopellsmN  34739  dihopellsm  34740  dihsslss  34761  dih1  34771  dih1dimatlem  34814  dihlspsnat  34818  dihintcl  34829  dihmeetcl  34830  dochval2  34837  dochcl  34838  dochlss  34839  dochssv  34840  dochvalr  34842  dochvalr2  34847  dochocss  34851  dochoc  34852  dochnoncon  34876  djhcl  34885  djhlj  34886  djhexmid  34896  dvh3dim3N  34934  lcfrlem21  35048  hlhilhillem  35448
  Copyright terms: Public domain W3C validator