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

Theorem syl13anc 1230
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
syl13anc.5  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
Assertion
Ref Expression
syl13anc  |-  ( ph  ->  et )

Proof of Theorem syl13anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
52, 3, 43jca 1176 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 661 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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  df-3an 975
This theorem is referenced by:  syl23anc  1235  syl33anc  1243  pm2.61da3neOLD  2788  disjxiun  4444  wereu2  4876  ordelord  4900  caovassd  6456  caovcand  6459  caovordid  6463  caovordd  6465  caovdid  6472  caovdird  6475  swoer  7336  swoord1  7337  swoord2  7338  frfi  7761  indexfi  7824  ssfii  7875  elfiun  7886  suplub2  7917  supgtoreq  7924  wemaplem2  7968  htalem  8310  cofsmo  8645  alephsing  8652  sornom  8653  axdc3lem4  8829  zorn2lem1  8872  ttukeylem6  8890  ttukeylem7  8891  prlem934  9407  supfirege  10521  suprfinzcl  10971  fzosubel3  11841  fsuppmapnn0fiublem  12060  seqsplit  12104  seqcaopr  12108  ccatass  12566  wrdcctswrd  12649  wrdeqcats1  12658  wrdeqs1cat  12659  splid  12688  spllen  12689  splfv1  12690  splfv2a  12691  splval2  12692  swrds2  12842  isercolllem2  13447  fsumiun  13594  pcgcd1  14255  cshwsidrepswmod0  14433  cshwshashlem2  14435  cshwsdisj  14437  firest  14684  iscatd2  14932  posasymb  15435  joinle  15497  meetle  15511  lattrd  15541  latleeqj1  15546  latjlej1  15548  latjlej12  15550  latnlej2  15554  latjidm  15557  latleeqm1  15562  latmlem1  15564  latmlem12  15566  latmidm  15569  latledi  15572  latjass  15578  latj12  15579  latj13  15581  latj31  15582  latjrot  15583  latj4  15584  mod1ile  15588  lubun  15606  clatleglb  15609  latdisdlem  15672  mnd32g  15737  mnd12g  15738  mnd4g  15739  prdsmndd  15767  imasmnd  15772  mrcmndind  15807  gsumspl  15835  grpidrcan  15904  grpidlcan  15905  grpinvinv  15906  grplmulf1o  15913  grpinvssd  15916  grpinvadd  15917  grpsubrcan  15920  grpsubadd  15927  grpaddsubass  15929  grppncan  15930  grpsubsub4  15932  grppnpcan2  15933  grpnpncan  15934  grpnpncan0  15935  grpnnncan2  15936  grplactcnv  15939  mulgnn0dir  15965  mulgdirlem  15966  mulgneg2  15969  mulgnnass  15970  mulgnn0ass  15971  mulgass  15972  imasgrp  15986  nsgconj  16029  isnsg3  16030  nmzsubg  16037  ssnmz  16038  eqger  16046  eqgcpbl  16050  conjghm  16092  conjnmz  16095  conjnmzb  16096  subgga  16133  gass  16134  gasubg  16135  galcan  16137  gacan  16138  gapm  16139  gaorber  16141  gastacl  16142  gastacos  16143  cntzsubm  16168  cntzsubg  16169  oppgmnd  16184  symggen  16291  odmodnn0  16360  mndodconglem  16361  odmod  16366  odcong  16369  odmulgid  16372  odbezout  16376  gexdvdsi  16399  gexdvds  16400  sylow1lem2  16415  sylow1lem4  16417  sylow2blem1  16436  sylow2blem2  16437  sylow2blem3  16438  sylow3lem1  16443  sylow3lem2  16444  lsmass  16484  lsmmod  16489  lsmdisj2  16496  subgdisj1  16505  efgredleme  16557  efgredlemc  16559  efgcpbllemb  16569  frgp0  16574  frgpuplem  16586  abl32  16615  abladdsub4  16620  abladdsub  16621  ablpncan2  16622  ablsubsub  16624  mulgdi  16631  mulgsubdi  16634  odadd1  16647  odadd2  16648  gex2abl  16650  oddvdssubg  16654  cygabl  16684  telgsumfzslem  16808  ablfacrp  16907  pgpfac1lem2  16916  pgpfac1lem3a  16917  pgpfac1lem3  16918  pgpfac1lem4  16919  srgmulgass  16970  srgpcomp  16971  srgpcompp  16972  srgpcomppsc  16973  srgbinomlem3  16981  srgbinomlem4  16982  srgbinomlem  16983  csrgbinom  16985  rngcom  17014  rnglz  17022  rngrz  17023  rngnegl  17026  rngnegr  17027  rngmneg1  17028  rngmneg2  17029  rngsubdi  17031  rngsubdir  17032  mulgass2  17033  prdsrngd  17045  imasrng  17052  opprrng  17064  mulgass3  17070  dvdsrtr  17085  dvdsrmul1  17086  unitgrp  17100  dvrass  17123  dvrcan1  17124  dvrcan3  17125  irredrmul  17140  drngmul0or  17200  subrginv  17228  cntzsubr  17244  lmod0vs  17328  lmodvs0  17329  lmodvsmmulgdi  17330  lmodvneg1  17336  lmodvsneg  17337  lmodcom  17339  lmodsubvs  17349  lmodsubdi  17350  lmodsubdir  17351  lssvsubcl  17373  lssvacl  17383  lssvscl  17384  islss3  17388  lss1d  17392  lssintcl  17393  prdslmodd  17398  lmodvsinv  17465  lmodvsinv2  17466  lmhmplusg  17473  lmhmvsca  17474  lsmcl  17512  pj1lmhm  17529  lvecvs0or  17537  lssvs0or  17539  lvecinv  17542  lspsnvs  17543  lspfixed  17557  lspexch  17558  lspsolvlem  17571  lspsolv  17572  lssacsex  17573  lspsnat  17574  lsppratlem1  17576  lsppratlem3  17578  lsppratlem4  17579  lbsextlem2  17588  lbsextlem4  17590  sralmod  17616  2idlcpbl  17664  unitrrg  17713  assa2ass  17742  issubassa  17744  sraassa  17745  asclghm  17758  asclmul1  17759  asclmul2  17760  asclrhm  17762  assamulgscmlem2  17769  psrbagcon  17793  psrbagconcl  17796  psrbagconf1o  17797  gsumbagdiaglem  17798  psrmulcllem  17811  psrlidm  17827  psrlidmOLD  17828  psrridm  17829  psrridmOLD  17830  psrass1  17831  psrdi  17832  psrdir  17833  psrass23l  17834  psrcom  17835  mplmon2mul  17937  evlslem1  17955  coe1subfv  18078  lply1binomsc  18120  mulgrhm  18299  mulgrhmOLD  18302  cygznlem3  18375  evpmodpmf1o  18399  ipdi  18442  ip2di  18443  ipsubdir  18444  ipsubdi  18445  ip2subdi  18446  ipassr  18448  ipassr2  18449  ip2eq  18455  ocvlss  18470  lsmcss  18490  frlmphl  18579  frlmup1  18599  mamuass  18671  mamudi  18672  mamudir  18673  mamuvs1  18674  mamuvs2  18675  dmatmul  18766  dmatsubcl  18767  scmataddcl  18785  smatvscl  18793  scmatghm  18802  mavmulass  18818  mdetrlin  18871  mdetrsca  18872  mdetralt  18877  mdetunilem7  18887  mdetuni0  18890  matinv  18946  pm2mpghm  19084  chpscmatgsummon  19113  chfacfscmulgsum  19128  chfacfpmmulgsum  19132  chfacfpmmulgsum2  19133  cpmadugsumlemB  19142  cpmadugsumlemC  19143  cpmadugsumlemF  19144  iinopn  19178  subbascn  19521  cnhaus  19621  nrmsep2  19623  nrmsep  19624  regsep2  19643  isreg2  19644  hauscmplem  19672  1stcfb  19712  2ndcctbss  19722  ptbasfi  19817  pthaus  19874  txtube  19876  txhaus  19883  xkohaus  19889  kqnrmlem1  19979  kqnrmlem2  19980  nrmr0reg  19985  nrmhmph  20030  fbssint  20074  infil  20099  fgabs  20115  filcon  20119  filuni  20121  trfil2  20123  trfg  20127  ufprim  20145  elfm3  20186  rnelfm  20189  fmfnfmlem2  20191  fmfnfmlem4  20193  hausflimi  20216  hauspwpwf1  20223  fclsneii  20253  supnfcls  20256  flimfnfcls  20264  fclscmpi  20265  alexsublem  20279  ghmcnp  20348  divstgpopn  20353  psmetsym  20549  psmettri  20550  psmetge0  20551  psmetres2  20553  xmetge0  20582  xmetsym  20585  xmettri  20589  xmetres2  20599  prdsxmetlem  20606  prdsmet  20608  imasdsf1olem  20611  imasf1oxmet  20613  bldisj  20636  xblss2ps  20639  xblss2  20640  xmeter  20671  prdsbl  20729  metustexhalfOLD  20801  metustexhalf  20802  metustOLD  20805  metust  20806  nrmmetd  20830  ngpsubcan  20868  nmmtri  20876  nmrtri  20878  ngptgp  20885  nlmvscnlem2  20929  nrginvrcnlem  20934  metdcnlem  21076  clmmulg  21328  cvsmuleqdivd  21346  cvsdiveqd  21347  cphabscl  21367  cphsqrtcl2  21368  cphsqrtcl3  21369  cphnmf  21377  cph2ass  21394  ipcau2  21412  tchcphlem2  21414  ipcnlem2  21419  cfilfcls  21448  iscau3  21452  iscmet3lem2  21466  iscmet3  21467  relcmpcmet  21490  minveclem2  21576  minveclem4  21582  pjthlem1  21587  pjthlem2  21588  uniioombllem4  21730  dyadmax  21742  itg1addlem4  21841  itg1climres  21856  ply1divex  22272  aalioulem2  22463  amgmlem  23047  dvdsppwf1o  23190  perfect1  23231  perfectlem1  23232  perfectlem2  23233  dchrptlem2  23268  colline  23743  ttgcontlem1  23864  axcontlem9  23951  eengtrkg  23964  eengtrkge  23965  4cycl4dv4e  24344  el2spthonot0  24547  usg2spthonot1  24566  clwlknclwlkdifnum  24637  eupa0  24650  eupares  24651  eupap1  24652  frg2woteu  24732  numclwwlk5  24789  numclwwlk6  24790  grpoidinvlem4  24885  grpoasscan2  24916  grpoinvop  24919  grpopncan  24929  grponpcan  24930  grpopnpcan2  24931  grpodiveq  24934  gxcom  24947  gxnn0add  24952  ghgrp  25046  rngo2  25066  rngolz  25079  rngorz  25080  zerdivemp1  25112  vcm  25140  nvmul0or  25223  nvpncan2  25227  nvnncan  25234  nvdif  25244  nvabs  25252  smcnlem  25283  lnomul  25351  minvecolem2  25467  superpos  26949  ssnnssfz  27265  omndmul2  27364  omndmul3  27365  ogrpaddltbi  27371  ogrpaddltrbid  27373  ogrpsublt  27374  ogrpinvlt  27376  isarchi3  27393  archirngz  27395  archiabllem1a  27397  archiabllem1  27399  archiabllem2a  27400  archiabllem2c  27401  slmdvs0  27430  gsumvsca1  27436  gsumvsca2  27437  dvrdir  27443  rdivmuldivd  27444  dvrcan5  27446  ornglmullt  27460  isarchiofld  27470  rhmdvd  27474  rhmunitinv  27475  metideq  27508  metider  27509  pstmxmet  27512  lmxrge0  27570  qqhghm  27605  qqhrhm  27606  oddpwdc  27933  ballotlemiex  28080  wrdsplex  28135  cvmopnlem  28363  cvmliftmolem2  28367  cvmliftlem6  28375  cvmliftlem8  28377  cvmliftlem9  28378  cvmlift2lem9  28396  cvmlift3lem2  28405  cvmlift3lem6  28409  cvmlift3lem7  28410  cvmlift3lem9  28412  zprod  28646  nodense  29026  cgrtriv  29229  cgrdegen  29231  cgrextend  29235  segconeq  29237  btwntriv2  29239  btwncomand  29242  btwntriv1  29243  btwnintr  29246  btwnexch3  29247  btwnouttr  29251  btwnexch  29252  trisegint  29255  ifscgr  29271  btwnxfr  29283  colineartriv1  29294  colineartriv2  29295  colinearxfr  29302  fscgr  29307  lineid  29310  idinside  29311  endofsegidand  29313  btwnconn1lem5  29318  btwnconn1lem7  29320  btwnconn1lem11  29324  btwnconn1lem12  29325  btwnconn1lem13  29326  brsegle2  29336  segleantisym  29342  broutsideof2  29349  btwnoutside  29352  outsideoftr  29356  outsideofeq  29357  outsideofeu  29358  outsidele  29359  lineunray  29374  lineelsb2  29375  linecom  29377  linethru  29380  heicant  29626  neibastop1  29780  mettrifi  29853  isbnd3  29883  heibor1lem  29908  bfplem2  29922  ghomdiv  29949  zerdivemp1x  29961  irrapxlem5  30366  aomclem2  30605  isnumbasgrplem2  30657  mpaaeu  30704  mendrng  30746  mendlmod  30747  caofcan  30828  stoweidlem18  31318  stoweidlem41  31341  stoweidlem45  31345  stoweidlem55  31355  fourierdlem25  31432  fourierdlem31  31438  fourierdlem37  31444  fourierdlem42  31449  ssnn0ssfz  32002  zlmodzxzsub  32013  invginvrid  32025  lmodvsmdi  32048  ply1sclrmsm  32056  lincsum  32103  lincscm  32104  lindslinindimp2lem4  32135  lindslinindsimp2lem5  32136  ldepsprlem  32146  lincresunit3lem1  32153  lincresunit3lem2  32154  isldepslvec2  32159  lfladdcl  33868  lflvscl  33874  eqlkr3  33898  lkrlsp  33899  lshpkrlem4  33910  oldmm1  34014  olj01  34022  latmassOLD  34026  latm32  34028  latmrot  34029  latm4  34030  olm01  34033  cmtcomlemN  34045  cmtbr3N  34051  cmtbr4N  34052  lecmtN  34053  omlfh1N  34055  atlen0  34107  atnle  34114  atlatmstc  34116  atlatle  34117  cvlexchb1  34127  cvlcvr1  34136  ishlat3N  34151  hlatjass  34166  hlatj12  34167  hlatj32  34168  hlsupr2  34183  hlhgt2  34185  hl0lt1N  34186  hlrelat  34198  hlrelat2  34199  exatleN  34200  hlrelat3  34208  cvrval5  34211  cvrexchlem  34215  cvratlem  34217  cvrat  34218  atcvr0eq  34222  lnnat  34223  atlt  34233  atlelt  34234  2atlt  34235  atexchltN  34237  cvrat3  34238  2atjm  34241  atbtwn  34242  4noncolr3  34249  athgt  34252  3dimlem3a  34256  3dimlem3OLDN  34258  3dimlem4a  34259  3dimlem4OLDN  34261  3dim1  34263  3dim2  34264  1cvratex  34269  ps-1  34273  ps-2  34274  hlatexch3N  34276  hlatexch4  34277  ps-2b  34278  3atlem1  34279  3atlem2  34280  3atlem5  34283  3atlem6  34284  llnnleat  34309  llncmp  34318  2at0mat0  34321  2atmat0  34322  2atm  34323  lplni2  34333  lvolex3N  34334  lplnnle2at  34337  lplnnleat  34338  lplnnlelln  34339  2atnelpln  34340  llncvrlpln  34354  2atmat  34357  lplncmp  34358  lplnexllnN  34360  2llnjaN  34362  2llnm4  34366  2llnmeqat  34367  lvolnle3at  34378  lvolnleat  34379  2atnelvolN  34383  islvol2aN  34388  4atlem3  34392  4atlem3a  34393  4atlem3b  34394  4atlem4a  34395  4atlem4b  34396  4atlem4c  34397  4atlem4d  34398  4atlem10  34402  4atlem11b  34404  4atlem11  34405  4atlem12b  34407  4atlem12  34408  4at2  34410  lplncvrlvol  34412  lvolcmp  34413  2lplnja  34415  dalemqrprot  34444  dalemply  34450  dalemsly  34451  dalemrot  34453  dalemrotyz  34454  dalem1  34455  dalemcea  34456  dalem3  34460  dalem5  34463  dalem8  34466  dalem-cly  34467  dalem11  34470  dalem12  34471  dalem16  34475  dalem17  34476  dalem18  34477  dalem21  34490  dalem24  34493  dalem25  34494  dalem38  34506  dalem39  34507  dalem44  34512  dalem54  34522  dalem55  34523  dalem57  34525  dalem58  34526  dalem59  34527  dalem60  34528  dath2  34533  2atm2atN  34581  2llnma1b  34582  2llnma3r  34584  cdlema1N  34587  cdlemblem  34589  paddasslem5  34620  paddasslem10  34625  paddasslem12  34627  paddasslem13  34628  paddass  34634  padd12N  34635  padd4N  34636  paddss  34641  pmodlem1  34642  pmodl42N  34647  pmapjoin  34648  pmapjlln1  34651  atmod1i2  34655  llnmod1i2  34656  llnexchb2  34665  dalawlem2  34668  dalawlem3  34669  dalawlem5  34671  dalawlem6  34672  dalawlem7  34673  dalawlem8  34674  dalawlem11  34677  dalawlem12  34678  dalawlem13  34679  pclunN  34694  osumcllem1N  34752  pexmidlem3N  34768  lhp2lt  34797  lhp0lt  34799  lhpexle2lem  34805  lhpexle3lem  34807  lhpocnle  34812  lhpj1  34818  lhpmcvr4N  34822  lhp2at0  34828  lhpat3  34842  4atexlemtlw  34863  4atexlemc  34865  4atexlemnclw  34866  4atexlemcnd  34868  lautcvr  34888  lautj  34889  lautm  34890  ltrnm  34927  ltrnj  34928  ltrncvr  34929  trlval3  34983  cdlemc5  34991  cdlemd2  34995  cdlemd3  34996  cdleme0e  35013  cdleme1  35023  cdleme3c  35026  cdleme3g  35030  cdleme3h  35031  cdleme3  35033  cdleme5  35036  cdleme7c  35041  cdleme7d  35042  cdleme7e  35043  cdleme7ga  35044  cdleme7  35045  cdleme9  35049  cdleme11c  35057  cdleme11g  35061  cdleme11k  35064  cdleme11  35066  cdleme12  35067  cdleme15b  35071  cdleme15d  35073  cdleme16d  35077  cdleme16e  35078  cdleme16f  35079  cdleme17b  35083  cdleme18b  35088  cdleme22gb  35090  cdlemednpq  35095  cdleme19a  35099  cdleme20aN  35105  cdleme20bN  35106  cdleme20c  35107  cdleme20d  35108  cdleme20j  35114  cdleme21c  35123  cdleme22aa  35135  cdleme22b  35137  cdleme22cN  35138  cdleme22d  35139  cdleme22e  35140  cdleme22eALTN  35141  cdleme23b  35146  cdleme23c  35147  cdleme28a  35166  cdleme30a  35174  cdlemefs29bpre0N  35212  cdlemefs29bpre1N  35213  cdlemefs29cpre1N  35214  cdlemefs29clN  35215  cdlemefs32fvaN  35218  cdlemefs32fva1  35219  cdleme32b  35238  cdleme32c  35239  cdleme32e  35241  cdleme35a  35244  cdleme35fnpq  35245  cdleme35b  35246  cdleme35f  35250  cdleme36a  35256  cdleme36m  35257  cdleme37m  35258  cdleme39a  35261  cdleme42c  35268  cdleme42i  35279  cdleme42keg  35282  cdleme42mgN  35284  cdleme48bw  35298  cdlemeg46fjgN  35317  cdlemeg46fjv  35319  cdlemeg46req  35325  cdleme50trn1  35345  cdlemf1  35357  cdlemf2  35358  cdlemg1cex  35384  cdlemg2fv2  35396  cdlemg7fvbwN  35403  cdlemg4c  35408  cdlemg4  35413  cdlemg6c  35416  cdlemg8b  35424  cdlemg10c  35435  cdlemg10  35437  cdlemg11b  35438  cdlemg12f  35444  cdlemg13a  35447  cdlemg17a  35457  cdlemg17dALTN  35460  cdlemg18b  35475  cdlemg19a  35479  cdlemg27a  35488  cdlemg27b  35492  cdlemg33b0  35497  cdlemg33a  35502  cdlemg35  35509  trlcolem  35522  cdlemg42  35525  cdlemg46  35531  trljco  35536  tendopltp  35576  cdlemh1  35611  cdlemh2  35612  cdlemi1  35614  cdlemi  35616  cdlemk3  35629  cdlemk10  35639  cdlemk11  35645  cdlemk15  35651  cdlemk1u  35655  cdlemk5u  35657  cdlemk11u  35667  cdlemk39  35712  cdlemkid1  35718  cdlemk50  35748  cdlemk51  35749  erngdvlem3-rN  35794  tendocnv  35818  tendospcanN  35820  dialss  35843  dia2dimlem1  35861  dia2dimlem2  35862  dia2dimlem3  35863  dia2dimlem10  35870  dia2dimlem12  35872  dvhvaddass  35894  dvhlveclem  35905  cdlemm10N  35915  doca2N  35923  djajN  35934  dib1dim2  35965  diblss  35967  diclspsn  35991  cdlemn2  35992  cdlemn10  36003  dihjustlem  36013  dihord1  36015  dihord2a  36016  dihord2pre2  36023  dib2dim  36040  dih2dimb  36041  dih2dimbALTN  36042  dihopelvalcpre  36045  dihord5b  36056  dihord6b  36057  dihord5apre  36059  dihmeetlem1N  36087  dihglblem5apreN  36088  dihglblem2N  36091  dihglbcpreN  36097  dihmeetbclemN  36101  dihmeetlem3N  36102  dihmeetlem6  36106  dih1dimatlem  36126  djhcvat42  36212  dihjatcclem1  36215  dihjatcclem4  36218  dvh4dimat  36235  lcfl7lem  36296  lclkrlem2m  36316  lcfrlem1  36339  lcdvsass  36404  baerlem3lem1  36504  baerlem5alem1  36505  baerlem5blem1  36506  mapdh6gN  36539  mapdh6hN  36540  hdmap1l6g  36614  hdmap1l6h  36615  hdmapneg  36646  hdmap14lem8  36675  hgmapadd  36694  hgmapmul  36695  hgmapvvlem1  36723
  Copyright terms: Public domain W3C validator