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

Theorem syldan 467
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 465 . 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  471  thema2a  1584  sbcied2  3212  csbied2  3303  elpwunsn  3905  elpw2g  4443  pofun  4644  fnbr  5501  dffv2  5752  grprinvlem  6290  caofid0l  6337  caofid0r  6338  caofid1  6339  caofid2  6340  caofcom  6341  fnexALT  6532  frxp  6671  fnse  6678  brovex  6729  tfr3  6844  tz7.48-2  6883  oaf1o  6990  omlimcl  7005  oeeulem  7028  ixpexg  7275  f1domg  7317  domdifsn  7382  unxpdom2  7509  xpfir  7523  fofinf1o  7580  fofi  7585  imafi  7592  intrnfi  7654  ordtypelem6  7725  oiexg  7737  cantnfp1lem3  7876  cantnflem1  7885  cantnfp1lem3OLD  7902  cantnflem1OLD  7908  infxpenlem  8168  fseqenlem2  8183  ssnum  8197  acni2  8204  finacn  8208  fonum  8216  infpwfien  8220  inffien  8221  infunsdom1  8370  infunsdom  8371  ackbij1lem12  8388  cfslb2n  8425  fin23lem28  8497  compssiso  8531  isf34lem5  8535  fin56  8550  axcc3  8595  axdc3lem2  8608  ttukeylem6  8671  ttukeylem7  8672  brdom3  8683  gchdomtri  8784  fpwwe2lem13  8797  gchxpidm  8824  tsken  8909  tsksn  8915  tsk1  8919  tsk2  8920  2domtsk  8921  tskcard  8936  r1tskina  8937  gruss  8951  gruxp  8962  gruina  8973  grur1a  8974  ltaddpr  9191  ltexprlem7  9199  1idsr  9253  addgt0sr  9259  recexsr  9262  msqgt0  9848  mulgt1  10176  gt0div  10183  ge0div  10184  ltdiv2  10205  ltrec1  10207  lerec2  10208  lediv2  10210  lediv12a  10213  recreclt  10219  creur  10304  nn2ge  10335  avgle1  10552  recnz  10705  suprzcl  10709  uzwo2  10907  rpnnen1lem5  10971  xrrege0  11134  xlemul1a  11239  xrsupsslem  11257  xrinfmsslem  11258  supxr2  11264  supxrpnf  11269  supxrunb1  11270  supxrunb2  11271  ixxun  11304  peano2fzor  11616  ioopnfsup  11687  modcl  11696  modge0  11701  zmodcl  11711  seqcl  11810  seqf  11811  seqfveq  11814  sermono  11822  seqsplit  11823  seqcaopr2  11826  seqf1olem2  11830  seqf1o  11831  seqhomo  11837  seqz  11838  le2sq2  11925  faclbnd4lem3  12055  bcpasc  12081  hashgt0  12135  hashge2el2dif  12168  seqcoll  12200  seqcoll2  12201  wrdsymb1  12246  ccatlid  12268  ccatass  12270  swrdtrcfvl  12328  swrdlsw  12330  2swrd1eqwrdeq  12332  ccatswrd  12334  swrd0swrd  12339  swrdccatwrd  12346  wrdeqcats1  12352  wrdeqs1cat  12353  swrdccatin2  12362  revccat  12390  revrev  12391  sqrlem7  12722  resqrex  12724  sqrgt0  12732  leabs  12772  absmax  12801  r19.2uz  12823  lo1bdd2  12986  o1lo12  13000  rlimclim1  13007  lo1eq  13030  rlimeq  13031  rlimcn1  13050  rlimcn2  13052  rlimdiv  13107  rlimsqzlem  13110  clim2ser  13116  clim2ser2  13117  climub  13123  isercolllem1  13126  isercolllem3  13128  isercoll2  13130  climsup  13131  serf0  13142  iseraltlem1  13143  fsumf1o  13184  fsumss  13186  fsumsplit  13200  fsum2dlem  13221  fsumless  13242  fsumabs  13247  fsumtscopo  13248  fsumparts  13252  fsumrlim  13257  fsumo1  13258  o1fsum  13259  cvgcmp  13262  cvgcmpce  13264  fsumiun  13267  binom1dif  13279  incexclem  13282  incexc  13283  isumsplit  13286  isumrpcl  13289  isumless  13291  isumsup2  13292  isumltss  13294  climcnds  13297  supcvg  13301  expcnv  13309  explecnv  13310  geomulcvg  13319  cvgrat  13326  mertenslem1  13327  efcllem  13346  ef0lem  13347  eftlub  13376  tanval3  13401  tanneg  13415  rpnnen2lem7  13486  rpnnen2lem9  13488  rpnnen2lem11  13490  ruclem9  13503  dvdssubr  13557  divalgmod  13593  bitsf1  13625  algfx  13738  eucalgcvga  13744  isprm6  13778  phimullem  13837  eulerthlem2  13840  pcid  13922  pcgcd  13927  unbenlem  13952  prmreclem4  13963  prmreclem5  13964  4sqlem9  13990  4sqlem15  14003  4sqlem16  14004  vdwlem2  14026  vdwlem6  14030  vdwlem10  14034  vdwlem11  14035  vdwlem13  14037  ramval  14052  ressabs  14219  imasaddflem  14451  imasvscaf  14460  mrcid  14534  mrcidb  14536  mrcidm  14540  fucidcl  14858  setcmon  14938  setcepi  14939  catccatid  14953  xpccatid  14981  yonedalem4c  15070  yonedainv  15074  pospo  15126  latjlej1  15218  latmlem1  15234  latledi  15242  latj32  15250  latjjdi  15256  mrelatlub  15339  mreclatBAD  15340  psss  15367  tsrlemax  15373  grpidd  15426  ismndd  15427  issubmnd  15432  subsubm  15467  gsumress  15487  gsumval2  15493  grpinvid1  15566  grpinvid2  15567  grplcan  15570  grpinvinv  15573  grpinvval2  15589  mulgass  15637  mulgpropd  15640  subginv  15668  subgmulg  15675  issubg2  15676  issubg4  15680  subsubg  15684  eqger  15711  divsinv  15720  resghm  15743  pwsdiagghm  15754  conjsubgen  15759  conjnsg  15762  subgga  15798  gass  15799  gasubg  15800  orbstafun  15809  orbsta  15811  symgextfv  15903  psgnunilem5  15980  gexcl2  16068  gexdvds3  16069  sylow1lem2  16078  sylow2blem1  16099  pj1ghm  16180  frgpup1  16252  frgpup3lem  16254  cntzspan  16306  cyggeninv  16340  lt6abl  16351  cycsubgcyg  16357  gsumval3eu  16361  gsumval3OLD  16362  gsumval3  16365  gsumzres  16368  gsumzresOLD  16372  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumzsplit  16398  gsumzsplitOLD  16399  gsum2d  16437  gsum2dOLD  16438  gsum2d2lem  16439  dprdres  16499  dprdz  16501  dmdprdsplitlem  16508  dmdprdsplitlemOLD  16509  dprdcntz2  16510  dprddisj2  16511  dprddisj2OLD  16512  dprd2dlem1  16514  dmdprdsplit2lem  16518  dmdprdsplit2  16519  dprdsplit  16521  ablfac1c  16546  ablfac1eulem  16547  ablfac1eu  16548  pgpfac1lem2  16550  ablfac2  16564  rngidss  16607  isrngd  16615  rnglz  16617  rngrz  16618  gsumdixpOLD  16635  gsumdixp  16636  0unit  16706  unitnegcl  16707  rnginvdv  16720  invrpropd  16724  subrg1  16799  subrginv  16805  issubrg2  16809  subsubrg  16815  abvneg  16843  lmod0vs  16905  lmodvs0  16906  lmodvneg1  16912  islss3  16962  lspsnsubg  16983  lspidm  16989  lspsnneg  17009  lmhmlsp  17052  drngnidl  17233  psrass1lem  17381  psrlinv  17402  psrlidm  17408  psrlidmOLD  17409  mplsubglem  17444  mplsubglemOLD  17446  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  mplind  17516  xrsdsreval  17702  xrsdsreclb  17704  zringmulg  17733  zrngmulg  17739  mulgrhm  17768  mulgrhmOLD  17771  znfld  17835  cygznlem3  17844  remulg  17879  ocvlsp  17943  pjff  17979  pjf2  17981  pjfo  17982  ocvpj  17984  ishil2  17986  frlmsslsp  18065  frlmsslspOLD  18066  islinds2  18084  f1lindf  18093  mdet0pr  18245  m2detleib  18279  tgcl  18416  tgclb  18417  tgss2  18434  tgfiss  18438  opncld  18479  ntrval2  18497  ntrss3  18506  clsidm  18513  ntridm  18514  opnssneib  18561  ssnei2  18562  neindisj  18563  opnnei  18566  innei  18571  resttopon  18607  restcld  18618  restcls  18627  restntr  18628  perfopn  18631  cnpnei  18710  cncls2i  18716  cnntri  18717  cnclsi  18718  lmss  18744  pnrmopn  18789  lpcls  18810  perfcls  18811  cncmp  18837  cmpsublem  18844  cmpsub  18845  consuba  18866  clscon  18876  1stcrest  18899  lly1stc  18942  hauspwdom  18947  llycmpkgen2  18965  ptclsg  19030  txcnp  19035  txcmplem1  19056  xkococnlem  19074  qtoptopon  19119  qtopid  19120  kqopn  19149  ptunhmeo  19223  trfbas2  19258  trfbas  19259  filin  19269  filintn0  19276  trfil2  19302  fgtr  19305  trufil  19325  cfinufil  19343  elfm3  19365  fmfnfmlem4  19372  neiflim  19389  flfval  19405  flfnei  19406  fclsbas  19436  ptcmplem5  19470  cnextf  19480  cnextfres  19482  tgplacthmeo  19516  tgpconcompeqg  19524  tgpconcomp  19525  tsmssubm  19558  tsmssplit  19568  tsmsxplem1  19569  restutopopn  19655  isucn2  19696  cnextucn  19720  blpnfctr  19853  mopni2  19910  stdbdmopn  19935  met1stc  19938  metutopOLD  19999  psmetutop  20000  nrmmetd  20009  tngngp2  20080  xrsxmet  20228  metdsle  20270  climcncf  20318  icoopnst  20353  iocopnst  20354  cnheibor  20369  bndth  20372  htpyco1  20392  htpyco2  20393  phtpyco2  20404  pi1xfr  20469  pi1coghm  20475  lmmbrf  20615  lmnn  20616  caucfil  20636  cmetcaulem  20641  iscmet3  20646  cfilresi  20648  caussi  20650  causs  20651  lmle  20654  lmclimf  20656  bcthlem4  20680  bcth3  20684  rrxnm  20737  rrxcph  20738  rrxmval  20746  rrxmetlem  20748  rrxmet  20749  rrxdstprj1  20750  minveclem4  20761  ivth2  20781  ivthicc  20784  cniccbdd  20787  ovollb2  20814  ovolctb  20815  ovolunlem1a  20821  ovolunlem1  20822  ovolshftlem1  20834  ovolicc2lem1  20842  ovolicc2lem2  20843  ovolicc2lem4  20845  ovolicc2lem5  20846  uniioombllem2  20905  uniioombllem3  20907  volivth  20929  mbfss  20966  mbflimsup  20986  itg1val2  21004  i1fadd  21015  i1fmul  21016  itg1addlem4  21019  i1fmulc  21023  itg1mulc  21024  mbfi1fseqlem4  21038  itg2const2  21061  itg2seq  21062  itg2splitlem  21068  itg2split  21069  itg2addlem  21078  itg2gt0  21080  itg2cnlem2  21082  iblss  21124  iblss2  21125  itgss3  21134  itgless  21136  itgfsum  21146  itgsplit  21155  itgsplitioo  21157  itgcn  21162  ditgcl  21175  ditgswap  21176  ditgsplitlem  21177  dvconst  21233  dvaddbr  21254  dvmulbr  21255  rolle  21304  dvlip  21307  dvlipcn  21308  dvlip2  21309  dveq0  21314  dv11cn  21315  dvivthlem1  21322  dvne0  21325  lhop1lem  21327  lhop2  21329  lhop  21330  dvcnvre  21333  dvfsumle  21335  dvfsumge  21336  dvfsumabs  21337  dvfsumlem2  21341  dvfsumlem3  21342  dvfsumrlimge0  21344  dvfsumrlim  21345  ftc1lem1  21349  ftc1lem4  21353  ftc1lem5  21354  itgsubstlem  21362  evl1sca  21381  mpfind  21396  deg1sclle  21469  uc1pmon1p  21508  plymullem  21569  coeeulem  21577  dgrlem  21582  dgrlb  21589  coemulhi  21606  dgrcolem2  21626  plydiveu  21649  vieta1lem2  21662  vieta1  21663  taylplem1  21713  taylplem2  21714  dvtaylp  21720  taylthlem1  21723  taylthlem2  21724  ulmdvlem1  21750  mtest  21754  radcnv0  21766  pserulm  21772  pserdvlem2  21778  abelthlem3  21783  abelthlem5  21785  abelthlem7  21788  efcvx  21799  sineq0  21868  tanord  21879  tanregt0  21880  logne0  21936  argregt0  21944  argimgt0  21946  argimlt0  21947  logneg2  21949  logcnlem3  21974  cxpsqr  22033  loglesqr  22081  ang180lem2  22091  isosctrlem1  22101  dcubic  22126  atanlogaddlem  22193  atanlogsub  22196  atantan  22203  atans2  22211  log2tlbnd  22225  birthdaylem2  22231  rlimcnp  22244  efrlim  22248  jensenlem1  22265  jensenlem2  22266  jensen  22267  fsumharmonic  22290  wilthlem2  22292  ftalem4  22298  ftalem5  22299  basellem3  22305  basellem4  22306  ppisval  22326  chtdif  22381  dvdsflsumcom  22413  musumsum  22417  muinv  22418  sgmmul  22425  chtleppi  22434  chtublem  22435  fsumvma  22437  chpval2  22442  chpub  22444  bposlem3  22510  lgsvalmod  22539  lgsdir2  22552  lgsdchr  22572  lgsquadlem2  22579  lgsquad2lem2  22583  chebbnd1lem1  22603  chebbnd1lem3  22605  dchrisumlem1  22623  dchrisumlem2  22624  dchrisumlem3  22625  dchrisum0fno1  22645  rpvmasum2  22646  dchrisum0lem1b  22649  dchrisum0lem1  22650  mulog2sumlem2  22669  chpdifbndlem1  22687  pntrsumbnd2  22701  pntrlog2bndlem6  22717  pntpbnd1  22720  pntlemj  22737  pntlemf  22739  qabvle  22759  padicabv  22764  padicabvcxp  22766  ostth2lem3  22769  ttgval  22944  colinearalg  22979  axcontlem2  23034  axcontlem7  23039  usgraedg3  23127  usgrarnedg1  23130  fargshiftfo  23347  grpoidinvlem2  23515  grpoidinvlem3  23516  grpoideu  23519  grpoinvid1  23540  grpoinvid2  23541  grpolcan  23543  grpo2inv  23549  grpoinvop  23551  grpomuldivass  23559  grpopnpcan2  23563  grponnncan2  23564  grponpncan  23565  gxinv  23580  gxid  23583  ablo4  23597  ablomuldiv  23599  ablodivdiv4  23601  ablonnncan  23603  ablonnncan1  23605  ghgrplem1  23676  ghgrp  23678  ghablo  23679  ghsubgolem  23680  rngolz  23711  rngorz  23712  vc0  23770  vcz  23771  nvzs  23848  nvmdi  23853  nvnegneg  23854  nvsubadd  23858  nvnpcan  23863  nvmeq0  23867  nvabs  23884  nvelbl2  23908  sspmval  23954  sspz  23956  sspival  23959  sspimsval  23961  nmoub3i  23996  nmblolbii  24022  dipsubdir  24071  sspph  24078  ubthlem1  24094  minvecolem3  24100  minvecolem4  24104  htthlem  24142  hvaddsub4  24303  hi2eq  24330  shsel3  24541  pjpreeq  24624  pjeq  24625  chabs1  24742  pjspansn  24803  chscllem1  24863  chscllem2  24864  chscllem4  24866  5oalem2  24881  3oalem2  24889  pjoi0  24943  nmopub2tALT  25136  nmfnleub2  25153  eigvalcl  25188  eighmre  25190  leopmul  25361  nmopleid  25366  opsqrlem4  25370  spansncv2  25520  chcv1  25582  atcv0eq  25606  atexch  25608  chirredi  25621  cdj1i  25660  elabreximd  25715  iocinif  25894  ressmulgnn  25967  archirngz  26030  slmdvs0  26090  dvrdir  26111  rhmunitinv  26143  kerunit  26144  metider  26175  tpr2rico  26196  fsumcvg4  26234  lmdvg  26237  rezh  26254  qqhvq  26270  logbrec  26318  indsum  26333  indpreima  26335  indf1ofs  26336  esummono  26363  esumpcvgval  26381  esumpmono  26382  esumcvg  26389  sigaclfu2  26418  cldssbrsiga  26455  eulerpartlems  26591  eulerpartlemb  26599  eulerpartlemgvv  26607  eulerpartlemgs2  26611  probun  26650  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemsel1i  26743  ballotlemsima  26746  ballotlemfrceq  26759  ballotlemirc  26762  sgnneg  26771  sgnmulrp2  26774  signsply0  26800  signslema  26811  signstf0  26817  signsvfn  26831  signsvfpn  26834  signsvfnn  26835  signshf  26837  dmlogdmgm  26858  subfacp1lem4  26919  subfacp1lem5  26920  erdszelem8  26934  ptpcon  26970  cvmliftmolem1  27018  cvmliftmolem2  27019  cvmliftlem6  27027  cvmliftlem7  27028  cvmliftlem10  27031  cvmlift2lem9  27048  cvmlift2lem11  27050  cvmlift2lem12  27051  ghomgsg  27159  ghomf1olem  27160  sinccvglem  27164  lediv2aALT  27169  rtrclreclem.trans  27195  clim2prod  27250  clim2div  27251  ntrivcvgfvn0  27261  ntrivcvgmullem  27263  fprodf1o  27306  prodss  27307  fprodss  27308  fprodser  27309  fprodsplit  27323  fprodeq0  27333  fprod2dlem  27338  binomfallfaclem2  27390  dfon2lem9  27451  sltval2  27644  outsideofeq  28008  lineelsb2  28026  bpolysum  28043  bpolydiflem  28044  onsuct0  28135  fin2so  28260  mblfinlem2  28273  voliunnfl  28279  volsupnfl  28280  dvtanlem  28285  itg2gt0cn  28291  itgaddnclem2  28295  bddiblnc  28306  ftc1cnnclem  28309  ftc1cnnc  28310  ftc1anclem2  28312  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  ftc2nc  28320  areacirc  28333  opnregcld  28369  isfne  28384  lfinpfin  28419  sdclem1  28483  fdc  28485  metf1o  28495  mettrifi  28497  equivtotbnd  28521  isbnd2  28526  bndss  28529  equivbnd2  28535  ismtyima  28546  ismtybndlem  28549  heiborlem1  28554  heiborlem8  28561  ismrer1  28581  ablo4pnp  28589  ghomdiv  28593  rngoneglmul  28601  rngonegrmul  28602  rngosubdi  28603  rngosubdir  28604  isdrngo2  28608  rngohomco  28624  rngoisoco  28632  iscringd  28643  crngm4  28647  idlsubcl  28667  divrngidl  28672  unichnidl  28675  keridl  28676  maxidln1  28688  maxidln0  28689  igenidl  28707  igenidl2  28709  ispridlc  28714  dmncan1  28720  elrfirn2  28877  2rexfrabdioph  28979  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  elnn0rabdioph  28986  irrapxlem5  29012  pell14qrre  29043  pell14qrne0  29044  pell14qrmulcl  29049  pellfundex  29072  monotoddzzfi  29128  jm2.17c  29150  fnwe2lem2  29249  flcidc  29376  itgpowd  29435  expgrowthi  29452  rfcnpre1  29586  rfcnpre2  29598  fmulcl  29607  fmul01lt1lem1  29610  fmul01lt1lem2  29611  climinf  29625  stoweidlem11  29652  stoweidlem14  29655  stoweidlem20  29661  stoweidlem26  29667  stoweidlem27  29668  stoweidlem31  29672  stoweidlem48  29689  stoweidlem51  29692  fsummsnunz  30087  wwlkm1edg  30213  clwlkisclwwlklem2a  30293  clwlkisclwwlk  30297  wrdnval  30320  wlkp1lenfislenp  30358  frgrareg  30556  pgrpgt2nabel  30600  invginvrid  30603  01eq0rng  30608  lincsumscmcl  30676  onetansqsecsq  30805  bnj594  31607  riotasv3d  32184  lssats  32230  lfl0  32283  lfladdcl  32289  lflvscl  32295  lkr0f  32312  olm11  32445  latm12  32448  cvrle  32496  cvrnle  32498  cvrne  32499  cvrval3  32630  atcvrj0  32645  atltcvr  32652  atbtwnexOLDN  32664  atbtwnex  32665  3at  32707  2atneat  32732  llncvrlpln2  32774  lplncvrlvol2  32832  dalemdnee  32883  linepsubN  32969  isline2  32991  paddasslem17  33053  pmodN  33067  pmapjlln1  33072  pclidN  33113  polval2N  33123  polssatN  33125  polpmapN  33129  2polpmapN  33130  2polvalN  33131  2polssN  33132  3polN  33133  pclss2polN  33138  2pmaplubN  33143  polatN  33148  2polatN  33149  psubclsubN  33157  pmapidclN  33159  ispsubcl2N  33164  linepsubclN  33168  polsubclN  33169  lhpoc2N  33232  ltrnlaut  33340  ltrncnv  33363  cdlemc3  33410  cdleme3b  33446  cdleme42ke  33702  trlcoat  33940  tendoid  33990  tendoex  34192  dvalveclem  34243  diaintclN  34276  diasslssN  34277  dvhgrp  34325  dvhlveclem  34326  docaclN  34342  diaocN  34343  doca2N  34344  doca3N  34345  dvadiaN  34346  djaclN  34354  djajN  34355  dibval2  34362  dibvalrel  34381  dibintclN  34385  dicvalrelN  34403  xihopellsmN  34472  dihopellsm  34473  dihsslss  34494  dih1  34504  dih1dimatlem  34547  dihlspsnat  34551  dihintcl  34562  dihmeetcl  34563  dochval2  34570  dochcl  34571  dochlss  34572  dochssv  34573  dochvalr  34575  dochvalr2  34580  dochocss  34584  dochoc  34585  dochnoncon  34609  djhcl  34618  djhlj  34619  djhexmid  34629  dvh3dim3N  34667  lcfrlem21  34781  hlhilhillem  35181
  Copyright terms: Public domain W3C validator