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

Theorem syldan 457
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 425 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 455 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 34 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sylan2  461  sbcied2  3190  csbied2  3286  elpw2g  4355  pofun  4511  elpwunsn  4748  fnbr  5538  dffv2  5787  fnexALT  5953  grprinvlem  6276  caofid0l  6323  caofid0r  6324  caofid1  6325  caofid2  6326  caofcom  6327  frxp  6447  fnse  6454  brovex  6465  riotasv3d  6589  tfr3  6651  tz7.48-2  6690  oaf1o  6797  omlimcl  6812  oeeulem  6835  ixpexg  7077  f1domg  7118  domdifsn  7182  unxpdom2  7308  xpfir  7322  fofinf1o  7378  fofi  7383  imafi  7390  intrnfi  7412  ordtypelem6  7481  oiexg  7493  cantnfp1lem3  7625  cantnflem1  7634  infxpenlem  7884  fseqenlem2  7895  ssnum  7909  acni2  7916  finacn  7920  fonum  7928  infpwfien  7932  inffien  7933  infunsdom1  8082  infunsdom  8083  ackbij1lem12  8100  cfslb2n  8137  fin23lem28  8209  compssiso  8243  isf34lem5  8247  fin56  8262  axcc3  8307  axdc3lem2  8320  ttukeylem6  8383  ttukeylem7  8384  brdom3  8395  gchdomtri  8493  fpwwe2lem13  8506  gchxpidm  8533  tsken  8618  tsksn  8624  tsk1  8628  tsk2  8629  2domtsk  8630  tskcard  8645  r1tskina  8646  gruss  8660  gruxp  8671  gruina  8682  grur1a  8683  ltaddpr  8900  ltexprlem7  8908  1idsr  8962  addgt0sr  8968  recexsr  8971  msqgt0  9537  mulgt1  9858  gt0div  9865  ge0div  9866  ltdiv2  9884  ltrec1  9886  lerec2  9887  lediv2  9889  lediv12a  9892  recreclt  9898  creur  9983  nn2ge  10014  avgle1  10196  recnz  10334  suprzcl  10338  uzwo2  10530  rpnnen1lem5  10593  xrrege0  10751  xlemul1a  10856  xrsupsslem  10874  xrinfmsslem  10875  supxr2  10881  supxrpnf  10886  supxrunb1  10887  supxrunb2  10888  ixxun  10921  peano2fzor  11182  ioopnfsup  11233  modcl  11241  modge0  11245  zmodcl  11254  seqcl  11331  seqf  11332  seqfveq  11335  sermono  11343  seqsplit  11344  seqcaopr2  11347  seqf1olem2  11351  seqf1o  11352  seqhomo  11358  seqz  11359  le2sq2  11445  faclbnd4lem3  11574  bcpasc  11600  hashgt0  11650  seqcoll  11700  seqcoll2  11701  ccatlid  11736  ccatass  11738  ccatswrd  11761  wrdeqcats1  11776  wrdeqs1cat  11777  revccat  11786  revrev  11787  sqrlem7  12042  resqrex  12044  sqrgt0  12052  leabs  12092  absmax  12121  r19.2uz  12143  lo1bdd2  12306  o1lo12  12320  rlimclim1  12327  lo1eq  12350  rlimeq  12351  rlimcn1  12370  rlimcn2  12372  rlimdiv  12427  rlimsqzlem  12430  clim2ser  12436  clim2ser2  12437  climub  12443  isercolllem1  12446  isercolllem3  12448  isercoll2  12450  climsup  12451  serf0  12462  iseraltlem1  12463  fsumf1o  12505  fsumss  12507  fsumsplit  12521  fsum2dlem  12542  fsumless  12563  fsumabs  12568  fsumtscopo  12569  fsumparts  12573  fsumrlim  12578  fsumo1  12579  o1fsum  12580  cvgcmp  12583  cvgcmpce  12585  fsumiun  12588  binom1dif  12600  incexclem  12604  incexc  12605  isumsplit  12608  isumrpcl  12611  isumless  12613  isumsup2  12614  isumltss  12616  climcnds  12619  supcvg  12623  expcnv  12631  explecnv  12632  geomulcvg  12641  cvgrat  12648  mertenslem1  12649  efcllem  12668  ef0lem  12669  eftlub  12698  tanval3  12723  tanneg  12737  rpnnen2lem7  12808  rpnnen2lem9  12810  rpnnen2lem11  12812  ruclem9  12825  dvdssubr  12879  divalgmod  12914  bitsf1  12946  algfx  13059  eucalgcvga  13065  isprm6  13097  phimullem  13156  eulerthlem2  13159  pcid  13234  pcgcd  13239  unbenlem  13264  prmreclem4  13275  prmreclem5  13276  4sqlem9  13302  4sqlem15  13315  4sqlem16  13316  vdwlem2  13338  vdwlem6  13342  vdwlem10  13346  vdwlem11  13347  vdwlem13  13349  ramval  13364  ressabs  13515  imasaddflem  13743  imasvscaf  13752  mrcid  13826  mrcidb  13828  mrcidm  13832  fucidcl  14150  setcmon  14230  setcepi  14231  catccatid  14245  xpccatid  14273  yonedalem4c  14362  yonedainv  14366  pospo  14418  latjlej1  14482  latmlem1  14498  latledi  14506  latj32  14514  latjjdi  14520  mrelatlub  14600  mreclat  14601  psss  14634  tsrlemax  14640  spwpr4c  14652  grpidd  14706  ismndd  14707  issubmnd  14712  subsubm  14745  gsumress  14765  gsumval2  14771  grpinvid1  14841  grpinvid2  14842  grplcan  14845  grpinvinv  14846  grpinvval2  14860  mulgass  14908  mulgpropd  14911  subginv  14939  subgmulg  14946  issubg2  14947  issubg4  14949  subsubg  14951  eqger  14978  divsinv  14987  resghm  15010  pwsdiagghm  15021  conjsubgen  15026  conjnsg  15029  subgga  15065  gass  15066  gasubg  15067  orbstafun  15076  orbsta  15078  gexcl2  15211  gexdvds3  15212  sylow1lem2  15221  sylow2blem1  15242  pj1ghm  15323  frgpup1  15395  frgpup3lem  15397  cntzspan  15448  cyggeninv  15481  lt6abl  15492  cycsubgcyg  15498  gsumval3eu  15501  gsumval3  15502  gsumzres  15505  gsumzaddlem  15514  gsumzsplit  15517  gsum2d  15534  gsum2d2lem  15535  dprdres  15574  dprdz  15576  dmdprdsplitlem  15583  dprdcntz2  15584  dprddisj2  15585  dprd2dlem1  15587  dmdprdsplit2lem  15591  dmdprdsplit2  15592  dprdsplit  15594  ablfac1c  15617  ablfac1eulem  15618  ablfac1eu  15619  pgpfac1lem2  15621  ablfac2  15635  rngidss  15678  isrngd  15686  rnglz  15688  rngrz  15689  gsumdixp  15703  0unit  15773  unitnegcl  15774  rnginvdv  15787  invrpropd  15791  subrg1  15866  subrginv  15872  issubrg2  15876  subsubrg  15882  abvneg  15910  lmod0vs  15971  lmodvs0  15972  lmodvneg1  15975  islss3  16023  lspsnsubg  16044  lspidm  16050  lspsnneg  16070  lmhmlsp  16113  drngnidl  16288  psrass1lem  16430  psrlinv  16449  psrlidm  16455  mplsubglem  16486  mplcoe1  16516  mplcoe2  16518  mplind  16550  xrsdsreval  16731  xrsdsreclb  16733  mulgrhm  16775  znfld  16829  cygznlem3  16838  ocvlsp  16891  pjff  16927  pjf2  16929  pjfo  16930  ocvpj  16932  ishil2  16934  tgcl  17022  tgclb  17023  tgss2  17040  tgfiss  17044  opncld  17085  ntrval2  17103  ntrss3  17112  clsidm  17119  ntridm  17120  opnssneib  17167  ssnei2  17168  neindisj  17169  opnnei  17172  innei  17177  resttopon  17213  restcld  17224  restcls  17233  restntr  17234  perfopn  17237  cnpnei  17316  cncls2i  17322  cnntri  17323  cnclsi  17324  lmss  17350  pnrmopn  17395  lpcls  17416  perfcls  17417  cncmp  17443  cmpsublem  17450  cmpsub  17451  consuba  17471  clscon  17481  1stcrest  17504  lly1stc  17547  hauspwdom  17552  llycmpkgen2  17570  ptclsg  17635  txcnp  17640  txcmplem1  17661  xkococnlem  17679  qtoptopon  17724  qtopid  17725  kqopn  17754  ptunhmeo  17828  trfbas2  17863  trfbas  17864  filin  17874  filintn0  17881  trfil2  17907  fgtr  17910  trufil  17930  cfinufil  17948  elfm3  17970  fmfnfmlem4  17977  neiflim  17994  flfval  18010  flfnei  18011  fclsbas  18041  ptcmplem5  18075  cnextf  18085  cnextfres  18087  tgplacthmeo  18121  tgpconcompeqg  18129  tgpconcomp  18130  tsmssubm  18160  tsmssplit  18169  tsmsxplem1  18170  restutopopn  18256  isucn2  18297  cnextucn  18321  blpnfctr  18454  mopni2  18511  stdbdmopn  18536  met1stc  18539  metutopOLD  18600  psmetutop  18601  nrmmetd  18610  tngngp2  18681  xrsxmet  18828  metdsle  18870  climcncf  18918  icoopnst  18952  iocopnst  18953  cnheibor  18968  bndth  18971  htpyco1  18991  htpyco2  18992  phtpyco2  19003  pi1xfr  19068  pi1coghm  19074  lmmbrf  19203  lmnn  19204  caucfil  19224  cmetcaulem  19229  iscmet3  19234  cfilresi  19236  caussi  19238  causs  19239  lmle  19242  lmclimf  19244  bcthlem4  19268  bcth3  19272  minveclem4  19321  ivth2  19340  ivthicc  19343  cniccbdd  19346  ovollb2  19373  ovolctb  19374  ovolunlem1a  19380  ovolunlem1  19381  ovolshftlem1  19393  ovolicc2lem1  19401  ovolicc2lem2  19402  ovolicc2lem4  19404  ovolicc2lem5  19405  uniioombllem2  19463  uniioombllem3  19465  volivth  19487  mbfss  19526  mbflimsup  19546  itg1val2  19564  i1fadd  19575  i1fmul  19576  itg1addlem4  19579  i1fmulc  19583  itg1mulc  19584  mbfi1fseqlem4  19598  itg2const2  19621  itg2seq  19622  itg2splitlem  19628  itg2split  19629  itg2addlem  19638  itg2gt0  19640  itg2cnlem2  19642  iblss  19684  iblss2  19685  itgss3  19694  itgless  19696  itgfsum  19706  itgsplit  19715  itgsplitioo  19717  itgcn  19722  ditgcl  19733  ditgswap  19734  ditgsplitlem  19735  dvconst  19791  dvaddbr  19812  dvmulbr  19813  rolle  19862  dvlip  19865  dvlipcn  19866  dvlip2  19867  dveq0  19872  dv11cn  19873  dvivthlem1  19880  dvne0  19883  lhop1lem  19885  lhop2  19887  lhop  19888  dvcnvre  19891  dvfsumle  19893  dvfsumge  19894  dvfsumabs  19895  dvfsumlem2  19899  dvfsumlem3  19900  dvfsumrlimge0  19902  dvfsumrlim  19903  ftc1lem1  19907  ftc1lem4  19911  ftc1lem5  19912  itgsubstlem  19920  evl1sca  19938  mpfind  19953  deg1sclle  20023  uc1pmon1p  20062  plymullem  20123  coeeulem  20131  dgrlem  20136  dgrlb  20143  coemulhi  20160  dgrcolem2  20180  plydiveu  20203  vieta1lem2  20216  vieta1  20217  taylplem1  20267  taylplem2  20268  dvtaylp  20274  taylthlem1  20277  taylthlem2  20278  ulmdvlem1  20304  mtest  20308  radcnv0  20320  pserulm  20326  pserdvlem2  20332  abelthlem3  20337  abelthlem5  20339  abelthlem7  20342  efcvx  20353  sineq0  20417  tanord  20428  tanregt0  20429  logne0  20485  argregt0  20493  argimgt0  20495  argimlt0  20496  logneg2  20498  logcnlem3  20523  cxpsqr  20582  loglesqr  20630  ang180lem2  20640  isosctrlem1  20650  dcubic  20674  atanlogaddlem  20741  atanlogsub  20744  atantan  20751  atans2  20759  log2tlbnd  20773  birthdaylem2  20779  rlimcnp  20792  efrlim  20796  jensenlem1  20813  jensenlem2  20814  jensen  20815  fsumharmonic  20838  wilthlem2  20840  ftalem4  20846  ftalem5  20847  basellem3  20853  basellem4  20854  ppisval  20874  chtdif  20929  dvdsflsumcom  20961  musumsum  20965  muinv  20966  sgmmul  20973  chtleppi  20982  chtublem  20983  fsumvma  20985  chpval2  20990  chpub  20992  bposlem3  21058  lgsvalmod  21087  lgsdir2  21100  lgsdchr  21120  lgsquadlem2  21127  lgsquad2lem2  21131  chebbnd1lem1  21151  chebbnd1lem3  21153  dchrisumlem1  21171  dchrisumlem2  21172  dchrisumlem3  21173  dchrisum0fno1  21193  rpvmasum2  21194  dchrisum0lem1b  21197  dchrisum0lem1  21198  mulog2sumlem2  21217  chpdifbndlem1  21235  pntrsumbnd2  21249  pntrlog2bndlem6  21265  pntpbnd1  21268  pntlemj  21285  pntlemf  21287  qabvle  21307  padicabv  21312  padicabvcxp  21314  ostth2lem3  21317  usgraedg3  21393  usgrarnedg1  21396  fargshiftfo  21613  grpoidinvlem2  21781  grpoidinvlem3  21782  grpoideu  21785  grpoinvid1  21806  grpoinvid2  21807  grpolcan  21809  grpo2inv  21815  grpoinvop  21817  grpomuldivass  21825  grpopnpcan2  21829  grponnncan2  21830  grponpncan  21831  gxinv  21846  gxid  21849  ablo4  21863  ablomuldiv  21865  ablodivdiv4  21867  ablonnncan  21869  ablonnncan1  21871  ghgrplem1  21942  ghgrp  21944  ghablo  21945  ghsubgolem  21946  rngolz  21977  rngorz  21978  vc0  22036  vcz  22037  nvzs  22114  nvmdi  22119  nvnegneg  22120  nvsubadd  22124  nvnpcan  22129  nvmeq0  22133  nvabs  22150  nvelbl2  22174  sspmval  22220  sspz  22222  sspival  22225  sspimsval  22227  nmoub3i  22262  nmblolbii  22288  dipsubdir  22337  sspph  22344  ubthlem1  22360  minvecolem3  22366  minvecolem4  22370  htthlem  22408  hvaddsub4  22568  hi2eq  22595  shsel3  22805  pjpreeq  22888  pjeq  22889  chabs1  23006  pjspansn  23067  chscllem1  23127  chscllem2  23128  chscllem4  23130  5oalem2  23145  3oalem2  23153  pjoi0  23207  nmopub2tALT  23400  nmfnleub2  23417  eigvalcl  23452  eighmre  23454  leopmul  23625  nmopleid  23630  opsqrlem4  23634  spansncv2  23784  chcv1  23846  atcv0eq  23870  atexch  23872  chirredi  23885  cdj1i  23924  elabreximd  23979  abfmpeld  24054  iocinif  24132  ressmulgnn  24193  dvrdir  24214  rhmunitinv  24248  kerunit  24249  zzsmulg  24253  remulg  24258  metider  24277  tpr2rico  24298  lmdvg  24326  rezh  24343  qqhvq  24359  logbrec  24393  indsum  24408  indpreima  24410  indf1ofs  24411  esummono  24438  esumpcvgval  24456  esumpmono  24457  esumcvg  24464  sigaclfu2  24492  cldssbrsiga  24529  probun  24665  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemsel1i  24758  ballotlemsima  24761  ballotlemfrceq  24774  ballotlemirc  24777  dmlogdmgm  24796  subfacp1lem4  24857  subfacp1lem5  24858  erdszelem8  24872  ptpcon  24908  cvmliftmolem1  24956  cvmliftmolem2  24957  cvmliftlem6  24965  cvmliftlem7  24966  cvmliftlem10  24969  cvmlift2lem9  24986  cvmlift2lem11  24988  cvmlift2lem12  24989  ghomgsg  25092  ghomf1olem  25093  sinccvglem  25097  lediv2aALT  25105  rtrclreclem.trans  25134  clim2prod  25205  clim2div  25206  ntrivcvgfvn0  25216  ntrivcvgmullem  25218  fprodf1o  25261  prodss  25262  fprodss  25263  fprodser  25264  fprodsplit  25278  fprodeq0  25288  fprod2dlem  25293  binomfallfaclem2  25345  dfon2lem9  25402  sltval2  25565  colinearalg  25797  axcontlem2  25852  axcontlem7  25857  outsideofeq  26012  lineelsb2  26030  bpolysum  26047  bpolydiflem  26048  onsuct0  26139  mblfinlem  26190  voliunnfl  26196  volsupnfl  26197  itg2gt0cn  26206  itgaddnclem2  26210  bddiblnc  26221  ftc1cnnclem  26224  ftc1cnnc  26225  areacirc  26234  opnregcld  26270  isfne  26285  lfinpfin  26320  sdclem1  26384  fdc  26386  metf1o  26398  mettrifi  26400  equivtotbnd  26424  isbnd2  26429  bndss  26432  equivbnd2  26438  ismtyima  26449  ismtybndlem  26452  heiborlem1  26457  heiborlem8  26464  ismrer1  26484  ablo4pnp  26492  ghomdiv  26496  rngoneglmul  26504  rngonegrmul  26505  rngosubdi  26506  rngosubdir  26507  isdrngo2  26511  rngohomco  26527  rngoisoco  26535  iscringd  26546  crngm4  26550  idlsubcl  26570  divrngidl  26575  unichnidl  26578  keridl  26579  maxidln1  26591  maxidln0  26592  igenidl  26610  igenidl2  26612  ispridlc  26617  dmncan1  26623  elrfirn2  26687  2rexfrabdioph  26793  3rexfrabdioph  26794  4rexfrabdioph  26795  6rexfrabdioph  26796  7rexfrabdioph  26797  elnn0rabdioph  26800  irrapxlem5  26826  pell14qrre  26857  pell14qrne0  26858  pell14qrmulcl  26863  pellfundex  26886  monotoddzzfi  26942  jm2.17c  26964  fnwe2lem2  27063  frlmsslsp  27163  islinds2  27198  f1lindf  27207  flcidc  27294  psgnunilem5  27332  expgrowthi  27465  rfcnpre1  27604  rfcnpre2  27616  fmulcl  27625  fmul01lt1lem1  27628  fmul01lt1lem2  27629  climinf  27646  stoweidlem11  27674  stoweidlem14  27677  stoweidlem20  27683  stoweidlem26  27689  stoweidlem27  27690  stoweidlem31  27694  stoweidlem48  27711  stoweidlem51  27714  onetansqsecsq  28362  bnj594  29137  lssats  29649  lfl0  29702  lfladdcl  29708  lflvscl  29714  lkr0f  29731  olm11  29864  latm12  29867  cvrle  29915  cvrnle  29917  cvrne  29918  cvrval3  30049  atcvrj0  30064  atltcvr  30071  atbtwnexOLDN  30083  atbtwnex  30084  3at  30126  2atneat  30151  llncvrlpln2  30193  lplncvrlvol2  30251  dalemdnee  30302  linepsubN  30388  isline2  30410  paddasslem17  30472  pmodN  30486  pmapjlln1  30491  pclidN  30532  polval2N  30542  polssatN  30544  polpmapN  30548  2polpmapN  30549  2polvalN  30550  2polssN  30551  3polN  30552  pclss2polN  30557  2pmaplubN  30562  polatN  30567  2polatN  30568  psubclsubN  30576  pmapidclN  30578  ispsubcl2N  30583  linepsubclN  30587  polsubclN  30588  lhpoc2N  30651  ltrnlaut  30759  ltrncnv  30782  cdlemc3  30829  cdleme3b  30865  cdleme42ke  31121  trlcoat  31359  tendoid  31409  tendoex  31611  dvalveclem  31662  diaintclN  31695  diasslssN  31696  dvhgrp  31744  dvhlveclem  31745  docaclN  31761  diaocN  31762  doca2N  31763  doca3N  31764  dvadiaN  31765  djaclN  31773  djajN  31774  dibval2  31781  dibvalrel  31800  dibintclN  31804  dicvalrelN  31822  xihopellsmN  31891  dihopellsm  31892  dihsslss  31913  dih1  31923  dih1dimatlem  31966  dihlspsnat  31970  dihintcl  31981  dihmeetcl  31982  dochval2  31989  dochcl  31990  dochlss  31991  dochssv  31992  dochvalr  31994  dochvalr2  31999  dochocss  32003  dochoc  32004  dochnoncon  32028  djhcl  32037  djhlj  32038  djhexmid  32048  dvh3dim3N  32086  lcfrlem21  32200  hlhilhillem  32600
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 178  df-an 361
  Copyright terms: Public domain W3C validator