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

Theorem syl13anc 1221
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 1168 . 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 965
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 967
This theorem is referenced by:  syl23anc  1226  syl33anc  1234  pm2.61da3neOLD  2769  disjxiun  4387  wereu2  4815  ordelord  4839  caovassd  6362  caovcand  6365  caovordid  6369  caovordd  6371  caovdid  6378  caovdird  6381  swoer  7229  swoord1  7230  swoord2  7231  frfi  7658  indexfi  7720  ssfii  7770  elfiun  7781  suplub2  7812  wemaplem2  7862  htalem  8204  cofsmo  8539  alephsing  8546  sornom  8547  axdc3lem4  8723  zorn2lem1  8766  ttukeylem6  8784  ttukeylem7  8785  prlem934  9303  fzosubel3  11702  seqsplit  11940  seqcaopr  11944  ccatass  12388  wrdcctswrd  12461  wrdeqcats1  12470  wrdeqs1cat  12471  splid  12497  spllen  12498  splfv1  12499  splfv2a  12500  splval2  12501  swrds2  12647  isercolllem2  13245  fsumiun  13386  pcgcd1  14045  cshwsidrepswmod0  14223  cshwshashlem2  14225  cshwsdisj  14227  firest  14473  iscatd2  14721  posasymb  15224  joinle  15286  meetle  15300  lattrd  15330  latleeqj1  15335  latjlej1  15337  latjlej12  15339  latnlej2  15343  latjidm  15346  latleeqm1  15351  latmlem1  15353  latmlem12  15355  latmidm  15358  latledi  15361  latjass  15367  latj12  15368  latj13  15370  latj31  15371  latjrot  15372  latj4  15373  mod1ile  15377  lubun  15395  clatleglb  15398  latdisdlem  15461  mnd32g  15526  mnd12g  15527  mnd4g  15528  prdsmndd  15556  imasmnd  15561  mrcmndind  15596  gsumspl  15624  grpidrcan  15693  grpidlcan  15694  grpinvinv  15695  grplmulf1o  15702  grpinvssd  15705  grpinvadd  15706  grpsubrcan  15709  grpsubadd  15715  grpaddsubass  15717  grppncan  15718  grpsubsub4  15720  grppnpcan2  15721  grpnpncan  15722  grpnnncan2  15723  grplactcnv  15726  mulgnn0dir  15752  mulgdirlem  15753  mulgneg2  15756  mulgnnass  15757  mulgnn0ass  15758  mulgass  15759  imasgrp  15773  nsgconj  15816  isnsg3  15817  nmzsubg  15824  ssnmz  15825  eqger  15833  eqgcpbl  15837  conjghm  15879  conjnmz  15882  conjnmzb  15883  subgga  15920  gass  15921  gasubg  15922  galcan  15924  gacan  15925  gapm  15926  gaorber  15928  gastacl  15929  gastacos  15930  cntzsubm  15955  cntzsubg  15956  oppgmnd  15971  symggen  16078  odmodnn0  16147  mndodconglem  16148  odmod  16153  odcong  16156  odmulgid  16159  odbezout  16163  gexdvdsi  16186  gexdvds  16187  sylow1lem2  16202  sylow1lem4  16204  sylow2blem1  16223  sylow2blem2  16224  sylow2blem3  16225  sylow3lem1  16230  sylow3lem2  16231  lsmass  16271  lsmmod  16276  lsmdisj2  16283  subgdisj1  16292  efgredleme  16344  efgredlemc  16346  efgcpbllemb  16356  frgp0  16361  frgpuplem  16373  abl32  16402  abladdsub4  16407  abladdsub  16408  ablpncan2  16409  ablsubsub  16411  mulgdi  16418  mulgsubdi  16421  odadd1  16434  odadd2  16435  gex2abl  16437  oddvdssubg  16441  cygabl  16471  ablfacrp  16672  pgpfac1lem2  16681  pgpfac1lem3a  16682  pgpfac1lem3  16683  pgpfac1lem4  16684  srgmulgass  16735  srgpcomp  16736  srgpcompp  16737  srgpcomppsc  16738  srgbinomlem3  16746  srgbinomlem4  16747  srgbinomlem  16748  csrgbinom  16750  rngcom  16779  rnglz  16787  rngrz  16788  rngnegl  16791  rngnegr  16792  rngmneg1  16793  rngmneg2  16794  rngsubdi  16796  rngsubdir  16797  mulgass2  16798  prdsrngd  16810  imasrng  16817  opprrng  16829  mulgass3  16835  dvdsrtr  16850  dvdsrmul1  16851  unitgrp  16865  dvrass  16888  dvrcan1  16889  dvrcan3  16890  irredrmul  16905  drngmul0or  16959  subrginv  16987  cntzsubr  17003  lmod0vs  17087  lmodvs0  17088  lmodvneg1  17094  lmodvsneg  17095  lmodcom  17097  lmodsubvs  17107  lmodsubdi  17108  lmodsubdir  17109  lssvsubcl  17131  lssvacl  17141  lssvscl  17142  islss3  17146  lss1d  17150  lssintcl  17151  prdslmodd  17156  lmodvsinv  17223  lmodvsinv2  17224  lmhmplusg  17231  lmhmvsca  17232  lsmcl  17270  pj1lmhm  17287  lvecvs0or  17295  lssvs0or  17297  lvecinv  17300  lspsnvs  17301  lspfixed  17315  lspexch  17316  lspsolvlem  17329  lspsolv  17330  lssacsex  17331  lspsnat  17332  lsppratlem1  17334  lsppratlem3  17336  lsppratlem4  17337  lbsextlem2  17346  lbsextlem4  17348  sralmod  17374  2idlcpbl  17422  unitrrg  17471  issubassa  17501  sraassa  17502  asclghm  17515  asclmul1  17516  asclmul2  17517  asclrhm  17518  psrbagcon  17546  psrbagconcl  17549  psrbagconf1o  17550  gsumbagdiaglem  17551  psrmulcllem  17564  psrlidm  17580  psrlidmOLD  17581  psrridm  17582  psrridmOLD  17583  psrass1  17584  psrdi  17585  psrdir  17586  psrass23l  17587  psrcom  17588  mplmon2mul  17690  evlslem1  17708  coe1subfv  17827  mulgrhm  18035  mulgrhmOLD  18038  cygznlem3  18111  evpmodpmf1o  18135  ipdi  18178  ip2di  18179  ipsubdir  18180  ipsubdi  18181  ip2subdi  18182  ipassr  18184  ipassr2  18185  ip2eq  18191  ocvlss  18206  lsmcss  18226  frlmphl  18315  frlmup1  18335  mamuass  18415  mamudi  18416  mamudir  18417  mamuvs1  18418  mamuvs2  18419  mavmulass  18471  mdetrlin  18524  mdetrsca  18525  mdetralt  18530  mdetunilem7  18540  mdetuni0  18543  matinv  18599  iinopn  18631  subbascn  18974  cnhaus  19074  nrmsep2  19076  nrmsep  19077  regsep2  19096  isreg2  19097  hauscmplem  19125  1stcfb  19165  2ndcctbss  19175  ptbasfi  19270  pthaus  19327  txtube  19329  txhaus  19336  xkohaus  19342  kqnrmlem1  19432  kqnrmlem2  19433  nrmr0reg  19438  nrmhmph  19483  fbssint  19527  infil  19552  fgabs  19568  filcon  19572  filuni  19574  trfil2  19576  trfg  19580  ufprim  19598  elfm3  19639  rnelfm  19642  fmfnfmlem2  19644  fmfnfmlem4  19646  hausflimi  19669  hauspwpwf1  19676  fclsneii  19706  supnfcls  19709  flimfnfcls  19717  fclscmpi  19718  alexsublem  19732  ghmcnp  19801  divstgpopn  19806  psmetsym  20002  psmettri  20003  psmetge0  20004  psmetres2  20006  xmetge0  20035  xmetsym  20038  xmettri  20042  xmetres2  20052  prdsxmetlem  20059  prdsmet  20061  imasdsf1olem  20064  imasf1oxmet  20066  bldisj  20089  xblss2ps  20092  xblss2  20093  xmeter  20124  prdsbl  20182  metustexhalfOLD  20254  metustexhalf  20255  metustOLD  20258  metust  20259  nrmmetd  20283  ngpsubcan  20321  nmmtri  20329  nmrtri  20331  ngptgp  20338  nlmvscnlem2  20382  nrginvrcnlem  20387  metdcnlem  20529  clmmulg  20781  cvsmuleqdivd  20799  cvsdiveqd  20800  cphabscl  20820  cphsqrcl2  20821  cphsqrcl3  20822  cphnmf  20830  cph2ass  20847  ipcau2  20865  tchcphlem2  20867  ipcnlem2  20872  cfilfcls  20901  iscau3  20905  iscmet3lem2  20919  iscmet3  20920  relcmpcmet  20943  minveclem2  21029  minveclem4  21035  pjthlem1  21040  pjthlem2  21041  uniioombllem4  21182  dyadmax  21194  itg1addlem4  21293  itg1climres  21308  ply1divex  21724  aalioulem2  21915  amgmlem  22499  dvdsppwf1o  22642  perfect1  22683  perfectlem1  22684  perfectlem2  22685  dchrptlem2  22720  colline  23177  ttgcontlem1  23266  axcontlem9  23353  eengtrkg  23366  eengtrkge  23367  4cycl4dv4e  23689  eupa0  23730  eupares  23731  eupap1  23732  grpoidinvlem4  23829  grpoasscan2  23860  grpoinvop  23863  grpopncan  23873  grponpcan  23874  grpopnpcan2  23875  grpodiveq  23878  gxcom  23891  gxnn0add  23896  ghgrp  23990  rngo2  24010  rngolz  24023  rngorz  24024  zerdivemp1  24056  vcm  24084  nvmul0or  24167  nvpncan2  24171  nvnncan  24178  nvdif  24188  nvabs  24196  smcnlem  24227  lnomul  24295  minvecolem2  24411  superpos  25893  ssnnssfz  26210  omndmul2  26309  omndmul3  26310  ogrpaddltbi  26316  ogrpaddltrbid  26318  ogrpsublt  26319  ogrpinvlt  26321  isarchi3  26338  archirngz  26340  archiabllem1a  26342  archiabllem1  26344  archiabllem2a  26345  archiabllem2c  26346  slmdvs0  26375  gsumvsca1  26385  gsumvsca2  26386  dvrdir  26392  rdivmuldivd  26393  dvrcan5  26395  ornglmullt  26409  isarchiofld  26419  rhmdvd  26423  rhmunitinv  26424  metideq  26454  metider  26455  pstmxmet  26458  lmxrge0  26516  qqhghm  26551  qqhrhm  26552  oddpwdc  26871  ballotlemiex  27018  wrdsplex  27073  cvmopnlem  27301  cvmliftmolem2  27305  cvmliftlem6  27313  cvmliftlem8  27315  cvmliftlem9  27316  cvmlift2lem9  27334  cvmlift3lem2  27343  cvmlift3lem6  27347  cvmlift3lem7  27348  cvmlift3lem9  27350  zprod  27584  nodense  27964  cgrtriv  28167  cgrdegen  28169  cgrextend  28173  segconeq  28175  btwntriv2  28177  btwncomand  28180  btwntriv1  28181  btwnintr  28184  btwnexch3  28185  btwnouttr  28189  btwnexch  28190  trisegint  28193  ifscgr  28209  btwnxfr  28221  colineartriv1  28232  colineartriv2  28233  colinearxfr  28240  fscgr  28245  lineid  28248  idinside  28249  endofsegidand  28251  btwnconn1lem5  28256  btwnconn1lem7  28258  btwnconn1lem11  28262  btwnconn1lem12  28263  btwnconn1lem13  28264  brsegle2  28274  segleantisym  28280  broutsideof2  28287  btwnoutside  28290  outsideoftr  28294  outsideofeq  28295  outsideofeu  28296  outsidele  28297  lineunray  28312  lineelsb2  28313  linecom  28315  linethru  28318  heicant  28564  neibastop1  28718  mettrifi  28791  isbnd3  28821  heibor1lem  28846  bfplem2  28860  ghomdiv  28887  zerdivemp1x  28899  irrapxlem5  29305  aomclem2  29546  isnumbasgrplem2  29598  mpaaeu  29645  mendrng  29687  mendlmod  29688  caofcan  29735  stoweidlem18  29951  stoweidlem41  29974  stoweidlem45  29978  stoweidlem55  29988  el2spthonot0  30528  usg2spthonot1  30547  clwlknclwlkdifnum  30717  frg2woteu  30786  numclwwlk5  30843  numclwwlk6  30844  ssnn0ssfz  30879  supgtoreq  30881  supfirege  30882  suprfinzcl  30883  zlmodzxzsub  30895  grpnpncan0  30905  invginvrid  30910  fsuppmapnn0fiublem  30936  telescfzgsumlem  30950  lmodvsmdi  30956  lmodvsmmulgdi  30957  assa2ass  30963  assamulgscmlem2  30965  ply1sclrmsm  30971  lply1binomsc  30998  dmatmul  31030  dmatsubcl  31031  lincsum  31070  lincscm  31071  lindslinindimp2lem4  31102  lindslinindsimp2lem5  31103  ldepsprlem  31113  lincresunit3lem1  31120  lincresunit3lem2  31121  isldepslvec2  31126  pmattomply1ghm  31270  cpscmatgsummon  31299  chfacfscmulgsum  31314  chfacfpmmulgsum  31318  chfacfpmmulgsum2  31319  cpmadugsumlemB  31328  cpmadugsumlemC  31329  cpmadugsumlemF  31330  lfladdcl  33022  lflvscl  33028  eqlkr3  33052  lkrlsp  33053  lshpkrlem4  33064  oldmm1  33168  olj01  33176  latmassOLD  33180  latm32  33182  latmrot  33183  latm4  33184  olm01  33187  cmtcomlemN  33199  cmtbr3N  33205  cmtbr4N  33206  lecmtN  33207  omlfh1N  33209  atlen0  33261  atnle  33268  atlatmstc  33270  atlatle  33271  cvlexchb1  33281  cvlcvr1  33290  ishlat3N  33305  hlatjass  33320  hlatj12  33321  hlatj32  33322  hlsupr2  33337  hlhgt2  33339  hl0lt1N  33340  hlrelat  33352  hlrelat2  33353  exatleN  33354  hlrelat3  33362  cvrval5  33365  cvrexchlem  33369  cvratlem  33371  cvrat  33372  atcvr0eq  33376  lnnat  33377  atlt  33387  atlelt  33388  2atlt  33389  atexchltN  33391  cvrat3  33392  2atjm  33395  atbtwn  33396  4noncolr3  33403  athgt  33406  3dimlem3a  33410  3dimlem3OLDN  33412  3dimlem4a  33413  3dimlem4OLDN  33415  3dim1  33417  3dim2  33418  1cvratex  33423  ps-1  33427  ps-2  33428  hlatexch3N  33430  hlatexch4  33431  ps-2b  33432  3atlem1  33433  3atlem2  33434  3atlem5  33437  3atlem6  33438  llnnleat  33463  llncmp  33472  2at0mat0  33475  2atmat0  33476  2atm  33477  lplni2  33487  lvolex3N  33488  lplnnle2at  33491  lplnnleat  33492  lplnnlelln  33493  2atnelpln  33494  llncvrlpln  33508  2atmat  33511  lplncmp  33512  lplnexllnN  33514  2llnjaN  33516  2llnm4  33520  2llnmeqat  33521  lvolnle3at  33532  lvolnleat  33533  2atnelvolN  33537  islvol2aN  33542  4atlem3  33546  4atlem3a  33547  4atlem3b  33548  4atlem4a  33549  4atlem4b  33550  4atlem4c  33551  4atlem4d  33552  4atlem10  33556  4atlem11b  33558  4atlem11  33559  4atlem12b  33561  4atlem12  33562  4at2  33564  lplncvrlvol  33566  lvolcmp  33567  2lplnja  33569  dalemqrprot  33598  dalemply  33604  dalemsly  33605  dalemrot  33607  dalemrotyz  33608  dalem1  33609  dalemcea  33610  dalem3  33614  dalem5  33617  dalem8  33620  dalem-cly  33621  dalem11  33624  dalem12  33625  dalem16  33629  dalem17  33630  dalem18  33631  dalem21  33644  dalem24  33647  dalem25  33648  dalem38  33660  dalem39  33661  dalem44  33666  dalem54  33676  dalem55  33677  dalem57  33679  dalem58  33680  dalem59  33681  dalem60  33682  dath2  33687  2atm2atN  33735  2llnma1b  33736  2llnma3r  33738  cdlema1N  33741  cdlemblem  33743  paddasslem5  33774  paddasslem10  33779  paddasslem12  33781  paddasslem13  33782  paddass  33788  padd12N  33789  padd4N  33790  paddss  33795  pmodlem1  33796  pmodl42N  33801  pmapjoin  33802  pmapjlln1  33805  atmod1i2  33809  llnmod1i2  33810  llnexchb2  33819  dalawlem2  33822  dalawlem3  33823  dalawlem5  33825  dalawlem6  33826  dalawlem7  33827  dalawlem8  33828  dalawlem11  33831  dalawlem12  33832  dalawlem13  33833  pclunN  33848  osumcllem1N  33906  pexmidlem3N  33922  lhp2lt  33951  lhp0lt  33953  lhpexle2lem  33959  lhpexle3lem  33961  lhpocnle  33966  lhpj1  33972  lhpmcvr4N  33976  lhp2at0  33982  lhpat3  33996  4atexlemtlw  34017  4atexlemc  34019  4atexlemnclw  34020  4atexlemcnd  34022  lautcvr  34042  lautj  34043  lautm  34044  ltrnm  34081  ltrnj  34082  ltrncvr  34083  trlval3  34137  cdlemc5  34145  cdlemd2  34149  cdlemd3  34150  cdleme0e  34167  cdleme1  34177  cdleme3c  34180  cdleme3g  34184  cdleme3h  34185  cdleme3  34187  cdleme5  34190  cdleme7c  34195  cdleme7d  34196  cdleme7e  34197  cdleme7ga  34198  cdleme7  34199  cdleme9  34203  cdleme11c  34211  cdleme11g  34215  cdleme11k  34218  cdleme11  34220  cdleme12  34221  cdleme15b  34225  cdleme15d  34227  cdleme16d  34231  cdleme16e  34232  cdleme16f  34233  cdleme17b  34237  cdleme18b  34242  cdleme22gb  34244  cdlemednpq  34249  cdleme19a  34253  cdleme20aN  34259  cdleme20bN  34260  cdleme20c  34261  cdleme20d  34262  cdleme20j  34268  cdleme21c  34277  cdleme22aa  34289  cdleme22b  34291  cdleme22cN  34292  cdleme22d  34293  cdleme22e  34294  cdleme22eALTN  34295  cdleme23b  34300  cdleme23c  34301  cdleme28a  34320  cdleme30a  34328  cdlemefs29bpre0N  34366  cdlemefs29bpre1N  34367  cdlemefs29cpre1N  34368  cdlemefs29clN  34369  cdlemefs32fvaN  34372  cdlemefs32fva1  34373  cdleme32b  34392  cdleme32c  34393  cdleme32e  34395  cdleme35a  34398  cdleme35fnpq  34399  cdleme35b  34400  cdleme35f  34404  cdleme36a  34410  cdleme36m  34411  cdleme37m  34412  cdleme39a  34415  cdleme42c  34422  cdleme42i  34433  cdleme42keg  34436  cdleme42mgN  34438  cdleme48bw  34452  cdlemeg46fjgN  34471  cdlemeg46fjv  34473  cdlemeg46req  34479  cdleme50trn1  34499  cdlemf1  34511  cdlemf2  34512  cdlemg1cex  34538  cdlemg2fv2  34550  cdlemg7fvbwN  34557  cdlemg4c  34562  cdlemg4  34567  cdlemg6c  34570  cdlemg8b  34578  cdlemg10c  34589  cdlemg10  34591  cdlemg11b  34592  cdlemg12f  34598  cdlemg13a  34601  cdlemg17a  34611  cdlemg17dALTN  34614  cdlemg18b  34629  cdlemg19a  34633  cdlemg27a  34642  cdlemg27b  34646  cdlemg33b0  34651  cdlemg33a  34656  cdlemg35  34663  trlcolem  34676  cdlemg42  34679  cdlemg46  34685  trljco  34690  tendopltp  34730  cdlemh1  34765  cdlemh2  34766  cdlemi1  34768  cdlemi  34770  cdlemk3  34783  cdlemk10  34793  cdlemk11  34799  cdlemk15  34805  cdlemk1u  34809  cdlemk5u  34811  cdlemk11u  34821  cdlemk39  34866  cdlemkid1  34872  cdlemk50  34902  cdlemk51  34903  erngdvlem3-rN  34948  tendocnv  34972  tendospcanN  34974  dialss  34997  dia2dimlem1  35015  dia2dimlem2  35016  dia2dimlem3  35017  dia2dimlem10  35024  dia2dimlem12  35026  dvhvaddass  35048  dvhlveclem  35059  cdlemm10N  35069  doca2N  35077  djajN  35088  dib1dim2  35119  diblss  35121  diclspsn  35145  cdlemn2  35146  cdlemn10  35157  dihjustlem  35167  dihord1  35169  dihord2a  35170  dihord2pre2  35177  dib2dim  35194  dih2dimb  35195  dih2dimbALTN  35196  dihopelvalcpre  35199  dihord5b  35210  dihord6b  35211  dihord5apre  35213  dihmeetlem1N  35241  dihglblem5apreN  35242  dihglblem2N  35245  dihglbcpreN  35251  dihmeetbclemN  35255  dihmeetlem3N  35256  dihmeetlem6  35260  dih1dimatlem  35280  djhcvat42  35366  dihjatcclem1  35369  dihjatcclem4  35372  dvh4dimat  35389  lcfl7lem  35450  lclkrlem2m  35470  lcfrlem1  35493  lcdvsass  35558  baerlem3lem1  35658  baerlem5alem1  35659  baerlem5blem1  35660  mapdh6gN  35693  mapdh6hN  35694  hdmap1l6g  35768  hdmap1l6h  35769  hdmapneg  35800  hdmap14lem8  35829  hgmapadd  35848  hgmapmul  35849  hgmapvvlem1  35877
  Copyright terms: Public domain W3C validator