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

Theorem syl13anc 1213
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 1161 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 654 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  syl23anc  1218  syl33anc  1226  pm2.61da3ne  2681  disjxiun  4277  wereu2  4704  ordelord  4728  caovassd  6251  caovcand  6254  caovordid  6258  caovordd  6260  caovdid  6267  caovdird  6270  swoer  7117  swoord1  7118  swoord2  7119  frfi  7545  indexfi  7607  ssfii  7657  elfiun  7668  suplub2  7699  wemaplem2  7749  htalem  8091  cofsmo  8426  alephsing  8433  sornom  8434  axdc3lem4  8610  zorn2lem1  8653  ttukeylem6  8671  ttukeylem7  8672  prlem934  9189  fzosubel3  11584  seqsplit  11822  seqcaopr  11826  ccatass  12269  wrdcctswrd  12342  wrdeqcats1  12351  wrdeqs1cat  12352  splid  12378  spllen  12379  splfv1  12380  splfv2a  12381  splval2  12382  swrds2  12528  isercolllem2  13126  fsumiun  13266  pcgcd1  13925  cshwsidrepswmod0  14103  cshwshashlem2  14105  cshwsdisj  14107  firest  14353  iscatd2  14601  posasymb  15104  joinle  15166  meetle  15180  lattrd  15210  latleeqj1  15215  latjlej1  15217  latjlej12  15219  latnlej2  15223  latjidm  15226  latleeqm1  15231  latmlem1  15233  latmlem12  15235  latmidm  15238  latledi  15241  latjass  15247  latj12  15248  latj13  15250  latj31  15251  latjrot  15252  latj4  15253  mod1ile  15257  lubun  15275  clatleglb  15278  latdisdlem  15341  mnd32g  15406  mnd12g  15407  mnd4g  15408  prdsmndd  15436  imasmnd  15441  mrcmndind  15475  gsumspl  15501  grpidrcan  15570  grpidlcan  15571  grpinvinv  15572  grplmulf1o  15579  grpinvssd  15582  grpinvadd  15583  grpsubrcan  15586  grpsubadd  15592  grpaddsubass  15594  grppncan  15595  grpsubsub4  15597  grppnpcan2  15598  grpnpncan  15599  grpnnncan2  15600  grplactcnv  15603  mulgnn0dir  15629  mulgdirlem  15630  mulgneg2  15633  mulgnnass  15634  mulgnn0ass  15635  mulgass  15636  imasgrp  15650  nsgconj  15693  isnsg3  15694  nmzsubg  15701  ssnmz  15702  eqger  15710  eqgcpbl  15714  conjghm  15756  conjnmz  15759  conjnmzb  15760  subgga  15797  gass  15798  gasubg  15799  galcan  15801  gacan  15802  gapm  15803  gaorber  15805  gastacl  15806  gastacos  15807  cntzsubm  15832  cntzsubg  15833  oppgmnd  15848  symggen  15955  odmodnn0  16022  mndodconglem  16023  odmod  16028  odcong  16031  odmulgid  16034  odbezout  16038  gexdvdsi  16061  gexdvds  16062  sylow1lem2  16077  sylow1lem4  16079  sylow2blem1  16098  sylow2blem2  16099  sylow2blem3  16100  sylow3lem1  16105  sylow3lem2  16106  lsmass  16146  lsmmod  16151  lsmdisj2  16158  subgdisj1  16167  efgredleme  16219  efgredlemc  16221  efgcpbllemb  16231  frgp0  16236  frgpuplem  16248  abl32  16277  abladdsub4  16282  abladdsub  16283  ablpncan2  16284  ablsubsub  16286  mulgdi  16293  mulgsubdi  16296  odadd1  16309  odadd2  16310  gex2abl  16312  oddvdssubg  16316  cygabl  16346  ablfacrp  16540  pgpfac1lem2  16549  pgpfac1lem3a  16550  pgpfac1lem3  16551  pgpfac1lem4  16552  rngcom  16608  rnglz  16616  rngrz  16617  rngnegl  16619  rngnegr  16620  rngmneg1  16621  rngmneg2  16622  rngsubdi  16624  rngsubdir  16625  mulgass2  16626  prdsrngd  16638  imasrng  16645  opprrng  16656  mulgass3  16662  dvdsrtr  16677  dvdsrmul1  16678  unitgrp  16692  dvrass  16715  dvrcan1  16716  dvrcan3  16717  irredrmul  16732  drngmul0or  16776  subrginv  16804  cntzsubr  16820  lmod0vs  16904  lmodvs0  16905  lmodvneg1  16911  lmodvsneg  16912  lmodcom  16914  lmodsubvs  16924  lmodsubdi  16925  lmodsubdir  16926  lssvsubcl  16946  lssvacl  16956  lssvscl  16957  islss3  16961  lss1d  16965  lssintcl  16966  prdslmodd  16971  lmodvsinv  17038  lmodvsinv2  17039  lmhmplusg  17046  lmhmvsca  17047  lsmcl  17085  pj1lmhm  17102  lvecvs0or  17110  lssvs0or  17112  lvecinv  17115  lspsnvs  17116  lspfixed  17130  lspexch  17131  lspsolvlem  17144  lspsolv  17145  lssacsex  17146  lspsnat  17147  lsppratlem1  17149  lsppratlem3  17151  lsppratlem4  17152  lbsextlem2  17161  lbsextlem4  17163  sralmod  17189  2idlcpbl  17237  unitrrg  17286  issubassa  17316  sraassa  17317  asclghm  17330  asclmul1  17331  asclmul2  17332  asclrhm  17333  psrbagcon  17373  psrbagconcl  17376  psrbagconf1o  17377  gsumbagdiaglem  17378  psrmulcllem  17391  psrlidm  17407  psrlidmOLD  17408  psrridm  17409  psrridmOLD  17410  psrass1  17411  psrdi  17412  psrdir  17413  psrcom  17414  psrass23  17415  mplmon2mul  17514  coe1subfv  17617  mulgrhm  17767  mulgrhmOLD  17770  cygznlem3  17843  evpmodpmf1o  17867  ipdi  17910  ip2di  17911  ipsubdir  17912  ipsubdi  17913  ip2subdi  17914  ipassr  17916  ipassr2  17917  ip2eq  17923  ocvlss  17938  lsmcss  17958  frlmphl  18047  frlmup1  18067  mamuass  18147  mamudi  18148  mamudir  18149  mamuvs1  18150  mamuvs2  18151  mavmulass  18201  mdetrlin  18250  mdetrsca  18251  mdetralt  18255  mdetunilem7  18265  mdetuni0  18268  matinv  18324  iinopn  18356  subbascn  18699  cnhaus  18799  nrmsep2  18801  nrmsep  18802  regsep2  18821  isreg2  18822  hauscmplem  18850  1stcfb  18890  2ndcctbss  18900  ptbasfi  18995  pthaus  19052  txtube  19054  txhaus  19061  xkohaus  19067  kqnrmlem1  19157  kqnrmlem2  19158  nrmr0reg  19163  nrmhmph  19208  fbssint  19252  infil  19277  fgabs  19293  filcon  19297  filuni  19299  trfil2  19301  trfg  19305  ufprim  19323  elfm3  19364  rnelfm  19367  fmfnfmlem2  19369  fmfnfmlem4  19371  hausflimi  19394  hauspwpwf1  19401  fclsneii  19431  supnfcls  19434  flimfnfcls  19442  fclscmpi  19443  alexsublem  19457  ghmcnp  19526  divstgpopn  19531  psmetsym  19727  psmettri  19728  psmetge0  19729  psmetres2  19731  xmetge0  19760  xmetsym  19763  xmettri  19767  xmetres2  19777  prdsxmetlem  19784  prdsmet  19786  imasdsf1olem  19789  imasf1oxmet  19791  bldisj  19814  xblss2ps  19817  xblss2  19818  xmeter  19849  prdsbl  19907  metustexhalfOLD  19979  metustexhalf  19980  metustOLD  19983  metust  19984  nrmmetd  20008  ngpsubcan  20046  nmmtri  20054  nmrtri  20056  ngptgp  20063  nlmvscnlem2  20107  nrginvrcnlem  20112  metdcnlem  20254  clmmulg  20506  cvsmuleqdivd  20524  cvsdiveqd  20525  cphabscl  20545  cphsqrcl2  20546  cphsqrcl3  20547  cphnmf  20555  cph2ass  20572  ipcau2  20590  tchcphlem2  20592  ipcnlem2  20597  cfilfcls  20626  iscau3  20630  iscmet3lem2  20644  iscmet3  20645  relcmpcmet  20668  minveclem2  20754  minveclem4  20760  pjthlem1  20765  pjthlem2  20766  uniioombllem4  20907  dyadmax  20919  itg1addlem4  21018  itg1climres  21033  evlslem1  21366  ply1divex  21492  aalioulem2  21683  amgmlem  22267  dvdsppwf1o  22410  perfect1  22451  perfectlem1  22452  perfectlem2  22453  dchrptlem2  22488  colline  22917  ttgcontlem1  22953  axcontlem9  23040  eengtrkg  23053  eengtrkge  23054  4cycl4dv4e  23376  eupa0  23417  eupares  23418  eupap1  23419  grpoidinvlem4  23516  grpoasscan2  23547  grpoinvop  23550  grpopncan  23560  grponpcan  23561  grpopnpcan2  23562  grpodiveq  23565  gxcom  23578  gxnn0add  23583  ghgrp  23677  rngo2  23697  rngolz  23710  rngorz  23711  zerdivemp1  23743  vcm  23771  nvmul0or  23854  nvpncan2  23858  nvnncan  23865  nvdif  23875  nvabs  23883  smcnlem  23914  lnomul  23982  minvecolem2  24098  superpos  25580  ssnnssfz  25898  omndmul2  25998  omndmul3  25999  ogrpaddltbi  26005  ogrpaddltrbid  26007  ogrpsublt  26008  ogrpinvlt  26010  isarchi3  26027  archirngz  26029  archiabllem1a  26031  archiabllem1  26033  archiabllem2a  26034  archiabllem2c  26035  slmdvs0  26089  gsumvsca1  26103  gsumvsca2  26104  dvrdir  26110  rdivmuldivd  26111  dvrcan5  26113  ornglmullt  26127  isarchiofld  26137  rhmdvd  26141  rhmunitinv  26142  metideq  26173  metider  26174  pstmxmet  26177  lmxrge0  26235  qqhghm  26270  qqhrhm  26271  oddpwdc  26584  ballotlemiex  26731  wrdsplex  26786  cvmopnlem  27014  cvmliftmolem2  27018  cvmliftlem6  27026  cvmliftlem8  27028  cvmliftlem9  27029  cvmlift2lem9  27047  cvmlift3lem2  27056  cvmlift3lem6  27060  cvmlift3lem7  27061  cvmlift3lem9  27063  zprod  27296  nodense  27676  cgrtriv  27879  cgrdegen  27881  cgrextend  27885  segconeq  27887  btwntriv2  27889  btwncomand  27892  btwntriv1  27893  btwnintr  27896  btwnexch3  27897  btwnouttr  27901  btwnexch  27902  trisegint  27905  ifscgr  27921  btwnxfr  27933  colineartriv1  27944  colineartriv2  27945  colinearxfr  27952  fscgr  27957  lineid  27960  idinside  27961  endofsegidand  27963  btwnconn1lem5  27968  btwnconn1lem7  27970  btwnconn1lem11  27974  btwnconn1lem12  27975  btwnconn1lem13  27976  brsegle2  27986  segleantisym  27992  broutsideof2  27999  btwnoutside  28002  outsideoftr  28006  outsideofeq  28007  outsideofeu  28008  outsidele  28009  lineunray  28024  lineelsb2  28025  linecom  28027  linethru  28030  heicant  28267  neibastop1  28421  mettrifi  28494  isbnd3  28524  heibor1lem  28549  bfplem2  28563  ghomdiv  28590  zerdivemp1x  28602  irrapxlem5  29009  aomclem2  29250  isnumbasgrplem2  29302  mpaaeu  29349  mendrng  29391  mendlmod  29392  caofcan  29439  stoweidlem18  29656  stoweidlem41  29679  stoweidlem45  29683  stoweidlem55  29693  el2spthonot0  30233  usg2spthonot1  30252  clwlknclwlkdifnum  30422  frg2woteu  30491  numclwwlk5  30548  numclwwlk6  30549  zlmodzxzsub  30588  invginvrid  30600  lincsum  30669  lincscm  30670  lindslinindimp2lem4  30701  lindslinindsimp2lem5  30702  ldepsprlem  30712  lincresunit3lem1  30719  lincresunit3lem2  30720  isldepslvec2  30725  lfladdcl  32286  lflvscl  32292  eqlkr3  32316  lkrlsp  32317  lshpkrlem4  32328  oldmm1  32432  olj01  32440  latmassOLD  32444  latm32  32446  latmrot  32447  latm4  32448  olm01  32451  cmtcomlemN  32463  cmtbr3N  32469  cmtbr4N  32470  lecmtN  32471  omlfh1N  32473  atlen0  32525  atnle  32532  atlatmstc  32534  atlatle  32535  cvlexchb1  32545  cvlcvr1  32554  ishlat3N  32569  hlatjass  32584  hlatj12  32585  hlatj32  32586  hlsupr2  32601  hlhgt2  32603  hl0lt1N  32604  hlrelat  32616  hlrelat2  32617  exatleN  32618  hlrelat3  32626  cvrval5  32629  cvrexchlem  32633  cvratlem  32635  cvrat  32636  atcvr0eq  32640  lnnat  32641  atlt  32651  atlelt  32652  2atlt  32653  atexchltN  32655  cvrat3  32656  2atjm  32659  atbtwn  32660  4noncolr3  32667  athgt  32670  3dimlem3a  32674  3dimlem3OLDN  32676  3dimlem4a  32677  3dimlem4OLDN  32679  3dim1  32681  3dim2  32682  1cvratex  32687  ps-1  32691  ps-2  32692  hlatexch3N  32694  hlatexch4  32695  ps-2b  32696  3atlem1  32697  3atlem2  32698  3atlem5  32701  3atlem6  32702  llnnleat  32727  llncmp  32736  2at0mat0  32739  2atmat0  32740  2atm  32741  lplni2  32751  lvolex3N  32752  lplnnle2at  32755  lplnnleat  32756  lplnnlelln  32757  2atnelpln  32758  llncvrlpln  32772  2atmat  32775  lplncmp  32776  lplnexllnN  32778  2llnjaN  32780  2llnm4  32784  2llnmeqat  32785  lvolnle3at  32796  lvolnleat  32797  2atnelvolN  32801  islvol2aN  32806  4atlem3  32810  4atlem3a  32811  4atlem3b  32812  4atlem4a  32813  4atlem4b  32814  4atlem4c  32815  4atlem4d  32816  4atlem10  32820  4atlem11b  32822  4atlem11  32823  4atlem12b  32825  4atlem12  32826  4at2  32828  lplncvrlvol  32830  lvolcmp  32831  2lplnja  32833  dalemqrprot  32862  dalemply  32868  dalemsly  32869  dalemrot  32871  dalemrotyz  32872  dalem1  32873  dalemcea  32874  dalem3  32878  dalem5  32881  dalem8  32884  dalem-cly  32885  dalem11  32888  dalem12  32889  dalem16  32893  dalem17  32894  dalem18  32895  dalem21  32908  dalem24  32911  dalem25  32912  dalem38  32924  dalem39  32925  dalem44  32930  dalem54  32940  dalem55  32941  dalem57  32943  dalem58  32944  dalem59  32945  dalem60  32946  dath2  32951  2atm2atN  32999  2llnma1b  33000  2llnma3r  33002  cdlema1N  33005  cdlemblem  33007  paddasslem5  33038  paddasslem10  33043  paddasslem12  33045  paddasslem13  33046  paddass  33052  padd12N  33053  padd4N  33054  paddss  33059  pmodlem1  33060  pmodl42N  33065  pmapjoin  33066  pmapjlln1  33069  atmod1i2  33073  llnmod1i2  33074  llnexchb2  33083  dalawlem2  33086  dalawlem3  33087  dalawlem5  33089  dalawlem6  33090  dalawlem7  33091  dalawlem8  33092  dalawlem11  33095  dalawlem12  33096  dalawlem13  33097  pclunN  33112  osumcllem1N  33170  pexmidlem3N  33186  lhp2lt  33215  lhp0lt  33217  lhpexle2lem  33223  lhpexle3lem  33225  lhpocnle  33230  lhpj1  33236  lhpmcvr4N  33240  lhp2at0  33246  lhpat3  33260  4atexlemtlw  33281  4atexlemc  33283  4atexlemnclw  33284  4atexlemcnd  33286  lautcvr  33306  lautj  33307  lautm  33308  ltrnm  33345  ltrnj  33346  ltrncvr  33347  trlval3  33401  cdlemc5  33409  cdlemd2  33413  cdlemd3  33414  cdleme0e  33431  cdleme1  33441  cdleme3c  33444  cdleme3g  33448  cdleme3h  33449  cdleme3  33451  cdleme5  33454  cdleme7c  33459  cdleme7d  33460  cdleme7e  33461  cdleme7ga  33462  cdleme7  33463  cdleme9  33467  cdleme11c  33475  cdleme11g  33479  cdleme11k  33482  cdleme11  33484  cdleme12  33485  cdleme15b  33489  cdleme15d  33491  cdleme16d  33495  cdleme16e  33496  cdleme16f  33497  cdleme17b  33501  cdleme18b  33506  cdleme22gb  33508  cdlemednpq  33513  cdleme19a  33517  cdleme20aN  33523  cdleme20bN  33524  cdleme20c  33525  cdleme20d  33526  cdleme20j  33532  cdleme21c  33541  cdleme22aa  33553  cdleme22b  33555  cdleme22cN  33556  cdleme22d  33557  cdleme22e  33558  cdleme22eALTN  33559  cdleme23b  33564  cdleme23c  33565  cdleme28a  33584  cdleme30a  33592  cdlemefs29bpre0N  33630  cdlemefs29bpre1N  33631  cdlemefs29cpre1N  33632  cdlemefs29clN  33633  cdlemefs32fvaN  33636  cdlemefs32fva1  33637  cdleme32b  33656  cdleme32c  33657  cdleme32e  33659  cdleme35a  33662  cdleme35fnpq  33663  cdleme35b  33664  cdleme35f  33668  cdleme36a  33674  cdleme36m  33675  cdleme37m  33676  cdleme39a  33679  cdleme42c  33686  cdleme42i  33697  cdleme42keg  33700  cdleme42mgN  33702  cdleme48bw  33716  cdlemeg46fjgN  33735  cdlemeg46fjv  33737  cdlemeg46req  33743  cdleme50trn1  33763  cdlemf1  33775  cdlemf2  33776  cdlemg1cex  33802  cdlemg2fv2  33814  cdlemg7fvbwN  33821  cdlemg4c  33826  cdlemg4  33831  cdlemg6c  33834  cdlemg8b  33842  cdlemg10c  33853  cdlemg10  33855  cdlemg11b  33856  cdlemg12f  33862  cdlemg13a  33865  cdlemg17a  33875  cdlemg17dALTN  33878  cdlemg18b  33893  cdlemg19a  33897  cdlemg27a  33906  cdlemg27b  33910  cdlemg33b0  33915  cdlemg33a  33920  cdlemg35  33927  trlcolem  33940  cdlemg42  33943  cdlemg46  33949  trljco  33954  tendopltp  33994  cdlemh1  34029  cdlemh2  34030  cdlemi1  34032  cdlemi  34034  cdlemk3  34047  cdlemk10  34057  cdlemk11  34063  cdlemk15  34069  cdlemk1u  34073  cdlemk5u  34075  cdlemk11u  34085  cdlemk39  34130  cdlemkid1  34136  cdlemk50  34166  cdlemk51  34167  erngdvlem3-rN  34212  tendocnv  34236  tendospcanN  34238  dialss  34261  dia2dimlem1  34279  dia2dimlem2  34280  dia2dimlem3  34281  dia2dimlem10  34288  dia2dimlem12  34290  dvhvaddass  34312  dvhlveclem  34323  cdlemm10N  34333  doca2N  34341  djajN  34352  dib1dim2  34383  diblss  34385  diclspsn  34409  cdlemn2  34410  cdlemn10  34421  dihjustlem  34431  dihord1  34433  dihord2a  34434  dihord2pre2  34441  dib2dim  34458  dih2dimb  34459  dih2dimbALTN  34460  dihopelvalcpre  34463  dihord5b  34474  dihord6b  34475  dihord5apre  34477  dihmeetlem1N  34505  dihglblem5apreN  34506  dihglblem2N  34509  dihglbcpreN  34515  dihmeetbclemN  34519  dihmeetlem3N  34520  dihmeetlem6  34524  dih1dimatlem  34544  djhcvat42  34630  dihjatcclem1  34633  dihjatcclem4  34636  dvh4dimat  34653  lcfl7lem  34714  lclkrlem2m  34734  lcfrlem1  34757  lcdvsass  34822  baerlem3lem1  34922  baerlem5alem1  34923  baerlem5blem1  34924  mapdh6gN  34957  mapdh6hN  34958  hdmap1l6g  35032  hdmap1l6h  35033  hdmapneg  35064  hdmap14lem8  35093  hgmapadd  35112  hgmapmul  35113  hgmapvvlem1  35141
  Copyright terms: Public domain W3C validator