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  3028  csbied2  3124  elpw2g  4174  pofun  4330  elpwunsn  4568  fnbr  5346  dffv2  5592  fnexALT  5742  grprinvlem  6058  caofid0l  6105  caofid0r  6106  caofid1  6107  caofid2  6108  caofcom  6109  frxp  6225  fnse  6232  riotasv3d  6353  tfr3  6415  tz7.48-2  6454  oaf1o  6561  omlimcl  6576  oeeulem  6599  ixpexg  6840  f1domg  6881  domdifsn  6945  unxpdom2  7071  xpfir  7085  fofinf1o  7137  fofi  7142  imafi  7148  intrnfi  7170  ordtypelem6  7238  oiexg  7250  cantnfp1lem3  7382  cantnflem1  7391  infxpenlem  7641  fseqenlem2  7652  ssnum  7666  acni2  7673  finacn  7677  fonum  7685  infpwfien  7689  inffien  7690  infunsdom1  7839  infunsdom  7840  ackbij1lem12  7857  cfslb2n  7894  fin23lem28  7966  compssiso  8000  isf34lem5  8004  fin56  8019  axcc3  8064  axdc3lem2  8077  ttukeylem6  8141  ttukeylem7  8142  brdom3  8153  gchdomtri  8251  fpwwe2lem13  8264  gchxpidm  8291  tsken  8376  tsksn  8382  tsk1  8386  tsk2  8387  2domtsk  8388  tskcard  8403  r1tskina  8404  gruss  8418  gruxp  8429  gruina  8440  grur1a  8441  ltaddpr  8658  ltexprlem7  8666  1idsr  8720  addgt0sr  8726  recexsr  8729  msqgt0  9294  mulgt1  9615  gt0div  9622  ge0div  9623  ltdiv2  9641  ltrec1  9643  lerec2  9644  lediv2  9646  lediv12a  9649  recreclt  9655  creur  9740  nn2ge  9771  avgle1  9951  recnz  10087  suprzcl  10091  uzwo2  10283  rpnnen1lem5  10346  xrrege0  10503  xlemul1a  10608  xrsupsslem  10625  xrinfmsslem  10626  supxr2  10632  supxrpnf  10637  supxrunb1  10638  supxrunb2  10639  ixxun  10672  peano2fzor  10919  ioopnfsup  10968  modcl  10976  modge0  10980  zmodcl  10989  seqcl  11066  seqf  11067  seqfveq  11070  sermono  11078  seqsplit  11079  seqcaopr2  11082  seqf1olem2  11086  seqf1o  11087  seqhomo  11093  seqz  11094  le2sq2  11179  faclbnd4lem3  11308  bcpasc  11333  seqcoll  11401  seqcoll2  11402  ccatlid  11434  ccatass  11436  ccatswrd  11459  wrdeqcats1  11474  wrdeqs1cat  11475  revccat  11484  revrev  11485  sqrlem7  11734  resqrex  11736  sqrgt0  11744  leabs  11784  absmax  11813  r19.2uz  11835  lo1bdd2  11998  o1lo12  12012  rlimclim1  12019  lo1eq  12042  rlimeq  12043  rlimcn1  12062  rlimcn2  12064  rlimdiv  12119  rlimsqzlem  12122  clim2ser  12128  clim2ser2  12129  climub  12135  isercolllem1  12138  isercolllem3  12140  isercoll2  12142  climsup  12143  serf0  12153  iseraltlem1  12154  fsumf1o  12196  fsumss  12198  fsumsplit  12212  fsum2dlem  12233  fsumless  12254  fsumabs  12259  fsumtscopo  12260  fsumparts  12264  fsumrlim  12269  fsumo1  12270  o1fsum  12271  cvgcmp  12274  cvgcmpce  12276  fsumiun  12279  binom1dif  12291  incexclem  12295  incexc  12296  isumsplit  12299  isumrpcl  12302  isumless  12304  isumsup2  12305  isumltss  12307  climcnds  12310  supcvg  12314  expcnv  12322  explecnv  12323  geomulcvg  12332  cvgrat  12339  mertenslem1  12340  efcllem  12359  ef0lem  12360  eftlub  12389  tanval3  12414  tanneg  12428  rpnnen2lem7  12499  rpnnen2lem9  12501  rpnnen2lem11  12503  ruclem9  12516  dvdssubr  12570  divalgmod  12605  bitsf1  12637  algfx  12750  eucalgcvga  12756  isprm6  12788  phimullem  12847  eulerthlem2  12850  pcid  12925  pcgcd  12930  unbenlem  12955  prmreclem4  12966  prmreclem5  12967  4sqlem9  12993  4sqlem15  13006  4sqlem16  13007  vdwlem2  13029  vdwlem6  13033  vdwlem10  13037  vdwlem11  13038  vdwlem13  13040  ramval  13055  ressabs  13206  imasaddflem  13432  imasvscaf  13441  mrcid  13515  mrcidb  13517  mrcidm  13521  fucidcl  13839  setcmon  13919  setcepi  13920  catccatid  13934  xpccatid  13962  yonedalem4c  14051  yonedainv  14055  pospo  14107  latjlej1  14171  latmlem1  14187  latledi  14195  latj32  14203  latjjdi  14209  ipoval  14257  mrelatlub  14289  mreclat  14290  psss  14323  tsrlemax  14329  spwpr4c  14341  grpidd  14395  ismndd  14396  issubmnd  14401  subsubm  14434  gsumress  14454  gsumval2  14460  grpinvid1  14530  grpinvid2  14531  grplcan  14534  grpinvinv  14535  grpinvval2  14549  mulgass  14597  mulgpropd  14600  subginv  14628  subgmulg  14635  issubg2  14636  issubg4  14638  subsubg  14640  eqger  14667  divsinv  14676  resghm  14699  pwsdiagghm  14710  conjsubgen  14715  conjnsg  14718  subgga  14754  gass  14755  gasubg  14756  orbstafun  14765  orbsta  14767  gexcl2  14900  gexdvds3  14901  sylow1lem2  14910  sylow2blem1  14931  pj1ghm  15012  frgpup1  15084  frgpup3lem  15086  cntzspan  15137  cyggeninv  15170  lt6abl  15181  cycsubgcyg  15187  gsumval3eu  15190  gsumval3  15191  gsumzres  15194  gsumzaddlem  15203  gsumzsplit  15206  gsum2d  15223  gsum2d2lem  15224  dprdres  15263  dprdz  15265  dmdprdsplitlem  15272  dprdcntz2  15273  dprddisj2  15274  dprd2dlem1  15276  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dprdsplit  15283  ablfac1c  15306  ablfac1eulem  15307  ablfac1eu  15308  pgpfac1lem2  15310  ablfac2  15324  rngidss  15367  isrngd  15375  rnglz  15377  rngrz  15378  gsumdixp  15392  0unit  15462  unitnegcl  15463  rnginvdv  15476  invrpropd  15480  subrg1  15555  subrginv  15561  issubrg2  15565  subsubrg  15571  abvneg  15599  lmod0vs  15663  lmodvs0  15664  lmodvneg1  15667  islss3  15716  lspsnsubg  15737  lspidm  15743  lspsnneg  15763  lmhmlsp  15806  drngnidl  15981  psrass1lem  16123  psrlinv  16142  psrlidm  16148  mplsubglem  16179  mplcoe1  16209  mplcoe2  16211  mplind  16243  xrsdsreval  16416  xrsdsreclb  16418  mulgrhm  16460  znfld  16514  cygznlem3  16523  ocvlsp  16576  pjff  16612  pjf2  16614  pjfo  16615  ocvpj  16617  ishil2  16619  tgcl  16707  tgclb  16708  tgss2  16725  tgfiss  16729  opncld  16770  ntrval2  16788  ntrss3  16797  clsidm  16804  ntridm  16805  opnssneib  16852  ssnei2  16853  neindisj  16854  opnnei  16857  innei  16862  resttopon  16892  restcld  16903  restcls  16911  restntr  16912  perfopn  16915  cnpnei  16993  cncls2i  16999  cnntri  17000  cnclsi  17001  lmss  17026  pnrmopn  17071  lpcls  17092  perfcls  17093  cncmp  17119  cmpsublem  17126  cmpsub  17127  consuba  17146  clscon  17156  1stcrest  17179  lly1stc  17222  hauspwdom  17227  llycmpkgen2  17245  ptclsg  17309  txcnp  17314  txcmplem1  17335  xkococnlem  17353  qtoptopon  17395  qtopid  17396  kqopn  17425  ptunhmeo  17499  trfbas2  17538  trfbas  17539  filin  17549  filintn0  17556  trfil2  17582  fgtr  17585  trufil  17605  cfinufil  17623  elfm3  17645  fmfnfmlem4  17652  neiflim  17669  flfval  17685  flfnei  17686  fclsbas  17716  ptcmplem5  17750  tgplacthmeo  17786  tgpconcompeqg  17794  tgpconcomp  17795  tsmssubm  17825  tsmssplit  17834  tsmsxplem1  17835  blpnfctr  17982  mopni2  18039  stdbdmopn  18064  met1stc  18067  nrmmetd  18097  tngngp2  18168  xrsxmet  18315  metdsle  18356  climcncf  18404  icoopnst  18437  iocopnst  18438  cnheibor  18453  bndth  18456  htpyco1  18476  htpyco2  18477  phtpyco2  18488  pi1xfr  18553  pi1coghm  18559  lmmbrf  18688  lmnn  18689  caucfil  18709  cmetcaulem  18714  iscmet3  18719  cfilresi  18721  caussi  18723  causs  18724  lmle  18727  lmclimf  18729  bcthlem4  18749  bcth3  18753  minveclem4  18796  ivth2  18815  ivthicc  18818  cniccbdd  18821  ovollb2  18848  ovolctb  18849  ovolunlem1a  18855  ovolunlem1  18856  ovolshftlem1  18868  ovolicc2lem1  18876  ovolicc2lem2  18877  ovolicc2lem4  18879  ovolicc2lem5  18880  uniioombllem2  18938  uniioombllem3  18940  volivth  18962  mbfss  19001  mbflimsup  19021  itg1val2  19039  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  i1fmulc  19058  itg1mulc  19059  mbfi1fseqlem4  19073  itg2const2  19096  itg2seq  19097  itg2splitlem  19103  itg2split  19104  itg2addlem  19113  itg2gt0  19115  itg2cnlem2  19117  iblss  19159  iblss2  19160  itgss3  19169  itgless  19171  itgfsum  19181  itgsplit  19190  itgsplitioo  19192  itgcn  19197  ditgcl  19208  ditgswap  19209  ditgsplitlem  19210  dvconst  19266  dvaddbr  19287  dvmulbr  19288  dvcnvlem  19323  rolle  19337  dvlip  19340  dvlipcn  19341  dvlip2  19342  dveq0  19347  dv11cn  19348  dvivthlem1  19355  dvne0  19358  lhop1lem  19360  lhop2  19362  lhop  19363  dvcnvre  19366  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumrlimge0  19377  dvfsumrlim  19378  ftc1lem1  19382  ftc1lem4  19386  ftc1lem5  19387  itgsubstlem  19395  evl1sca  19413  mpfind  19428  deg1sclle  19498  plymullem  19598  coeeulem  19606  dgrlem  19611  dgrlb  19618  coemulhi  19635  dgrcolem2  19655  plydiveu  19678  vieta1lem2  19691  vieta1  19692  taylplem1  19742  taylplem2  19743  dvtaylp  19749  taylthlem1  19752  taylthlem2  19753  ulmdvlem1  19777  mtest  19781  radcnv0  19792  pserulm  19798  pserdvlem2  19804  abelthlem3  19809  abelthlem5  19811  abelthlem7  19814  efcvx  19825  sineq0  19889  tanord  19900  tanregt0  19901  logne0  19956  argregt0  19964  argimgt0  19966  argimlt0  19967  logneg2  19969  logcnlem3  19991  cxpsqr  20050  loglesqr  20098  ang180lem2  20108  isosctrlem1  20118  dcubic  20142  atanlogaddlem  20209  atanlogsub  20212  atantan  20219  atans2  20227  log2tlbnd  20241  birthdaylem2  20247  rlimcnp  20260  efrlim  20264  jensenlem1  20281  jensenlem2  20282  jensen  20283  fsumharmonic  20305  wilthlem2  20307  ftalem4  20313  ftalem5  20314  basellem3  20320  basellem4  20321  ppisval  20341  chtdif  20396  dvdsflsumcom  20428  musumsum  20432  muinv  20433  sgmmul  20440  chtleppi  20449  chtublem  20450  fsumvma  20452  chpval2  20457  chpub  20459  bposlem3  20525  lgsvalmod  20554  lgsdir2  20567  lgsdchr  20587  lgsquadlem2  20594  lgsquad2lem2  20598  chebbnd1lem1  20618  chebbnd1lem3  20620  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0lem1b  20664  dchrisum0lem1  20665  mulog2sumlem2  20684  chpdifbndlem1  20702  pntrsumbnd2  20716  pntrlog2bndlem6  20732  pntpbnd1  20735  pntlemj  20752  pntlemf  20754  qabvle  20774  padicabv  20779  padicabvcxp  20781  ostth2lem3  20784  grpoidinvlem2  20872  grpoidinvlem3  20873  grpoideu  20876  grpoinvid1  20897  grpoinvid2  20898  grpolcan  20900  grpo2inv  20906  grpoinvop  20908  grpomuldivass  20916  grpopnpcan2  20920  grponnncan2  20921  grponpncan  20922  gxinv  20937  gxid  20940  ablo4  20954  ablomuldiv  20956  ablodivdiv4  20958  ablonnncan  20960  ablonnncan1  20962  ghgrplem1  21033  ghgrp  21035  ghablo  21036  ghsubgolem  21037  rngolz  21068  rngorz  21069  vc0  21125  vcz  21126  nvzs  21203  nvmdi  21208  nvnegneg  21209  nvsubadd  21213  nvnpcan  21218  nvmeq0  21222  nvabs  21239  nvelbl2  21263  sspmval  21309  sspz  21311  sspival  21314  sspimsval  21316  nmoub3i  21351  nmblolbii  21377  dipsubdir  21426  sspph  21433  ubthlem1  21449  minvecolem3  21455  minvecolem4  21459  htthlem  21497  hvaddsub4  21657  hi2eq  21684  shsel3  21894  pjpreeq  21977  pjeq  21978  chabs1  22095  pjspansn  22156  chscllem1  22216  chscllem2  22217  chscllem4  22219  5oalem2  22234  3oalem2  22242  pjoi0  22296  nmopub2tALT  22489  nmfnleub2  22506  eigvalcl  22541  eighmre  22543  leopmul  22714  nmopleid  22719  opsqrlem4  22723  spansncv2  22873  chcv1  22935  atcv0eq  22959  atexch  22961  chirredi  22974  cdj1i  23013  elabreximd  23039  ballotlemfp1  23050  ballotlemimin  23064  ballotlemsel1i  23071  ballotlemsima  23074  ballotlemfrceq  23087  ballotlemirc  23090  subfacp1lem4  23125  subfacp1lem5  23126  erdszelem8  23140  ptpcon  23175  cvmliftmolem1  23223  cvmliftmolem2  23224  cvmliftlem6  23232  cvmliftlem7  23233  cvmliftlem10  23236  cvmlift2lem9  23253  cvmlift2lem11  23255  cvmlift2lem12  23256  ghomgsg  23411  ghomf1olem  23412  sinccvglem  23416  lediv2aALT  23424  rtrclreclem.trans  23454  dfon2lem9  23558  sltval2  23721  colinearalg  23949  axcontlem2  24004  axcontlem7  24009  outsideofeq  24164  lineelsb2  24182  bpolysum  24199  bpolydiflem  24200  onsuct0  24291  areacirc  24343  fprod1fi  24738  grpodrcan  24787  ltrinvlem  24818  invaddvec  24879  dblsubvec  24886  mvecrtol2  24889  basexre  24934  intopcoaconb  24952  qusp  24954  cntrset  25014  msr4  25018  lvsovso  25038  lvsovso3  25040  dmrngcmp  25163  dualcat2  25196  idfisf  25253  prismorcsetlem  25324  isgraphmrph  25335  idmor  25358  domidmor  25360  codidmor  25362  grphidmor  25364  grphidmor3  25366  cmp2morpcats  25373  cmpidmor2  25381  cmpidmor3  25382  lemindclsbu  25407  isconc2  25419  opnregcld  25660  isfne  25680  lfinpfin  25715  sdclem1  25865  fdc  25867  metf1o  25881  mettrifi  25885  equivtotbnd  25914  isbnd2  25919  bndss  25922  equivbnd2  25928  ismtyima  25939  ismtybndlem  25942  heiborlem1  25947  heiborlem8  25954  ismrer1  25974  ablo4pnp  25982  ghomdiv  25986  rngoneglmul  25994  rngonegrmul  25995  rngosubdi  25996  rngosubdir  25997  isdrngo2  26001  rngohomco  26017  rngoisoco  26025  iscringd  26036  crngm4  26040  idlsubcl  26060  divrngidl  26065  unichnidl  26068  keridl  26069  maxidln1  26081  maxidln0  26082  igenidl  26100  igenidl2  26102  ispridlc  26107  dmncan1  26113  elrfirn2  26183  2rexfrabdioph  26289  3rexfrabdioph  26290  4rexfrabdioph  26291  6rexfrabdioph  26292  7rexfrabdioph  26293  elnn0rabdioph  26296  irrapxlem5  26323  pell14qrre  26354  pell14qrne0  26355  pell14qrmulcl  26360  pellfundex  26383  monotoddzzfi  26439  jm2.17c  26461  fnwe2lem2  26560  frlmsslsp  26660  islinds2  26695  f1lindf  26704  flcidc  26791  psgnunilem5  26829  expgrowthi  26962  sumpair  27118  climinf  27144  stoweidlem26  27187  stoweidlem27  27188  stoweidlem61  27222  onetansqsecsq  27593  bnj594  28317  lssats  28575  lfl0  28628  lfladdcl  28634  lflvscl  28640  lkr0f  28657  olm11  28790  latm12  28793  cvrle  28841  cvrnle  28843  cvrne  28844  cvrval3  28975  atcvrj0  28990  atltcvr  28997  atbtwnexOLDN  29009  atbtwnex  29010  3at  29052  2atneat  29077  llncvrlpln2  29119  lplncvrlvol2  29177  dalemdnee  29228  linepsubN  29314  isline2  29336  paddasslem17  29398  pmodN  29412  pmapjlln1  29417  pclidN  29458  polval2N  29468  polssatN  29470  polpmapN  29474  2polpmapN  29475  2polvalN  29476  2polssN  29477  3polN  29478  pclss2polN  29483  2pmaplubN  29488  polatN  29493  2polatN  29494  psubclsubN  29502  pmapidclN  29504  ispsubcl2N  29509  linepsubclN  29513  polsubclN  29514  lhpoc2N  29577  ltrnlaut  29685  ltrncnv  29708  cdlemc3  29755  cdleme3b  29791  cdleme42ke  30047  trlcoat  30285  tendoid  30335  tendoex  30537  dvalveclem  30588  diaintclN  30621  diasslssN  30622  dvhgrp  30670  dvhlveclem  30671  docaclN  30687  diaocN  30688  doca2N  30689  doca3N  30690  dvadiaN  30691  djaclN  30699  djajN  30700  dibval2  30707  dibvalrel  30726  dibintclN  30730  dicvalrelN  30748  xihopellsmN  30817  dihopellsm  30818  dihsslss  30839  dih1  30849  dih1dimatlem  30892  dihlspsnat  30896  dihintcl  30907  dihmeetcl  30908  dochval2  30915  dochcl  30916  dochlss  30917  dochssv  30918  dochvalr  30920  dochvalr2  30925  dochocss  30929  dochoc  30930  dochnoncon  30954  djhcl  30963  djhlj  30964  djhexmid  30974  dvh3dim3N  31012  lcfrlem21  31126  hlhilhillem  31526
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