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

Theorem syl13anc 1229
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 1175 . 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 972
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 974
This theorem is referenced by:  syl23anc  1234  syl33anc  1242  pm2.61da3neOLD  2762  disjxiun  4431  wereu2  4863  ordelord  4887  caovassd  6456  caovcand  6459  caovordid  6463  caovordd  6465  caovdid  6472  caovdird  6475  swoer  7338  swoord1  7339  swoord2  7340  frfi  7764  indexfi  7827  ssfii  7878  elfiun  7889  suplub2  7920  supgtoreq  7928  wemaplem2  7972  htalem  8314  cofsmo  8649  alephsing  8656  sornom  8657  axdc3lem4  8833  zorn2lem1  8876  ttukeylem6  8894  ttukeylem7  8895  prlem934  9411  supfirege  10528  suprfinzcl  10980  fzosubel3  11853  fsuppmapnn0fiublem  12072  seqsplit  12116  seqcaopr  12120  ccatass  12581  wrdcctswrd  12666  wrdeqcats1  12675  wrdeqs1cat  12676  splid  12705  spllen  12706  splfv1  12707  splfv2a  12708  splval2  12709  swrds2  12859  isercolllem2  13464  fsumiun  13611  pcgcd1  14274  cshwsidrepswmod0  14453  cshwshashlem2  14455  cshwsdisj  14457  firest  14704  iscatd2  14952  posasymb  15453  joinle  15515  meetle  15529  lattrd  15559  latleeqj1  15564  latjlej1  15566  latjlej12  15568  latnlej2  15572  latjidm  15575  latleeqm1  15580  latmlem1  15582  latmlem12  15584  latmidm  15587  latledi  15590  latjass  15596  latj12  15597  latj13  15599  latj31  15600  latjrot  15601  latj4  15602  mod1ile  15606  lubun  15624  clatleglb  15627  latdisdlem  15690  mnd32g  15806  mnd12g  15807  mnd4g  15808  ismndd  15814  prdsmndd  15824  imasmnd  15829  mrcmndind  15868  gsumspl  15883  grpidrcan  15974  grpidlcan  15975  grpinvinv  15976  grplmulf1o  15983  grpinvssd  15986  grpinvadd  15987  grpsubrcan  15990  grpsubadd  15997  grpaddsubass  15999  grppncan  16000  grpsubsub4  16002  grppnpcan2  16003  grpnpncan  16004  grpnpncan0  16005  grpnnncan2  16006  grplactcnv  16009  mulgnn0dir  16036  mulgdirlem  16037  mulgneg2  16040  mulgnnass  16041  mulgnn0ass  16042  mulgass  16043  imasgrp  16057  mhmmnd  16063  nsgconj  16105  isnsg3  16106  nmzsubg  16113  ssnmz  16114  eqger  16122  eqgcpbl  16126  conjghm  16168  conjnmz  16171  conjnmzb  16172  subgga  16209  gass  16210  gasubg  16211  galcan  16213  gacan  16214  gapm  16215  gaorber  16217  gastacl  16218  gastacos  16219  cntzsubm  16244  cntzsubg  16245  oppgmnd  16260  symggen  16366  odmodnn0  16435  mndodconglem  16436  odmod  16441  odcong  16444  odmulgid  16447  odbezout  16451  gexdvdsi  16474  gexdvds  16475  sylow1lem2  16490  sylow1lem4  16492  sylow2blem1  16511  sylow2blem2  16512  sylow2blem3  16513  sylow3lem1  16518  sylow3lem2  16519  lsmass  16559  lsmmod  16564  lsmdisj2  16571  subgdisj1  16580  efgredleme  16632  efgredlemc  16634  efgcpbllemb  16644  frgp0  16649  frgpuplem  16661  abl32  16690  abladdsub4  16695  abladdsub  16696  ablpncan2  16697  ablsubsub  16699  mulgdi  16706  mulgsubdi  16709  odadd1  16725  odadd2  16726  gex2abl  16728  oddvdssubg  16732  cygabl  16764  telgsumfzslem  16888  ablfacrp  16988  pgpfac1lem2  16997  pgpfac1lem3a  16998  pgpfac1lem3  16999  pgpfac1lem4  17000  srgmulgass  17053  srgpcomp  17054  srgpcompp  17055  srgpcomppsc  17056  srgbinomlem3  17064  srgbinomlem4  17065  srgbinomlem  17066  csrgbinom  17068  ringcom  17098  ringlz  17106  ringrz  17107  ringnegl  17111  rngnegr  17112  ringmneg1  17113  ringmneg2  17114  ringsubdi  17116  rngsubdir  17117  mulgass2  17118  prdsringd  17132  imasring  17139  opprring  17151  mulgass3  17157  dvdsrtr  17172  dvdsrmul1  17173  unitgrp  17187  dvrass  17210  dvrcan1  17211  dvrcan3  17212  irredrmul  17227  drngmul0or  17288  subrginv  17316  cntzsubr  17332  lmod0vs  17416  lmodvs0  17417  lmodvsmmulgdi  17418  lmodvneg1  17424  lmodvsneg  17425  lmodcom  17427  lmodsubvs  17437  lmodsubdi  17438  lmodsubdir  17439  lssvsubcl  17461  lssvacl  17471  lssvscl  17472  islss3  17476  lss1d  17480  lssintcl  17481  prdslmodd  17486  lmodvsinv  17553  lmodvsinv2  17554  lmhmplusg  17561  lmhmvsca  17562  lsmcl  17600  pj1lmhm  17617  lvecvs0or  17625  lssvs0or  17627  lvecinv  17630  lspsnvs  17631  lspfixed  17645  lspexch  17646  lspsolvlem  17659  lspsolv  17660  lssacsex  17661  lspsnat  17662  lsppratlem1  17664  lsppratlem3  17666  lsppratlem4  17667  lbsextlem2  17676  lbsextlem4  17678  sralmod  17704  2idlcpbl  17753  unitrrg  17813  assa2ass  17842  issubassa  17844  sraassa  17845  asclghm  17858  asclmul1  17859  asclmul2  17860  asclrhm  17862  assamulgscmlem2  17869  psrbagcon  17893  psrbagconcl  17896  psrbagconf1o  17897  gsumbagdiaglem  17898  psrmulcllem  17911  psrlidm  17927  psrlidmOLD  17928  psrridm  17929  psrridmOLD  17930  psrass1  17931  psrdi  17932  psrdir  17933  psrass23l  17934  psrcom  17935  mplmon2mul  18037  evlslem1  18055  coe1subfv  18178  lply1binomsc  18220  mulgrhm  18402  mulgrhmOLD  18405  cygznlem3  18478  evpmodpmf1o  18502  ipdi  18545  ip2di  18546  ipsubdir  18547  ipsubdi  18548  ip2subdi  18549  ipassr  18551  ipassr2  18552  ip2eq  18558  ocvlss  18573  lsmcss  18593  frlmphl  18682  frlmup1  18702  mamuass  18774  mamudi  18775  mamudir  18776  mamuvs1  18777  mamuvs2  18778  dmatmul  18869  dmatsubcl  18870  scmataddcl  18888  smatvscl  18896  scmatghm  18905  mavmulass  18921  mdetrlin  18974  mdetrsca  18975  mdetralt  18980  mdetunilem7  18990  mdetuni0  18993  matinv  19049  pm2mpghm  19187  chpscmatgsummon  19216  chfacfscmulgsum  19231  chfacfpmmulgsum  19235  chfacfpmmulgsum2  19236  cpmadugsumlemB  19245  cpmadugsumlemC  19246  cpmadugsumlemF  19247  iinopn  19281  subbascn  19625  cnhaus  19725  nrmsep2  19727  nrmsep  19728  regsep2  19747  isreg2  19748  hauscmplem  19776  1stcfb  19816  2ndcctbss  19826  ptbasfi  19952  pthaus  20009  txtube  20011  txhaus  20018  xkohaus  20024  kqnrmlem1  20114  kqnrmlem2  20115  nrmr0reg  20120  nrmhmph  20165  fbssint  20209  infil  20234  fgabs  20250  filcon  20254  filuni  20256  trfil2  20258  trfg  20262  ufprim  20280  elfm3  20321  rnelfm  20324  fmfnfmlem2  20326  fmfnfmlem4  20328  hausflimi  20351  hauspwpwf1  20358  fclsneii  20388  supnfcls  20391  flimfnfcls  20399  fclscmpi  20400  alexsublem  20414  ghmcnp  20483  qustgpopn  20488  psmetsym  20684  psmettri  20685  psmetge0  20686  psmetres2  20688  xmetge0  20717  xmetsym  20720  xmettri  20724  xmetres2  20734  prdsxmetlem  20741  prdsmet  20743  imasdsf1olem  20746  imasf1oxmet  20748  bldisj  20771  xblss2ps  20774  xblss2  20775  xmeter  20806  prdsbl  20864  metustexhalfOLD  20936  metustexhalf  20937  metustOLD  20940  metust  20941  nrmmetd  20965  ngpsubcan  21003  nmmtri  21011  nmrtri  21013  ngptgp  21020  nlmvscnlem2  21064  nrginvrcnlem  21069  metdcnlem  21211  clmmulg  21463  cvsmuleqdivd  21481  cvsdiveqd  21482  cphabscl  21502  cphsqrtcl2  21503  cphsqrtcl3  21504  cphnmf  21512  cph2ass  21529  ipcau2  21547  tchcphlem2  21549  ipcnlem2  21554  cfilfcls  21583  iscau3  21587  iscmet3lem2  21601  iscmet3  21602  relcmpcmet  21625  minveclem2  21711  minveclem4  21717  pjthlem1  21722  pjthlem2  21723  uniioombllem4  21865  dyadmax  21877  itg1addlem4  21976  itg1climres  21991  ply1divex  22407  aalioulem2  22598  amgmlem  23188  dvdsppwf1o  23331  perfect1  23372  perfectlem1  23373  perfectlem2  23374  dchrptlem2  23409  colline  23899  ttgcontlem1  24057  axcontlem9  24144  eengtrkg  24157  eengtrkge  24158  4cycl4dv4e  24537  el2spthonot0  24740  usg2spthonot1  24759  clwlknclwlkdifnum  24830  eupa0  24843  eupares  24844  eupap1  24845  frg2woteu  24924  numclwwlk5  24981  numclwwlk6  24982  grpoidinvlem4  25078  grpoasscan2  25109  grpoinvop  25112  grpopncan  25122  grponpcan  25123  grpopnpcan2  25124  grpodiveq  25127  gxcom  25140  gxnn0add  25145  ghgrpOLD  25239  rngo2  25259  rngolz  25272  rngorz  25273  zerdivemp1  25305  vcm  25333  nvmul0or  25416  nvpncan2  25420  nvnncan  25427  nvdif  25437  nvabs  25445  smcnlem  25476  lnomul  25544  minvecolem2  25660  superpos  27142  ssnnssfz  27466  omndmul2  27572  omndmul3  27573  ogrpaddltbi  27579  ogrpaddltrbid  27581  ogrpsublt  27582  ogrpinvlt  27584  isarchi3  27601  archirngz  27603  archiabllem1a  27605  archiabllem1  27607  archiabllem2a  27608  archiabllem2c  27609  slmdvs0  27638  gsumvsca1  27643  gsumvsca2  27644  dvrdir  27650  rdivmuldivd  27651  dvrcan5  27653  ornglmullt  27667  isarchiofld  27677  rhmdvd  27681  rhmunitinv  27682  locfinref  27714  metideq  27742  metider  27743  pstmxmet  27746  lmxrge0  27804  qqhghm  27839  qqhrhm  27840  measdivcst  28066  oddpwdc  28163  ballotlemiex  28310  wrdsplex  28365  cvmopnlem  28593  cvmliftmolem2  28597  cvmliftlem6  28605  cvmliftlem8  28607  cvmliftlem9  28608  cvmlift2lem9  28626  cvmlift3lem2  28635  cvmlift3lem6  28639  cvmlift3lem7  28640  cvmlift3lem9  28642  zprod  29041  nodense  29421  cgrtriv  29624  cgrdegen  29626  cgrextend  29630  segconeq  29632  btwntriv2  29634  btwncomand  29637  btwntriv1  29638  btwnintr  29641  btwnexch3  29642  btwnouttr  29646  btwnexch  29647  trisegint  29650  ifscgr  29666  btwnxfr  29678  colineartriv1  29689  colineartriv2  29690  colinearxfr  29697  fscgr  29702  lineid  29705  idinside  29706  endofsegidand  29708  btwnconn1lem5  29713  btwnconn1lem7  29715  btwnconn1lem11  29719  btwnconn1lem12  29720  btwnconn1lem13  29721  brsegle2  29731  segleantisym  29737  broutsideof2  29744  btwnoutside  29747  outsideoftr  29751  outsideofeq  29752  outsideofeu  29753  outsidele  29754  lineunray  29769  lineelsb2  29770  linecom  29772  linethru  29775  heicant  30021  neibastop1  30149  mettrifi  30222  isbnd3  30252  heibor1lem  30277  bfplem2  30291  ghomdiv  30318  zerdivemp1x  30330  irrapxlem5  30734  aomclem2  30973  isnumbasgrplem2  31025  mpaaeu  31072  mendring  31114  mendlmod  31115  caofcan  31201  stoweidlem18  31689  stoweidlem41  31712  stoweidlem45  31716  stoweidlem55  31726  fourierdlem25  31803  fourierdlem31  31809  fourierdlem37  31815  fourierdlem42  31820  ssnn0ssfz  32666  zlmodzxzsub  32677  invginvrid  32688  lmodvsmdi  32705  ply1sclrmsm  32713  lincsum  32760  lincscm  32761  lindslinindimp2lem4  32792  lindslinindsimp2lem5  32793  ldepsprlem  32803  lincresunit3lem1  32810  lincresunit3lem2  32811  isldepslvec2  32816  lfladdcl  34519  lflvscl  34525  eqlkr3  34549  lkrlsp  34550  lshpkrlem4  34561  oldmm1  34665  olj01  34673  latmassOLD  34677  latm32  34679  latmrot  34680  latm4  34681  olm01  34684  cmtcomlemN  34696  cmtbr3N  34702  cmtbr4N  34703  lecmtN  34704  omlfh1N  34706  atlen0  34758  atnle  34765  atlatmstc  34767  atlatle  34768  cvlexchb1  34778  cvlcvr1  34787  ishlat3N  34802  hlatjass  34817  hlatj12  34818  hlatj32  34819  hlsupr2  34834  hlhgt2  34836  hl0lt1N  34837  hlrelat  34849  hlrelat2  34850  exatleN  34851  hlrelat3  34859  cvrval5  34862  cvrexchlem  34866  cvratlem  34868  cvrat  34869  atcvr0eq  34873  lnnat  34874  atlt  34884  atlelt  34885  2atlt  34886  atexchltN  34888  cvrat3  34889  2atjm  34892  atbtwn  34893  4noncolr3  34900  athgt  34903  3dimlem3a  34907  3dimlem3OLDN  34909  3dimlem4a  34910  3dimlem4OLDN  34912  3dim1  34914  3dim2  34915  1cvratex  34920  ps-1  34924  ps-2  34925  hlatexch3N  34927  hlatexch4  34928  ps-2b  34929  3atlem1  34930  3atlem2  34931  3atlem5  34934  3atlem6  34935  llnnleat  34960  llncmp  34969  2at0mat0  34972  2atmat0  34973  2atm  34974  lplni2  34984  lvolex3N  34985  lplnnle2at  34988  lplnnleat  34989  lplnnlelln  34990  2atnelpln  34991  llncvrlpln  35005  2atmat  35008  lplncmp  35009  lplnexllnN  35011  2llnjaN  35013  2llnm4  35017  2llnmeqat  35018  lvolnle3at  35029  lvolnleat  35030  2atnelvolN  35034  islvol2aN  35039  4atlem3  35043  4atlem3a  35044  4atlem3b  35045  4atlem4a  35046  4atlem4b  35047  4atlem4c  35048  4atlem4d  35049  4atlem10  35053  4atlem11b  35055  4atlem11  35056  4atlem12b  35058  4atlem12  35059  4at2  35061  lplncvrlvol  35063  lvolcmp  35064  2lplnja  35066  dalemqrprot  35095  dalemply  35101  dalemsly  35102  dalemrot  35104  dalemrotyz  35105  dalem1  35106  dalemcea  35107  dalem3  35111  dalem5  35114  dalem8  35117  dalem-cly  35118  dalem11  35121  dalem12  35122  dalem16  35126  dalem17  35127  dalem18  35128  dalem21  35141  dalem24  35144  dalem25  35145  dalem38  35157  dalem39  35158  dalem44  35163  dalem54  35173  dalem55  35174  dalem57  35176  dalem58  35177  dalem59  35178  dalem60  35179  dath2  35184  2atm2atN  35232  2llnma1b  35233  2llnma3r  35235  cdlema1N  35238  cdlemblem  35240  paddasslem5  35271  paddasslem10  35276  paddasslem12  35278  paddasslem13  35279  paddass  35285  padd12N  35286  padd4N  35287  paddss  35292  pmodlem1  35293  pmodl42N  35298  pmapjoin  35299  pmapjlln1  35302  atmod1i2  35306  llnmod1i2  35307  llnexchb2  35316  dalawlem2  35319  dalawlem3  35320  dalawlem5  35322  dalawlem6  35323  dalawlem7  35324  dalawlem8  35325  dalawlem11  35328  dalawlem12  35329  dalawlem13  35330  pclunN  35345  osumcllem1N  35403  pexmidlem3N  35419  lhp2lt  35448  lhp0lt  35450  lhpexle2lem  35456  lhpexle3lem  35458  lhpocnle  35463  lhpj1  35469  lhpmcvr4N  35473  lhp2at0  35479  lhpat3  35493  4atexlemtlw  35514  4atexlemc  35516  4atexlemnclw  35517  4atexlemcnd  35519  lautcvr  35539  lautj  35540  lautm  35541  ltrnm  35578  ltrnj  35579  ltrncvr  35580  trlval3  35635  cdlemc5  35643  cdlemd2  35647  cdlemd3  35648  cdleme0e  35665  cdleme1  35675  cdleme3c  35678  cdleme3g  35682  cdleme3h  35683  cdleme3  35685  cdleme5  35688  cdleme7c  35693  cdleme7d  35694  cdleme7e  35695  cdleme7ga  35696  cdleme7  35697  cdleme9  35701  cdleme11c  35709  cdleme11g  35713  cdleme11k  35716  cdleme11  35718  cdleme12  35719  cdleme15b  35723  cdleme15d  35725  cdleme16d  35729  cdleme16e  35730  cdleme16f  35731  cdleme17b  35735  cdleme18b  35740  cdleme22gb  35742  cdlemednpq  35747  cdleme19a  35752  cdleme20aN  35758  cdleme20bN  35759  cdleme20c  35760  cdleme20d  35761  cdleme20j  35767  cdleme21c  35776  cdleme22aa  35788  cdleme22b  35790  cdleme22cN  35791  cdleme22d  35792  cdleme22e  35793  cdleme22eALTN  35794  cdleme23b  35799  cdleme23c  35800  cdleme28a  35819  cdleme30a  35827  cdlemefs29bpre0N  35865  cdlemefs29bpre1N  35866  cdlemefs29cpre1N  35867  cdlemefs29clN  35868  cdlemefs32fvaN  35871  cdlemefs32fva1  35872  cdleme32b  35891  cdleme32c  35892  cdleme32e  35894  cdleme35a  35897  cdleme35fnpq  35898  cdleme35b  35899  cdleme35f  35903  cdleme36a  35909  cdleme36m  35910  cdleme37m  35911  cdleme39a  35914  cdleme42c  35921  cdleme42i  35932  cdleme42keg  35935  cdleme42mgN  35937  cdleme48bw  35951  cdlemeg46fjgN  35970  cdlemeg46fjv  35972  cdlemeg46req  35978  cdleme50trn1  35998  cdlemf1  36010  cdlemf2  36011  cdlemg1cex  36037  cdlemg2fv2  36049  cdlemg7fvbwN  36056  cdlemg4c  36061  cdlemg4  36066  cdlemg6c  36069  cdlemg8b  36077  cdlemg10c  36088  cdlemg10  36090  cdlemg11b  36091  cdlemg12f  36097  cdlemg13a  36100  cdlemg17a  36110  cdlemg17dALTN  36113  cdlemg18b  36128  cdlemg19a  36132  cdlemg27a  36141  cdlemg27b  36145  cdlemg33b0  36150  cdlemg33a  36155  cdlemg35  36162  trlcolem  36175  cdlemg42  36178  cdlemg46  36184  trljco  36189  tendopltp  36229  cdlemh1  36264  cdlemh2  36265  cdlemi1  36267  cdlemi  36269  cdlemk3  36282  cdlemk10  36292  cdlemk11  36298  cdlemk15  36304  cdlemk1u  36308  cdlemk5u  36310  cdlemk11u  36320  cdlemk39  36365  cdlemkid1  36371  cdlemk50  36401  cdlemk51  36402  erngdvlem3-rN  36447  tendocnv  36471  tendospcanN  36473  dialss  36496  dia2dimlem1  36514  dia2dimlem2  36515  dia2dimlem3  36516  dia2dimlem10  36523  dia2dimlem12  36525  dvhvaddass  36547  dvhlveclem  36558  cdlemm10N  36568  doca2N  36576  djajN  36587  dib1dim2  36618  diblss  36620  diclspsn  36644  cdlemn2  36645  cdlemn10  36656  dihjustlem  36666  dihord1  36668  dihord2a  36669  dihord2pre2  36676  dib2dim  36693  dih2dimb  36694  dih2dimbALTN  36695  dihopelvalcpre  36698  dihord5b  36709  dihord6b  36710  dihord5apre  36712  dihmeetlem1N  36740  dihglblem5apreN  36741  dihglblem2N  36744  dihglbcpreN  36750  dihmeetbclemN  36754  dihmeetlem3N  36755  dihmeetlem6  36759  dih1dimatlem  36779  djhcvat42  36865  dihjatcclem1  36868  dihjatcclem4  36871  dvh4dimat  36888  lcfl7lem  36949  lclkrlem2m  36969  lcfrlem1  36992  lcdvsass  37057  baerlem3lem1  37157  baerlem5alem1  37158  baerlem5blem1  37159  mapdh6gN  37192  mapdh6hN  37193  hdmap1l6g  37267  hdmap1l6h  37268  hdmapneg  37299  hdmap14lem8  37328  hgmapadd  37347  hgmapmul  37348  hgmapvvlem1  37376
  Copyright terms: Public domain W3C validator