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  3114  csbied2  3210  elpw2g  4276  pofun  4433  elpwunsn  4671  fnbr  5451  dffv2  5699  fnexALT  5862  grprinvlem  6185  caofid0l  6232  caofid0r  6233  caofid1  6234  caofid2  6235  caofcom  6236  frxp  6353  fnse  6360  brovex  6371  riotasv3d  6495  tfr3  6557  tz7.48-2  6596  oaf1o  6703  omlimcl  6718  oeeulem  6741  ixpexg  6983  f1domg  7024  domdifsn  7088  unxpdom2  7214  xpfir  7228  fofinf1o  7284  fofi  7289  imafi  7295  intrnfi  7317  ordtypelem6  7385  oiexg  7397  cantnfp1lem3  7529  cantnflem1  7538  infxpenlem  7788  fseqenlem2  7799  ssnum  7813  acni2  7820  finacn  7824  fonum  7832  infpwfien  7836  inffien  7837  infunsdom1  7986  infunsdom  7987  ackbij1lem12  8004  cfslb2n  8041  fin23lem28  8113  compssiso  8147  isf34lem5  8151  fin56  8166  axcc3  8211  axdc3lem2  8224  ttukeylem6  8288  ttukeylem7  8289  brdom3  8300  gchdomtri  8398  fpwwe2lem13  8411  gchxpidm  8438  tsken  8523  tsksn  8529  tsk1  8533  tsk2  8534  2domtsk  8535  tskcard  8550  r1tskina  8551  gruss  8565  gruxp  8576  gruina  8587  grur1a  8588  ltaddpr  8805  ltexprlem7  8813  1idsr  8867  addgt0sr  8873  recexsr  8876  msqgt0  9441  mulgt1  9762  gt0div  9769  ge0div  9770  ltdiv2  9788  ltrec1  9790  lerec2  9791  lediv2  9793  lediv12a  9796  recreclt  9802  creur  9887  nn2ge  9918  avgle1  10100  recnz  10238  suprzcl  10242  uzwo2  10434  rpnnen1lem5  10497  xrrege0  10655  xlemul1a  10760  xrsupsslem  10778  xrinfmsslem  10779  supxr2  10785  supxrpnf  10790  supxrunb1  10791  supxrunb2  10792  ixxun  10825  peano2fzor  11081  ioopnfsup  11132  modcl  11140  modge0  11144  zmodcl  11153  seqcl  11230  seqf  11231  seqfveq  11234  sermono  11242  seqsplit  11243  seqcaopr2  11246  seqf1olem2  11250  seqf1o  11251  seqhomo  11257  seqz  11258  le2sq2  11344  faclbnd4lem3  11473  bcpasc  11499  hashgt0  11549  seqcoll  11599  seqcoll2  11600  ccatlid  11635  ccatass  11637  ccatswrd  11660  wrdeqcats1  11675  wrdeqs1cat  11676  revccat  11685  revrev  11686  sqrlem7  11941  resqrex  11943  sqrgt0  11951  leabs  11991  absmax  12020  r19.2uz  12042  lo1bdd2  12205  o1lo12  12219  rlimclim1  12226  lo1eq  12249  rlimeq  12250  rlimcn1  12269  rlimcn2  12271  rlimdiv  12326  rlimsqzlem  12329  clim2ser  12335  clim2ser2  12336  climub  12342  isercolllem1  12345  isercolllem3  12347  isercoll2  12349  climsup  12350  serf0  12361  iseraltlem1  12362  fsumf1o  12404  fsumss  12406  fsumsplit  12420  fsum2dlem  12441  fsumless  12462  fsumabs  12467  fsumtscopo  12468  fsumparts  12472  fsumrlim  12477  fsumo1  12478  o1fsum  12479  cvgcmp  12482  cvgcmpce  12484  fsumiun  12487  binom1dif  12499  incexclem  12503  incexc  12504  isumsplit  12507  isumrpcl  12510  isumless  12512  isumsup2  12513  isumltss  12515  climcnds  12518  supcvg  12522  expcnv  12530  explecnv  12531  geomulcvg  12540  cvgrat  12547  mertenslem1  12548  efcllem  12567  ef0lem  12568  eftlub  12597  tanval3  12622  tanneg  12636  rpnnen2lem7  12707  rpnnen2lem9  12709  rpnnen2lem11  12711  ruclem9  12724  dvdssubr  12778  divalgmod  12813  bitsf1  12845  algfx  12958  eucalgcvga  12964  isprm6  12996  phimullem  13055  eulerthlem2  13058  pcid  13133  pcgcd  13138  unbenlem  13163  prmreclem4  13174  prmreclem5  13175  4sqlem9  13201  4sqlem15  13214  4sqlem16  13215  vdwlem2  13237  vdwlem6  13241  vdwlem10  13245  vdwlem11  13246  vdwlem13  13248  ramval  13263  ressabs  13414  imasaddflem  13642  imasvscaf  13651  mrcid  13725  mrcidb  13727  mrcidm  13731  fucidcl  14049  setcmon  14129  setcepi  14130  catccatid  14144  xpccatid  14172  yonedalem4c  14261  yonedainv  14265  pospo  14317  latjlej1  14381  latmlem1  14397  latledi  14405  latj32  14413  latjjdi  14419  ipoval  14467  mrelatlub  14499  mreclat  14500  psss  14533  tsrlemax  14539  spwpr4c  14551  grpidd  14605  ismndd  14606  issubmnd  14611  subsubm  14644  gsumress  14664  gsumval2  14670  grpinvid1  14740  grpinvid2  14741  grplcan  14744  grpinvinv  14745  grpinvval2  14759  mulgass  14807  mulgpropd  14810  subginv  14838  subgmulg  14845  issubg2  14846  issubg4  14848  subsubg  14850  eqger  14877  divsinv  14886  resghm  14909  pwsdiagghm  14920  conjsubgen  14925  conjnsg  14928  subgga  14964  gass  14965  gasubg  14966  orbstafun  14975  orbsta  14977  gexcl2  15110  gexdvds3  15111  sylow1lem2  15120  sylow2blem1  15141  pj1ghm  15222  frgpup1  15294  frgpup3lem  15296  cntzspan  15347  cyggeninv  15380  lt6abl  15391  cycsubgcyg  15397  gsumval3eu  15400  gsumval3  15401  gsumzres  15404  gsumzaddlem  15413  gsumzsplit  15416  gsum2d  15433  gsum2d2lem  15434  dprdres  15473  dprdz  15475  dmdprdsplitlem  15482  dprdcntz2  15483  dprddisj2  15484  dprd2dlem1  15486  dmdprdsplit2lem  15490  dmdprdsplit2  15491  dprdsplit  15493  ablfac1c  15516  ablfac1eulem  15517  ablfac1eu  15518  pgpfac1lem2  15520  ablfac2  15534  rngidss  15577  isrngd  15585  rnglz  15587  rngrz  15588  gsumdixp  15602  0unit  15672  unitnegcl  15673  rnginvdv  15686  invrpropd  15690  subrg1  15765  subrginv  15771  issubrg2  15775  subsubrg  15781  abvneg  15809  lmod0vs  15873  lmodvs0  15874  lmodvneg1  15877  islss3  15926  lspsnsubg  15947  lspidm  15953  lspsnneg  15973  lmhmlsp  16016  drngnidl  16191  psrass1lem  16333  psrlinv  16352  psrlidm  16358  mplsubglem  16389  mplcoe1  16419  mplcoe2  16421  mplind  16453  xrsdsreval  16633  xrsdsreclb  16635  mulgrhm  16677  znfld  16731  cygznlem3  16740  ocvlsp  16793  pjff  16829  pjf2  16831  pjfo  16832  ocvpj  16834  ishil2  16836  tgcl  16924  tgclb  16925  tgss2  16942  tgfiss  16946  opncld  16987  ntrval2  17005  ntrss3  17014  clsidm  17021  ntridm  17022  opnssneib  17069  ssnei2  17070  neindisj  17071  opnnei  17074  innei  17079  resttopon  17109  restcld  17120  restcls  17128  restntr  17129  perfopn  17132  cnpnei  17210  cncls2i  17216  cnntri  17217  cnclsi  17218  lmss  17243  pnrmopn  17288  lpcls  17309  perfcls  17310  cncmp  17336  cmpsublem  17343  cmpsub  17344  consuba  17363  clscon  17373  1stcrest  17396  lly1stc  17439  hauspwdom  17444  llycmpkgen2  17462  ptclsg  17526  txcnp  17531  txcmplem1  17552  xkococnlem  17570  qtoptopon  17612  qtopid  17613  kqopn  17642  ptunhmeo  17716  trfbas2  17751  trfbas  17752  filin  17762  filintn0  17769  trfil2  17795  fgtr  17798  trufil  17818  cfinufil  17836  elfm3  17858  fmfnfmlem4  17865  neiflim  17882  flfval  17898  flfnei  17899  fclsbas  17929  ptcmplem5  17963  tgplacthmeo  17999  tgpconcompeqg  18007  tgpconcomp  18008  tsmssubm  18038  tsmssplit  18047  tsmsxplem1  18048  blpnfctr  18195  mopni2  18252  stdbdmopn  18277  met1stc  18280  nrmmetd  18310  tngngp2  18381  xrsxmet  18528  metdsle  18570  climcncf  18618  icoopnst  18652  iocopnst  18653  cnheibor  18668  bndth  18671  htpyco1  18691  htpyco2  18692  phtpyco2  18703  pi1xfr  18768  pi1coghm  18774  lmmbrf  18903  lmnn  18904  caucfil  18924  cmetcaulem  18929  iscmet3  18934  cfilresi  18936  caussi  18938  causs  18939  lmle  18942  lmclimf  18944  bcthlem4  18964  bcth3  18968  minveclem4  19011  ivth2  19030  ivthicc  19033  cniccbdd  19036  ovollb2  19063  ovolctb  19064  ovolunlem1a  19070  ovolunlem1  19071  ovolshftlem1  19083  ovolicc2lem1  19091  ovolicc2lem2  19092  ovolicc2lem4  19094  ovolicc2lem5  19095  uniioombllem2  19153  uniioombllem3  19155  volivth  19177  mbfss  19216  mbflimsup  19236  itg1val2  19254  i1fadd  19265  i1fmul  19266  itg1addlem4  19269  i1fmulc  19273  itg1mulc  19274  mbfi1fseqlem4  19288  itg2const2  19311  itg2seq  19312  itg2splitlem  19318  itg2split  19319  itg2addlem  19328  itg2gt0  19330  itg2cnlem2  19332  iblss  19374  iblss2  19375  itgss3  19384  itgless  19386  itgfsum  19396  itgsplit  19405  itgsplitioo  19407  itgcn  19412  ditgcl  19423  ditgswap  19424  ditgsplitlem  19425  dvconst  19481  dvaddbr  19502  dvmulbr  19503  dvcnvlem  19538  rolle  19552  dvlip  19555  dvlipcn  19556  dvlip2  19557  dveq0  19562  dv11cn  19563  dvivthlem1  19570  dvne0  19573  lhop1lem  19575  lhop2  19577  lhop  19578  dvcnvre  19581  dvfsumle  19583  dvfsumge  19584  dvfsumabs  19585  dvfsumlem2  19589  dvfsumlem3  19590  dvfsumrlimge0  19592  dvfsumrlim  19593  ftc1lem1  19597  ftc1lem4  19601  ftc1lem5  19602  itgsubstlem  19610  evl1sca  19628  mpfind  19643  deg1sclle  19713  plymullem  19813  coeeulem  19821  dgrlem  19826  dgrlb  19833  coemulhi  19850  dgrcolem2  19870  plydiveu  19893  vieta1lem2  19906  vieta1  19907  taylplem1  19957  taylplem2  19958  dvtaylp  19964  taylthlem1  19967  taylthlem2  19968  ulmdvlem1  19994  mtest  19998  mtestbdd  19999  radcnv0  20010  pserulm  20016  pserdvlem2  20022  abelthlem3  20027  abelthlem5  20029  abelthlem7  20032  efcvx  20043  sineq0  20107  tanord  20118  tanregt0  20119  logne0  20175  argregt0  20183  argimgt0  20185  argimlt0  20186  logneg2  20188  logcnlem3  20213  cxpsqr  20272  loglesqr  20320  ang180lem2  20330  isosctrlem1  20340  dcubic  20364  atanlogaddlem  20431  atanlogsub  20434  atantan  20441  atans2  20449  log2tlbnd  20463  birthdaylem2  20469  rlimcnp  20482  efrlim  20486  jensenlem1  20503  jensenlem2  20504  jensen  20505  fsumharmonic  20528  wilthlem2  20530  ftalem4  20536  ftalem5  20537  basellem3  20543  basellem4  20544  ppisval  20564  chtdif  20619  dvdsflsumcom  20651  musumsum  20655  muinv  20656  sgmmul  20663  chtleppi  20672  chtublem  20673  fsumvma  20675  chpval2  20680  chpub  20682  bposlem3  20748  lgsvalmod  20777  lgsdir2  20790  lgsdchr  20810  lgsquadlem2  20817  lgsquad2lem2  20821  chebbnd1lem1  20841  chebbnd1lem3  20843  dchrisumlem1  20861  dchrisumlem2  20862  dchrisumlem3  20863  dchrisum0fno1  20883  rpvmasum2  20884  dchrisum0lem1b  20887  dchrisum0lem1  20888  mulog2sumlem2  20907  chpdifbndlem1  20925  pntrsumbnd2  20939  pntrlog2bndlem6  20955  pntpbnd1  20958  pntlemj  20975  pntlemf  20977  qabvle  20997  padicabv  21002  padicabvcxp  21004  ostth2lem3  21007  usgraedg3  21082  usgrarnedg1  21085  grpoidinvlem2  21304  grpoidinvlem3  21305  grpoideu  21308  grpoinvid1  21329  grpoinvid2  21330  grpolcan  21332  grpo2inv  21338  grpoinvop  21340  grpomuldivass  21348  grpopnpcan2  21352  grponnncan2  21353  grponpncan  21354  gxinv  21369  gxid  21372  ablo4  21386  ablomuldiv  21388  ablodivdiv4  21390  ablonnncan  21392  ablonnncan1  21394  ghgrplem1  21465  ghgrp  21467  ghablo  21468  ghsubgolem  21469  rngolz  21500  rngorz  21501  vc0  21559  vcz  21560  nvzs  21637  nvmdi  21642  nvnegneg  21643  nvsubadd  21647  nvnpcan  21652  nvmeq0  21656  nvabs  21673  nvelbl2  21697  sspmval  21743  sspz  21745  sspival  21748  sspimsval  21750  nmoub3i  21785  nmblolbii  21811  dipsubdir  21860  sspph  21867  ubthlem1  21883  minvecolem3  21889  minvecolem4  21893  htthlem  21931  hvaddsub4  22091  hi2eq  22118  shsel3  22328  pjpreeq  22411  pjeq  22412  chabs1  22529  pjspansn  22590  chscllem1  22650  chscllem2  22651  chscllem4  22653  5oalem2  22668  3oalem2  22676  pjoi0  22730  nmopub2tALT  22923  nmfnleub2  22940  eigvalcl  22975  eighmre  22977  leopmul  23148  nmopleid  23153  opsqrlem4  23157  spansncv2  23307  chcv1  23369  atcv0eq  23393  atexch  23395  chirredi  23408  cdj1i  23447  elabreximd  23507  iocinif  23666  ressmulgnn  23717  dvrdir  23738  rhmunitinv  23746  kerunit  23747  zzsmulg  23751  remulg  23756  tpr2rico  23786  lmdvg  23814  cnextf  23823  restutopopn  23862  metutop  23931  logbrec  23991  indsum  24006  esummono  24036  esumpcvgval  24054  esumpmono  24055  esumcvg  24062  sigaclfu2  24090  cldssbrsiga  24127  ballotlemfp1  24318  ballotlemimin  24332  ballotlemsel1i  24339  ballotlemsima  24342  ballotlemfrceq  24355  ballotlemirc  24358  dmlogdmgm  24377  lgambdd  24390  subfacp1lem4  24438  subfacp1lem5  24439  erdszelem8  24453  ptpcon  24488  cvmliftmolem1  24536  cvmliftmolem2  24537  cvmliftlem6  24545  cvmliftlem7  24546  cvmliftlem10  24549  cvmlift2lem9  24566  cvmlift2lem11  24568  cvmlift2lem12  24569  ghomgsg  24672  ghomf1olem  24673  sinccvglem  24677  lediv2aALT  24685  rtrclreclem.trans  24715  clim2prod  24785  clim2div  24786  ntrivcvgfvn0  24796  ntrivcvgmullem  24798  fprodf1o  24841  prodss  24842  fprodss  24843  fprodser  24844  fprodsplit  24858  fprodeq0  24868  dfon2lem9  24973  sltval2  25136  colinearalg  25365  axcontlem2  25420  axcontlem7  25425  outsideofeq  25580  lineelsb2  25598  bpolysum  25615  bpolydiflem  25616  onsuct0  25707  voliunnfl  25758  volsupnfl  25759  itg2gt0cn  25763  bddiblnc  25778  ftc1cnnclem  25781  ftc1cnnc  25782  areacirc  25791  opnregcld  25840  isfne  25860  lfinpfin  25895  sdclem1  26045  fdc  26047  metf1o  26061  mettrifi  26065  equivtotbnd  26093  isbnd2  26098  bndss  26101  equivbnd2  26107  ismtyima  26118  ismtybndlem  26121  heiborlem1  26126  heiborlem8  26133  ismrer1  26153  ablo4pnp  26161  ghomdiv  26165  rngoneglmul  26173  rngonegrmul  26174  rngosubdi  26175  rngosubdir  26176  isdrngo2  26180  rngohomco  26196  rngoisoco  26204  iscringd  26215  crngm4  26219  idlsubcl  26239  divrngidl  26244  unichnidl  26247  keridl  26248  maxidln1  26260  maxidln0  26261  igenidl  26279  igenidl2  26281  ispridlc  26286  dmncan1  26292  elrfirn2  26362  2rexfrabdioph  26468  3rexfrabdioph  26469  4rexfrabdioph  26470  6rexfrabdioph  26471  7rexfrabdioph  26472  elnn0rabdioph  26475  irrapxlem5  26502  pell14qrre  26533  pell14qrne0  26534  pell14qrmulcl  26539  pellfundex  26562  monotoddzzfi  26618  jm2.17c  26640  fnwe2lem2  26739  frlmsslsp  26839  islinds2  26874  f1lindf  26883  flcidc  26970  psgnunilem5  27008  expgrowthi  27141  sumpair  27297  climinf  27323  stoweidlem26  27366  stoweidlem27  27367  stoweidlem61  27401  fargshiftfo  27772  onetansqsecsq  27921  bnj594  28696  lssats  29261  lfl0  29314  lfladdcl  29320  lflvscl  29326  lkr0f  29343  olm11  29476  latm12  29479  cvrle  29527  cvrnle  29529  cvrne  29530  cvrval3  29661  atcvrj0  29676  atltcvr  29683  atbtwnexOLDN  29695  atbtwnex  29696  3at  29738  2atneat  29763  llncvrlpln2  29805  lplncvrlvol2  29863  dalemdnee  29914  linepsubN  30000  isline2  30022  paddasslem17  30084  pmodN  30098  pmapjlln1  30103  pclidN  30144  polval2N  30154  polssatN  30156  polpmapN  30160  2polpmapN  30161  2polvalN  30162  2polssN  30163  3polN  30164  pclss2polN  30169  2pmaplubN  30174  polatN  30179  2polatN  30180  psubclsubN  30188  pmapidclN  30190  ispsubcl2N  30195  linepsubclN  30199  polsubclN  30200  lhpoc2N  30263  ltrnlaut  30371  ltrncnv  30394  cdlemc3  30441  cdleme3b  30477  cdleme42ke  30733  trlcoat  30971  tendoid  31021  tendoex  31223  dvalveclem  31274  diaintclN  31307  diasslssN  31308  dvhgrp  31356  dvhlveclem  31357  docaclN  31373  diaocN  31374  doca2N  31375  doca3N  31376  dvadiaN  31377  djaclN  31385  djajN  31386  dibval2  31393  dibvalrel  31412  dibintclN  31416  dicvalrelN  31434  xihopellsmN  31503  dihopellsm  31504  dihsslss  31525  dih1  31535  dih1dimatlem  31578  dihlspsnat  31582  dihintcl  31593  dihmeetcl  31594  dochval2  31601  dochcl  31602  dochlss  31603  dochssv  31604  dochvalr  31606  dochvalr2  31611  dochocss  31615  dochoc  31616  dochnoncon  31640  djhcl  31649  djhlj  31650  djhexmid  31660  dvh3dim3N  31698  lcfrlem21  31812  hlhilhillem  32212
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