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  3041  csbied2  3137  elpw2g  4190  pofun  4346  elpwunsn  4584  fnbr  5362  dffv2  5608  fnexALT  5758  grprinvlem  6074  caofid0l  6121  caofid0r  6122  caofid1  6123  caofid2  6124  caofcom  6125  frxp  6241  fnse  6248  riotasv3d  6369  tfr3  6431  tz7.48-2  6470  oaf1o  6577  omlimcl  6592  oeeulem  6615  ixpexg  6856  f1domg  6897  domdifsn  6961  unxpdom2  7087  xpfir  7101  fofinf1o  7153  fofi  7158  imafi  7164  intrnfi  7186  ordtypelem6  7254  oiexg  7266  cantnfp1lem3  7398  cantnflem1  7407  infxpenlem  7657  fseqenlem2  7668  ssnum  7682  acni2  7689  finacn  7693  fonum  7701  infpwfien  7705  inffien  7706  infunsdom1  7855  infunsdom  7856  ackbij1lem12  7873  cfslb2n  7910  fin23lem28  7982  compssiso  8016  isf34lem5  8020  fin56  8035  axcc3  8080  axdc3lem2  8093  ttukeylem6  8157  ttukeylem7  8158  brdom3  8169  gchdomtri  8267  fpwwe2lem13  8280  gchxpidm  8307  tsken  8392  tsksn  8398  tsk1  8402  tsk2  8403  2domtsk  8404  tskcard  8419  r1tskina  8420  gruss  8434  gruxp  8445  gruina  8456  grur1a  8457  ltaddpr  8674  ltexprlem7  8682  1idsr  8736  addgt0sr  8742  recexsr  8745  msqgt0  9310  mulgt1  9631  gt0div  9638  ge0div  9639  ltdiv2  9657  ltrec1  9659  lerec2  9660  lediv2  9662  lediv12a  9665  recreclt  9671  creur  9756  nn2ge  9787  avgle1  9967  recnz  10103  suprzcl  10107  uzwo2  10299  rpnnen1lem5  10362  xrrege0  10519  xlemul1a  10624  xrsupsslem  10641  xrinfmsslem  10642  supxr2  10648  supxrpnf  10653  supxrunb1  10654  supxrunb2  10655  ixxun  10688  peano2fzor  10935  ioopnfsup  10984  modcl  10992  modge0  10996  zmodcl  11005  seqcl  11082  seqf  11083  seqfveq  11086  sermono  11094  seqsplit  11095  seqcaopr2  11098  seqf1olem2  11102  seqf1o  11103  seqhomo  11109  seqz  11110  le2sq2  11195  faclbnd4lem3  11324  bcpasc  11349  seqcoll  11417  seqcoll2  11418  ccatlid  11450  ccatass  11452  ccatswrd  11475  wrdeqcats1  11490  wrdeqs1cat  11491  revccat  11500  revrev  11501  sqrlem7  11750  resqrex  11752  sqrgt0  11760  leabs  11800  absmax  11829  r19.2uz  11851  lo1bdd2  12014  o1lo12  12028  rlimclim1  12035  lo1eq  12058  rlimeq  12059  rlimcn1  12078  rlimcn2  12080  rlimdiv  12135  rlimsqzlem  12138  clim2ser  12144  clim2ser2  12145  climub  12151  isercolllem1  12154  isercolllem3  12156  isercoll2  12158  climsup  12159  serf0  12169  iseraltlem1  12170  fsumf1o  12212  fsumss  12214  fsumsplit  12228  fsum2dlem  12249  fsumless  12270  fsumabs  12275  fsumtscopo  12276  fsumparts  12280  fsumrlim  12285  fsumo1  12286  o1fsum  12287  cvgcmp  12290  cvgcmpce  12292  fsumiun  12295  binom1dif  12307  incexclem  12311  incexc  12312  isumsplit  12315  isumrpcl  12318  isumless  12320  isumsup2  12321  isumltss  12323  climcnds  12326  supcvg  12330  expcnv  12338  explecnv  12339  geomulcvg  12348  cvgrat  12355  mertenslem1  12356  efcllem  12375  ef0lem  12376  eftlub  12405  tanval3  12430  tanneg  12444  rpnnen2lem7  12515  rpnnen2lem9  12517  rpnnen2lem11  12519  ruclem9  12532  dvdssubr  12586  divalgmod  12621  bitsf1  12653  algfx  12766  eucalgcvga  12772  isprm6  12804  phimullem  12863  eulerthlem2  12866  pcid  12941  pcgcd  12946  unbenlem  12971  prmreclem4  12982  prmreclem5  12983  4sqlem9  13009  4sqlem15  13022  4sqlem16  13023  vdwlem2  13045  vdwlem6  13049  vdwlem10  13053  vdwlem11  13054  vdwlem13  13056  ramval  13071  ressabs  13222  imasaddflem  13448  imasvscaf  13457  mrcid  13531  mrcidb  13533  mrcidm  13537  fucidcl  13855  setcmon  13935  setcepi  13936  catccatid  13950  xpccatid  13978  yonedalem4c  14067  yonedainv  14071  pospo  14123  latjlej1  14187  latmlem1  14203  latledi  14211  latj32  14219  latjjdi  14225  ipoval  14273  mrelatlub  14305  mreclat  14306  psss  14339  tsrlemax  14345  spwpr4c  14357  grpidd  14411  ismndd  14412  issubmnd  14417  subsubm  14450  gsumress  14470  gsumval2  14476  grpinvid1  14546  grpinvid2  14547  grplcan  14550  grpinvinv  14551  grpinvval2  14565  mulgass  14613  mulgpropd  14616  subginv  14644  subgmulg  14651  issubg2  14652  issubg4  14654  subsubg  14656  eqger  14683  divsinv  14692  resghm  14715  pwsdiagghm  14726  conjsubgen  14731  conjnsg  14734  subgga  14770  gass  14771  gasubg  14772  orbstafun  14781  orbsta  14783  gexcl2  14916  gexdvds3  14917  sylow1lem2  14926  sylow2blem1  14947  pj1ghm  15028  frgpup1  15100  frgpup3lem  15102  cntzspan  15153  cyggeninv  15186  lt6abl  15197  cycsubgcyg  15203  gsumval3eu  15206  gsumval3  15207  gsumzres  15210  gsumzaddlem  15219  gsumzsplit  15222  gsum2d  15239  gsum2d2lem  15240  dprdres  15279  dprdz  15281  dmdprdsplitlem  15288  dprdcntz2  15289  dprddisj2  15290  dprd2dlem1  15292  dmdprdsplit2lem  15296  dmdprdsplit2  15297  dprdsplit  15299  ablfac1c  15322  ablfac1eulem  15323  ablfac1eu  15324  pgpfac1lem2  15326  ablfac2  15340  rngidss  15383  isrngd  15391  rnglz  15393  rngrz  15394  gsumdixp  15408  0unit  15478  unitnegcl  15479  rnginvdv  15492  invrpropd  15496  subrg1  15571  subrginv  15577  issubrg2  15581  subsubrg  15587  abvneg  15615  lmod0vs  15679  lmodvs0  15680  lmodvneg1  15683  islss3  15732  lspsnsubg  15753  lspidm  15759  lspsnneg  15779  lmhmlsp  15822  drngnidl  15997  psrass1lem  16139  psrlinv  16158  psrlidm  16164  mplsubglem  16195  mplcoe1  16225  mplcoe2  16227  mplind  16259  xrsdsreval  16432  xrsdsreclb  16434  mulgrhm  16476  znfld  16530  cygznlem3  16539  ocvlsp  16592  pjff  16628  pjf2  16630  pjfo  16631  ocvpj  16633  ishil2  16635  tgcl  16723  tgclb  16724  tgss2  16741  tgfiss  16745  opncld  16786  ntrval2  16804  ntrss3  16813  clsidm  16820  ntridm  16821  opnssneib  16868  ssnei2  16869  neindisj  16870  opnnei  16873  innei  16878  resttopon  16908  restcld  16919  restcls  16927  restntr  16928  perfopn  16931  cnpnei  17009  cncls2i  17015  cnntri  17016  cnclsi  17017  lmss  17042  pnrmopn  17087  lpcls  17108  perfcls  17109  cncmp  17135  cmpsublem  17142  cmpsub  17143  consuba  17162  clscon  17172  1stcrest  17195  lly1stc  17238  hauspwdom  17243  llycmpkgen2  17261  ptclsg  17325  txcnp  17330  txcmplem1  17351  xkococnlem  17369  qtoptopon  17411  qtopid  17412  kqopn  17441  ptunhmeo  17515  trfbas2  17554  trfbas  17555  filin  17565  filintn0  17572  trfil2  17598  fgtr  17601  trufil  17621  cfinufil  17639  elfm3  17661  fmfnfmlem4  17668  neiflim  17685  flfval  17701  flfnei  17702  fclsbas  17732  ptcmplem5  17766  tgplacthmeo  17802  tgpconcompeqg  17810  tgpconcomp  17811  tsmssubm  17841  tsmssplit  17850  tsmsxplem1  17851  blpnfctr  17998  mopni2  18055  stdbdmopn  18080  met1stc  18083  nrmmetd  18113  tngngp2  18184  xrsxmet  18331  metdsle  18372  climcncf  18420  icoopnst  18453  iocopnst  18454  cnheibor  18469  bndth  18472  htpyco1  18492  htpyco2  18493  phtpyco2  18504  pi1xfr  18569  pi1coghm  18575  lmmbrf  18704  lmnn  18705  caucfil  18725  cmetcaulem  18730  iscmet3  18735  cfilresi  18737  caussi  18739  causs  18740  lmle  18743  lmclimf  18745  bcthlem4  18765  bcth3  18769  minveclem4  18812  ivth2  18831  ivthicc  18834  cniccbdd  18837  ovollb2  18864  ovolctb  18865  ovolunlem1a  18871  ovolunlem1  18872  ovolshftlem1  18884  ovolicc2lem1  18892  ovolicc2lem2  18893  ovolicc2lem4  18895  ovolicc2lem5  18896  uniioombllem2  18954  uniioombllem3  18956  volivth  18978  mbfss  19017  mbflimsup  19037  itg1val2  19055  i1fadd  19066  i1fmul  19067  itg1addlem4  19070  i1fmulc  19074  itg1mulc  19075  mbfi1fseqlem4  19089  itg2const2  19112  itg2seq  19113  itg2splitlem  19119  itg2split  19120  itg2addlem  19129  itg2gt0  19131  itg2cnlem2  19133  iblss  19175  iblss2  19176  itgss3  19185  itgless  19187  itgfsum  19197  itgsplit  19206  itgsplitioo  19208  itgcn  19213  ditgcl  19224  ditgswap  19225  ditgsplitlem  19226  dvconst  19282  dvaddbr  19303  dvmulbr  19304  dvcnvlem  19339  rolle  19353  dvlip  19356  dvlipcn  19357  dvlip2  19358  dveq0  19363  dv11cn  19364  dvivthlem1  19371  dvne0  19374  lhop1lem  19376  lhop2  19378  lhop  19379  dvcnvre  19382  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumrlimge0  19393  dvfsumrlim  19394  ftc1lem1  19398  ftc1lem4  19402  ftc1lem5  19403  itgsubstlem  19411  evl1sca  19429  mpfind  19444  deg1sclle  19514  plymullem  19614  coeeulem  19622  dgrlem  19627  dgrlb  19634  coemulhi  19651  dgrcolem2  19671  plydiveu  19694  vieta1lem2  19707  vieta1  19708  taylplem1  19758  taylplem2  19759  dvtaylp  19765  taylthlem1  19768  taylthlem2  19769  ulmdvlem1  19793  mtest  19797  radcnv0  19808  pserulm  19814  pserdvlem2  19820  abelthlem3  19825  abelthlem5  19827  abelthlem7  19830  efcvx  19841  sineq0  19905  tanord  19916  tanregt0  19917  logne0  19972  argregt0  19980  argimgt0  19982  argimlt0  19983  logneg2  19985  logcnlem3  20007  cxpsqr  20066  loglesqr  20114  ang180lem2  20124  isosctrlem1  20134  dcubic  20158  atanlogaddlem  20225  atanlogsub  20228  atantan  20235  atans2  20243  log2tlbnd  20257  birthdaylem2  20263  rlimcnp  20276  efrlim  20280  jensenlem1  20297  jensenlem2  20298  jensen  20299  fsumharmonic  20321  wilthlem2  20323  ftalem4  20329  ftalem5  20330  basellem3  20336  basellem4  20337  ppisval  20357  chtdif  20412  dvdsflsumcom  20444  musumsum  20448  muinv  20449  sgmmul  20456  chtleppi  20465  chtublem  20466  fsumvma  20468  chpval2  20473  chpub  20475  bposlem3  20541  lgsvalmod  20570  lgsdir2  20583  lgsdchr  20603  lgsquadlem2  20610  lgsquad2lem2  20614  chebbnd1lem1  20634  chebbnd1lem3  20636  dchrisumlem1  20654  dchrisumlem2  20655  dchrisumlem3  20656  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0lem1b  20680  dchrisum0lem1  20681  mulog2sumlem2  20700  chpdifbndlem1  20718  pntrsumbnd2  20732  pntrlog2bndlem6  20748  pntpbnd1  20751  pntlemj  20768  pntlemf  20770  qabvle  20790  padicabv  20795  padicabvcxp  20797  ostth2lem3  20800  grpoidinvlem2  20888  grpoidinvlem3  20889  grpoideu  20892  grpoinvid1  20913  grpoinvid2  20914  grpolcan  20916  grpo2inv  20922  grpoinvop  20924  grpomuldivass  20932  grpopnpcan2  20936  grponnncan2  20937  grponpncan  20938  gxinv  20953  gxid  20956  ablo4  20970  ablomuldiv  20972  ablodivdiv4  20974  ablonnncan  20976  ablonnncan1  20978  ghgrplem1  21049  ghgrp  21051  ghablo  21052  ghsubgolem  21053  rngolz  21084  rngorz  21085  vc0  21141  vcz  21142  nvzs  21219  nvmdi  21224  nvnegneg  21225  nvsubadd  21229  nvnpcan  21234  nvmeq0  21238  nvabs  21255  nvelbl2  21279  sspmval  21325  sspz  21327  sspival  21330  sspimsval  21332  nmoub3i  21367  nmblolbii  21393  dipsubdir  21442  sspph  21449  ubthlem1  21465  minvecolem3  21471  minvecolem4  21475  htthlem  21513  hvaddsub4  21673  hi2eq  21700  shsel3  21910  pjpreeq  21993  pjeq  21994  chabs1  22111  pjspansn  22172  chscllem1  22232  chscllem2  22233  chscllem4  22235  5oalem2  22250  3oalem2  22258  pjoi0  22312  nmopub2tALT  22505  nmfnleub2  22522  eigvalcl  22557  eighmre  22559  leopmul  22730  nmopleid  22735  opsqrlem4  22739  spansncv2  22889  chcv1  22951  atcv0eq  22975  atexch  22977  chirredi  22990  cdj1i  23029  elabreximd  23055  ballotlemfp1  23066  ballotlemimin  23080  ballotlemsel1i  23087  ballotlemsima  23090  ballotlemfrceq  23103  ballotlemirc  23106  iocinif  23289  tpr2rico  23311  ressmulgnn  23323  lmdvg  23391  hashgt0  23402  logbrec  23422  esumpcvgval  23461  esumpmono  23462  esumcvg  23469  sigaclfu2  23497  cldssbrsiga  23533  indsum  23621  subfacp1lem4  23729  subfacp1lem5  23730  erdszelem8  23744  ptpcon  23779  cvmliftmolem1  23827  cvmliftmolem2  23828  cvmliftlem6  23836  cvmliftlem7  23837  cvmliftlem10  23840  cvmlift2lem9  23857  cvmlift2lem11  23859  cvmlift2lem12  23860  ghomgsg  24015  ghomf1olem  24016  sinccvglem  24020  lediv2aALT  24028  rtrclreclem.trans  24058  fprodf1o  24172  dfon2lem9  24218  sltval2  24381  colinearalg  24610  axcontlem2  24665  axcontlem7  24670  outsideofeq  24825  lineelsb2  24843  bpolysum  24860  bpolydiflem  24861  onsuct0  24952  itg2gt0cn  25006  bddiblnc  25021  ftc1cnnclem  25024  ftc1cnnc  25025  areacirc  25034  fprod1fi  25429  grpodrcan  25478  ltrinvlem  25509  invaddvec  25570  dblsubvec  25577  mvecrtol2  25580  basexre  25625  intopcoaconb  25643  qusp  25645  cntrset  25705  msr4  25709  lvsovso  25729  lvsovso3  25731  dmrngcmp  25854  dualcat2  25887  idfisf  25944  prismorcsetlem  26015  isgraphmrph  26026  idmor  26049  domidmor  26051  codidmor  26053  grphidmor  26055  grphidmor3  26057  cmp2morpcats  26064  cmpidmor2  26072  cmpidmor3  26073  lemindclsbu  26098  isconc2  26110  opnregcld  26351  isfne  26371  lfinpfin  26406  sdclem1  26556  fdc  26558  metf1o  26572  mettrifi  26576  equivtotbnd  26605  isbnd2  26610  bndss  26613  equivbnd2  26619  ismtyima  26630  ismtybndlem  26633  heiborlem1  26638  heiborlem8  26645  ismrer1  26665  ablo4pnp  26673  ghomdiv  26677  rngoneglmul  26685  rngonegrmul  26686  rngosubdi  26687  rngosubdir  26688  isdrngo2  26692  rngohomco  26708  rngoisoco  26716  iscringd  26727  crngm4  26731  idlsubcl  26751  divrngidl  26756  unichnidl  26759  keridl  26760  maxidln1  26772  maxidln0  26773  igenidl  26791  igenidl2  26793  ispridlc  26798  dmncan1  26804  elrfirn2  26874  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  elnn0rabdioph  26987  irrapxlem5  27014  pell14qrre  27045  pell14qrne0  27046  pell14qrmulcl  27051  pellfundex  27074  monotoddzzfi  27130  jm2.17c  27152  fnwe2lem2  27251  frlmsslsp  27351  islinds2  27386  f1lindf  27395  flcidc  27482  psgnunilem5  27520  expgrowthi  27653  sumpair  27809  climinf  27835  stoweidlem26  27878  stoweidlem27  27879  stoweidlem61  27913  brovex  28205  fargshiftfo  28383  onetansqsecsq  28485  bnj594  29260  lssats  29824  lfl0  29877  lfladdcl  29883  lflvscl  29889  lkr0f  29906  olm11  30039  latm12  30042  cvrle  30090  cvrnle  30092  cvrne  30093  cvrval3  30224  atcvrj0  30239  atltcvr  30246  atbtwnexOLDN  30258  atbtwnex  30259  3at  30301  2atneat  30326  llncvrlpln2  30368  lplncvrlvol2  30426  dalemdnee  30477  linepsubN  30563  isline2  30585  paddasslem17  30647  pmodN  30661  pmapjlln1  30666  pclidN  30707  polval2N  30717  polssatN  30719  polpmapN  30723  2polpmapN  30724  2polvalN  30725  2polssN  30726  3polN  30727  pclss2polN  30732  2pmaplubN  30737  polatN  30742  2polatN  30743  psubclsubN  30751  pmapidclN  30753  ispsubcl2N  30758  linepsubclN  30762  polsubclN  30763  lhpoc2N  30826  ltrnlaut  30934  ltrncnv  30957  cdlemc3  31004  cdleme3b  31040  cdleme42ke  31296  trlcoat  31534  tendoid  31584  tendoex  31786  dvalveclem  31837  diaintclN  31870  diasslssN  31871  dvhgrp  31919  dvhlveclem  31920  docaclN  31936  diaocN  31937  doca2N  31938  doca3N  31939  dvadiaN  31940  djaclN  31948  djajN  31949  dibval2  31956  dibvalrel  31975  dibintclN  31979  dicvalrelN  31997  xihopellsmN  32066  dihopellsm  32067  dihsslss  32088  dih1  32098  dih1dimatlem  32141  dihlspsnat  32145  dihintcl  32156  dihmeetcl  32157  dochval2  32164  dochcl  32165  dochlss  32166  dochssv  32167  dochvalr  32169  dochvalr2  32174  dochocss  32178  dochoc  32179  dochnoncon  32203  djhcl  32212  djhlj  32213  djhexmid  32223  dvh3dim3N  32261  lcfrlem21  32375  hlhilhillem  32775
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