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

Theorem syldan 456
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 424 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 454 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 32 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sylan2  460  sbcied2  3029  csbied2  3125  elpw2g  4168  pofun  4329  elpwunsn  4567  fnbr  5312  dffv2  5554  fnexALT  5704  grprinvlem  6020  caofid0l  6067  caofid0r  6068  caofid1  6069  caofid2  6070  caofcom  6071  frxp  6187  fnse  6194  riotasv3d  6349  tfr3  6411  tz7.48-2  6450  oaf1o  6557  omlimcl  6572  oeeulem  6595  ixpexg  6836  f1domg  6877  domdifsn  6941  unxpdom2  7067  xpfir  7081  fofinf1o  7133  fofi  7138  imafi  7144  intrnfi  7166  ordtypelem6  7234  oiexg  7246  cantnfp1lem3  7378  cantnflem1  7387  infxpenlem  7637  fseqenlem2  7648  ssnum  7662  acni2  7669  finacn  7673  fonum  7681  infpwfien  7685  inffien  7686  infunsdom1  7835  infunsdom  7836  ackbij1lem12  7853  cfslb2n  7890  fin23lem28  7962  compssiso  7996  isf34lem5  8000  fin56  8015  axcc3  8060  axdc3lem2  8073  ttukeylem6  8137  ttukeylem7  8138  brdom3  8149  gchdomtri  8247  fpwwe2lem13  8260  gchxpidm  8287  tsken  8372  tsksn  8378  tsk1  8382  tsk2  8383  2domtsk  8384  tskcard  8399  r1tskina  8400  gruss  8414  gruxp  8425  gruina  8436  grur1a  8437  ltaddpr  8654  ltexprlem7  8662  1idsr  8716  addgt0sr  8722  recexsr  8725  msqgt0  9290  mulgt1  9611  gt0div  9618  ge0div  9619  ltdiv2  9637  ltrec1  9639  lerec2  9640  lediv2  9642  lediv12a  9645  recreclt  9651  creur  9736  nn2ge  9767  avgle1  9947  recnz  10083  suprzcl  10087  uzwo2  10279  rpnnen1lem5  10342  xrrege0  10499  xlemul1a  10604  xrsupsslem  10621  xrinfmsslem  10622  supxr2  10628  supxrpnf  10633  supxrunb1  10634  supxrunb2  10635  ixxun  10668  peano2fzor  10915  ioopnfsup  10964  modcl  10972  modge0  10976  zmodcl  10985  seqcl  11062  seqf  11063  seqfveq  11066  sermono  11074  seqsplit  11075  seqcaopr2  11078  seqf1olem2  11082  seqf1o  11083  seqhomo  11089  seqz  11090  le2sq2  11175  faclbnd4lem3  11304  bcpasc  11329  seqcoll  11397  seqcoll2  11398  ccatlid  11430  ccatass  11432  ccatswrd  11455  wrdeqcats1  11470  wrdeqs1cat  11471  revccat  11480  revrev  11481  sqrlem7  11730  resqrex  11732  sqrgt0  11740  leabs  11780  absmax  11809  r19.2uz  11831  lo1bdd2  11994  o1lo12  12008  rlimclim1  12015  lo1eq  12038  rlimeq  12039  rlimcn1  12058  rlimcn2  12060  rlimdiv  12115  rlimsqzlem  12118  clim2ser  12124  clim2ser2  12125  climub  12131  isercolllem1  12134  isercolllem3  12136  isercoll2  12138  climsup  12139  serf0  12149  iseraltlem1  12150  fsumf1o  12192  fsumss  12194  fsumsplit  12208  fsum2dlem  12229  fsumless  12250  fsumabs  12255  fsumtscopo  12256  fsumparts  12260  fsumrlim  12265  fsumo1  12266  o1fsum  12267  cvgcmp  12270  cvgcmpce  12272  fsumiun  12275  binom1dif  12287  incexclem  12291  incexc  12292  isumsplit  12295  isumrpcl  12298  isumless  12300  isumsup2  12301  isumltss  12303  climcnds  12306  supcvg  12310  expcnv  12318  explecnv  12319  geomulcvg  12328  cvgrat  12335  mertenslem1  12336  efcllem  12355  ef0lem  12356  eftlub  12385  tanval3  12410  tanneg  12424  rpnnen2lem7  12495  rpnnen2lem9  12497  rpnnen2lem11  12499  ruclem9  12512  dvdssubr  12566  divalgmod  12601  bitsf1  12633  algfx  12746  eucalgcvga  12752  isprm6  12784  phimullem  12843  eulerthlem2  12846  pcid  12921  pcgcd  12926  unbenlem  12951  prmreclem4  12962  prmreclem5  12963  4sqlem9  12989  4sqlem15  13002  4sqlem16  13003  vdwlem2  13025  vdwlem6  13029  vdwlem10  13033  vdwlem11  13034  vdwlem13  13036  ramval  13051  ressabs  13202  imasaddflem  13428  imasvscaf  13437  mrcid  13511  mrcidb  13513  mrcidm  13517  fucidcl  13835  setcmon  13915  setcepi  13916  catccatid  13930  xpccatid  13958  yonedalem4c  14047  yonedainv  14051  pospo  14103  latjlej1  14167  latmlem1  14183  latledi  14191  latj32  14199  latjjdi  14205  ipoval  14253  mrelatlub  14285  mreclat  14286  psss  14319  tsrlemax  14325  spwpr4c  14337  grpidd  14391  ismndd  14392  issubmnd  14397  subsubm  14430  gsumress  14450  gsumval2  14456  grpinvid1  14526  grpinvid2  14527  grplcan  14530  grpinvinv  14531  grpinvval2  14545  mulgass  14593  mulgpropd  14596  subginv  14624  subgmulg  14631  issubg2  14632  issubg4  14634  subsubg  14636  eqger  14663  divsinv  14672  resghm  14695  pwsdiagghm  14706  conjsubgen  14711  conjnsg  14714  subgga  14750  gass  14751  gasubg  14752  orbstafun  14761  orbsta  14763  gexcl2  14896  gexdvds3  14897  sylow1lem2  14906  sylow2blem1  14927  pj1ghm  15008  frgpup1  15080  frgpup3lem  15082  cntzspan  15133  cyggeninv  15166  lt6abl  15177  cycsubgcyg  15183  gsumval3eu  15186  gsumval3  15187  gsumzres  15190  gsumzaddlem  15199  gsumzsplit  15202  gsum2d  15219  gsum2d2lem  15220  dprdres  15259  dprdz  15261  dmdprdsplitlem  15268  dprdcntz2  15269  dprddisj2  15270  dprd2dlem1  15272  dmdprdsplit2lem  15276  dmdprdsplit2  15277  dprdsplit  15279  ablfac1c  15302  ablfac1eulem  15303  ablfac1eu  15304  pgpfac1lem2  15306  ablfac2  15320  rngidss  15363  isrngd  15371  rnglz  15373  rngrz  15374  gsumdixp  15388  0unit  15458  unitnegcl  15459  rnginvdv  15472  invrpropd  15476  subrg1  15551  subrginv  15557  issubrg2  15561  subsubrg  15567  abvneg  15595  lmod0vs  15659  lmodvs0  15660  lmodvneg1  15663  islss3  15712  lspsnsubg  15733  lspidm  15739  lspsnneg  15759  lmhmlsp  15802  drngnidl  15977  psrass1lem  16119  psrlinv  16138  psrlidm  16144  mplsubglem  16175  mplcoe1  16205  mplcoe2  16207  mplind  16239  xrsdsreval  16412  xrsdsreclb  16414  mulgrhm  16456  znfld  16510  cygznlem3  16519  ocvlsp  16572  pjff  16608  pjf2  16610  pjfo  16611  ocvpj  16613  ishil2  16615  tgcl  16703  tgclb  16704  tgss2  16721  tgfiss  16725  opncld  16766  ntrval2  16784  ntrss3  16793  clsidm  16800  ntridm  16801  opnssneib  16848  ssnei2  16849  neindisj  16850  opnnei  16853  innei  16858  resttopon  16888  restcld  16899  restcls  16907  restntr  16908  perfopn  16911  cnpnei  16989  cncls2i  16995  cnntri  16996  cnclsi  16997  lmss  17022  pnrmopn  17067  lpcls  17088  perfcls  17089  cncmp  17115  cmpsublem  17122  cmpsub  17123  consuba  17142  clscon  17152  1stcrest  17175  lly1stc  17218  hauspwdom  17223  llycmpkgen2  17241  ptclsg  17305  txcnp  17310  txcmplem1  17331  xkococnlem  17349  qtoptopon  17391  qtopid  17392  kqopn  17421  ptunhmeo  17495  trfbas2  17534  trfbas  17535  filin  17545  filintn0  17552  trfil2  17578  fgtr  17581  trufil  17601  cfinufil  17619  elfm3  17641  fmfnfmlem4  17648  neiflim  17665  flfval  17681  flfnei  17682  fclsbas  17712  ptcmplem5  17746  tgplacthmeo  17782  tgpconcompeqg  17790  tgpconcomp  17791  tsmssubm  17821  tsmssplit  17830  tsmsxplem1  17831  blpnfctr  17978  mopni2  18035  stdbdmopn  18060  met1stc  18063  nrmmetd  18093  tngngp2  18164  xrsxmet  18311  metdsle  18352  climcncf  18400  icoopnst  18433  iocopnst  18434  cnheibor  18449  bndth  18452  htpyco1  18472  htpyco2  18473  phtpyco2  18484  pi1xfr  18549  pi1coghm  18555  lmmbrf  18684  lmnn  18685  caucfil  18705  cmetcaulem  18710  iscmet3  18715  cfilresi  18717  caussi  18719  causs  18720  lmle  18723  lmclimf  18725  bcthlem4  18745  bcth3  18749  minveclem4  18792  ivth2  18811  ivthicc  18814  cniccbdd  18817  ovollb2  18844  ovolctb  18845  ovolunlem1a  18851  ovolunlem1  18852  ovolshftlem1  18864  ovolicc2lem1  18872  ovolicc2lem2  18873  ovolicc2lem4  18875  ovolicc2lem5  18876  uniioombllem2  18934  uniioombllem3  18936  volivth  18958  mbfss  18997  mbflimsup  19017  itg1val2  19035  i1fadd  19046  i1fmul  19047  itg1addlem4  19050  i1fmulc  19054  itg1mulc  19055  mbfi1fseqlem4  19069  itg2const2  19092  itg2seq  19093  itg2splitlem  19099  itg2split  19100  itg2addlem  19109  itg2gt0  19111  itg2cnlem2  19113  iblss  19155  iblss2  19156  itgss3  19165  itgless  19167  itgfsum  19177  itgsplit  19186  itgsplitioo  19188  itgcn  19193  ditgcl  19204  ditgswap  19205  ditgsplitlem  19206  dvconst  19262  dvaddbr  19283  dvmulbr  19284  dvcnvlem  19319  rolle  19333  dvlip  19336  dvlipcn  19337  dvlip2  19338  dveq0  19343  dv11cn  19344  dvivthlem1  19351  dvne0  19354  lhop1lem  19356  lhop2  19358  lhop  19359  dvcnvre  19362  dvfsumle  19364  dvfsumge  19365  dvfsumabs  19366  dvfsumlem2  19370  dvfsumlem3  19371  dvfsumrlimge0  19373  dvfsumrlim  19374  ftc1lem1  19378  ftc1lem4  19382  ftc1lem5  19383  itgsubstlem  19391  evl1sca  19409  mpfind  19424  deg1sclle  19494  plymullem  19594  coeeulem  19602  dgrlem  19607  dgrlb  19614  coemulhi  19631  dgrcolem2  19651  plydiveu  19674  vieta1lem2  19687  vieta1  19688  taylplem1  19738  taylplem2  19739  dvtaylp  19745  taylthlem1  19748  taylthlem2  19749  ulmdvlem1  19773  mtest  19777  radcnv0  19788  pserulm  19794  pserdvlem2  19800  abelthlem3  19805  abelthlem5  19807  abelthlem7  19810  efcvx  19821  sineq0  19885  tanord  19896  tanregt0  19897  logne0  19952  argregt0  19960  argimgt0  19962  argimlt0  19963  logneg2  19965  logcnlem3  19987  cxpsqr  20046  loglesqr  20094  ang180lem2  20104  isosctrlem1  20114  dcubic  20138  atanlogaddlem  20205  atanlogsub  20208  atantan  20215  atans2  20223  log2tlbnd  20237  birthdaylem2  20243  rlimcnp  20256  efrlim  20260  jensenlem1  20277  jensenlem2  20278  jensen  20279  fsumharmonic  20301  wilthlem2  20303  ftalem4  20309  ftalem5  20310  basellem3  20316  basellem4  20317  ppisval  20337  chtdif  20392  dvdsflsumcom  20424  musumsum  20428  muinv  20429  sgmmul  20436  chtleppi  20445  chtublem  20446  fsumvma  20448  chpval2  20453  chpub  20455  bposlem3  20521  lgsvalmod  20550  lgsdir2  20563  lgsdchr  20583  lgsquadlem2  20590  lgsquad2lem2  20594  chebbnd1lem1  20614  chebbnd1lem3  20616  dchrisumlem1  20634  dchrisumlem2  20635  dchrisumlem3  20636  dchrisum0fno1  20656  rpvmasum2  20657  dchrisum0lem1b  20660  dchrisum0lem1  20661  mulog2sumlem2  20680  chpdifbndlem1  20698  pntrsumbnd2  20712  pntrlog2bndlem6  20728  pntpbnd1  20731  pntlemj  20748  pntlemf  20750  qabvle  20770  padicabv  20775  padicabvcxp  20777  ostth2lem3  20780  grpoidinvlem2  20866  grpoidinvlem3  20867  grpoideu  20870  grpoinvid1  20891  grpoinvid2  20892  grpolcan  20894  grpo2inv  20900  grpoinvop  20902  grpomuldivass  20910  grpopnpcan2  20914  grponnncan2  20915  grponpncan  20916  gxinv  20931  gxid  20934  ablo4  20948  ablomuldiv  20950  ablodivdiv4  20952  ablonnncan  20954  ablonnncan1  20956  ghgrplem1  21027  ghgrp  21029  ghablo  21030  ghsubgolem  21031  rngolz  21062  rngorz  21063  vc0  21119  vcz  21120  nvzs  21197  nvmdi  21202  nvnegneg  21203  nvsubadd  21207  nvnpcan  21212  nvmeq0  21216  nvabs  21233  nvelbl2  21257  sspmval  21303  sspz  21305  sspival  21308  sspimsval  21310  nmoub3i  21345  nmblolbii  21371  dipsubdir  21420  sspph  21427  ubthlem1  21443  minvecolem3  21449  minvecolem4  21453  htthlem  21491  hvaddsub4  21653  hi2eq  21680  shsel3  21890  pjpreeq  21973  pjeq  21974  chabs1  22091  pjspansn  22152  chscllem1  22212  chscllem2  22213  chscllem4  22215  5oalem2  22230  3oalem2  22238  pjoi0  22292  nmopub2tALT  22485  nmfnleub2  22502  eigvalcl  22537  eighmre  22539  leopmul  22710  nmopleid  22715  opsqrlem4  22719  spansncv2  22869  chcv1  22931  atcv0eq  22955  atexch  22957  chirredi  22970  cdj1i  23009  elabreximd  23035  ballotlemfp1  23046  ballotlemimin  23060  ballotlemsel1i  23067  ballotlemsima  23070  ballotlemfrceq  23083  ballotlemirc  23086  subfacp1lem4  23121  subfacp1lem5  23122  erdszelem8  23136  ptpcon  23171  cvmliftmolem1  23219  cvmliftmolem2  23220  cvmliftlem6  23228  cvmliftlem7  23229  cvmliftlem10  23232  cvmlift2lem9  23249  cvmlift2lem11  23251  cvmlift2lem12  23252  ghomgsg  23407  ghomf1olem  23408  sinccvglem  23412  lediv2aALT  23420  rtrclreclem.trans  23450  dfon2lem9  23551  sltval2  23713  colinearalg  23948  axcontlem2  24003  axcontlem7  24008  outsideofeq  24163  lineelsb2  24181  bpolysum  24198  bpolydiflem  24199  onsuct0  24290  areacirc  24341  fprod1fi  24737  grpodrcan  24786  ltrinvlem  24817  invaddvec  24878  dblsubvec  24885  mvecrtol2  24888  basexre  24933  intopcoaconb  24951  qusp  24953  cntrset  25013  msr4  25017  lvsovso  25037  lvsovso3  25039  dmrngcmp  25162  dualcat2  25195  idfisf  25252  prismorcsetlem  25323  isgraphmrph  25334  idmor  25357  domidmor  25359  codidmor  25361  grphidmor  25363  grphidmor3  25365  cmp2morpcats  25372  cmpidmor2  25380  cmpidmor3  25381  lemindclsbu  25406  isconc2  25418  opnregcld  25659  isfne  25679  lfinpfin  25714  sdclem1  25864  fdc  25866  metf1o  25880  mettrifi  25884  equivtotbnd  25913  isbnd2  25918  bndss  25921  equivbnd2  25927  ismtyima  25938  ismtybndlem  25941  heiborlem1  25946  heiborlem8  25953  ismrer1  25973  ablo4pnp  25981  ghomdiv  25985  rngoneglmul  25993  rngonegrmul  25994  rngosubdi  25995  rngosubdir  25996  isdrngo2  26000  rngohomco  26016  rngoisoco  26024  iscringd  26035  crngm4  26039  idlsubcl  26059  divrngidl  26064  unichnidl  26067  keridl  26068  maxidln1  26080  maxidln0  26081  igenidl  26099  igenidl2  26101  ispridlc  26106  dmncan1  26112  elrfirn2  26182  2rexfrabdioph  26288  3rexfrabdioph  26289  4rexfrabdioph  26290  6rexfrabdioph  26291  7rexfrabdioph  26292  elnn0rabdioph  26295  irrapxlem5  26322  pell14qrre  26353  pell14qrne0  26354  pell14qrmulcl  26359  pellfundex  26382  monotoddzzfi  26438  jm2.17c  26460  fnwe2lem2  26559  frlmsslsp  26659  islinds2  26694  f1lindf  26703  flcidc  26790  psgnunilem5  26828  expgrowthi  26961  sumpair  27117  climinf  27143  stoweidlem26  27186  stoweidlem27  27187  stoweidlem61  27221  onetansqsecsq  27503  bnj594  28223  lssats  28481  lfl0  28534  lfladdcl  28540  lflvscl  28546  lkr0f  28563  olm11  28696  latm12  28699  cvrle  28747  cvrnle  28749  cvrne  28750  cvrval3  28881  atcvrj0  28896  atltcvr  28903  atbtwnexOLDN  28915  atbtwnex  28916  3at  28958  2atneat  28983  llncvrlpln2  29025  lplncvrlvol2  29083  dalemdnee  29134  linepsubN  29220  isline2  29242  paddasslem17  29304  pmodN  29318  pmapjlln1  29323  pclidN  29364  polval2N  29374  polssatN  29376  polpmapN  29380  2polpmapN  29381  2polvalN  29382  2polssN  29383  3polN  29384  pclss2polN  29389  2pmaplubN  29394  polatN  29399  2polatN  29400  psubclsubN  29408  pmapidclN  29410  ispsubcl2N  29415  linepsubclN  29419  polsubclN  29420  lhpoc2N  29483  ltrnlaut  29591  ltrncnv  29614  cdlemc3  29661  cdleme3b  29697  cdleme42ke  29953  trlcoat  30191  tendoid  30241  tendoex  30443  dvalveclem  30494  diaintclN  30527  diasslssN  30528  dvhgrp  30576  dvhlveclem  30577  docaclN  30593  diaocN  30594  doca2N  30595  doca3N  30596  dvadiaN  30597  djaclN  30605  djajN  30606  dibval2  30613  dibvalrel  30632  dibintclN  30636  dicvalrelN  30654  xihopellsmN  30723  dihopellsm  30724  dihsslss  30745  dih1  30755  dih1dimatlem  30798  dihlspsnat  30802  dihintcl  30813  dihmeetcl  30814  dochval2  30821  dochcl  30822  dochlss  30823  dochssv  30824  dochvalr  30826  dochvalr2  30831  dochocss  30835  dochoc  30836  dochnoncon  30860  djhcl  30869  djhlj  30870  djhexmid  30880  dvh3dim3N  30918  lcfrlem21  31032  hlhilhillem  31432
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator