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

Theorem syl13anc 1278
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 1194 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 671 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  syl23anc  1283  syl33anc  1291  disjxiun  4415  wereu2  4853  ordelord  5468  caovassd  6500  caovcand  6503  caovordid  6507  caovordd  6509  caovdid  6516  caovdird  6519  swoer  7422  swoord1  7423  swoord2  7424  frfi  7847  indexfi  7913  ssfii  7964  elfiun  7975  suplub2  8006  supgtoreq  8017  infltoreq  8049  wemaplem2  8093  htalem  8398  cofsmo  8730  alephsing  8737  sornom  8738  axdc3lem4  8914  zorn2lem1  8957  ttukeylem6  8975  ttukeylem7  8976  prlem934  9489  supfirege  10631  suprfinzcl  11084  fzosubel3  12012  fsuppmapnn0fiublem  12240  seqsplit  12284  seqcaopr  12288  ccatass  12774  wrdcctswrd  12864  wrdeqcats1OLD  12873  wrdeqs1cat  12874  splid  12903  spllen  12904  splfv1  12905  splfv2a  12906  splval2  12907  swrds2  13072  isercolllem2  13784  fsumiun  13936  zprod  14046  lcmftp  14664  pcgcd1  14881  cshwsidrepswmod0  15120  cshwshashlem2  15122  cshwsdisj  15124  firest  15386  iscatd2  15642  posasymb  16253  joinle  16315  meetle  16329  lattrd  16359  latleeqj1  16364  latjlej1  16366  latjlej12  16368  latnlej2  16372  latjidm  16375  latleeqm1  16380  latmlem1  16382  latmlem12  16384  latmidm  16387  latledi  16390  latjass  16396  latj12  16397  latj13  16399  latj31  16400  latjrot  16401  latj4  16402  mod1ile  16406  lubun  16424  clatleglb  16427  latdisdlem  16490  mnd32g  16606  mnd12g  16607  mnd4g  16608  ismndd  16614  prdsmndd  16624  imasmnd  16629  mrcmndind  16668  gsumspl  16683  grpidrcan  16774  grpidlcan  16775  grpinvinv  16776  grplmulf1o  16783  grpinvssd  16786  grpinvadd  16787  grpsubrcan  16790  grpsubadd  16797  grpaddsubass  16799  grppncan  16800  grpsubsub4  16802  grppnpcan2  16803  grpnpncan  16804  grpnpncan0  16805  grpnnncan2  16806  grplactcnv  16809  mulgnn0dir  16836  mulgdirlem  16837  mulgneg2  16840  mulgnnass  16841  mulgnn0ass  16842  mulgass  16843  imasgrp  16857  mhmmnd  16863  nsgconj  16905  isnsg3  16906  nmzsubg  16913  ssnmz  16914  eqger  16922  eqgcpbl  16926  conjghm  16968  conjnmz  16971  conjnmzb  16972  subgga  17009  gass  17010  gasubg  17011  galcan  17013  gacan  17014  gapm  17015  gaorber  17017  gastacl  17018  gastacos  17019  cntzsubm  17044  cntzsubg  17045  oppgmnd  17060  symggen  17166  odmodnn0  17244  mndodconglem  17245  odmod  17250  odcong  17253  odmulgid  17260  odbezout  17264  gexdvdsi  17289  gexdvds  17290  sylow1lem2  17306  sylow1lem4  17308  sylow2blem1  17327  sylow2blem2  17328  sylow2blem3  17329  sylow3lem1  17334  sylow3lem2  17335  lsmass  17375  lsmmod  17380  lsmdisj2  17387  subgdisj1  17396  efgredleme  17448  efgredlemc  17450  efgcpbllemb  17460  frgp0  17465  frgpuplem  17477  abl32  17506  abladdsub4  17511  abladdsub  17512  ablpncan2  17513  ablsubsub  17515  mulgdi  17522  mulgsubdi  17525  odadd1  17541  odadd2  17542  gex2abl  17544  oddvdssubg  17548  cygabl  17580  telgsumfzslem  17673  ablfacrp  17754  pgpfac1lem2  17763  pgpfac1lem3a  17764  pgpfac1lem3  17765  pgpfac1lem4  17766  srgmulgass  17819  srgpcomp  17820  srgpcompp  17821  srgpcomppsc  17822  srgbinomlem3  17830  srgbinomlem4  17831  srgbinomlem  17832  csrgbinom  17834  ringcom  17864  ringlz  17872  ringrz  17873  ringnegl  17877  rngnegr  17878  ringmneg1  17879  ringmneg2  17880  ringsubdi  17882  rngsubdir  17883  mulgass2  17884  prdsringd  17895  imasring  17902  opprring  17914  mulgass3  17920  dvdsrtr  17935  dvdsrmul1  17936  unitgrp  17950  dvrass  17973  dvrcan1  17974  dvrcan3  17975  irredrmul  17990  drngmul0or  18051  subrginv  18079  cntzsubr  18095  lmod0vs  18179  lmodvs0  18180  lmodvsmmulgdi  18181  lmodvneg1  18186  lmodvsneg  18187  lmodcom  18189  lmodsubvs  18199  lmodsubdi  18200  lmodsubdir  18201  lssvsubcl  18222  lssvacl  18232  lssvscl  18233  islss3  18237  lss1d  18241  lssintcl  18242  prdslmodd  18247  lmodvsinv  18314  lmodvsinv2  18315  lmhmplusg  18322  lmhmvsca  18323  lsmcl  18361  pj1lmhm  18378  lvecvs0or  18386  lssvs0or  18388  lvecinv  18391  lspsnvs  18392  lspfixed  18406  lspexch  18407  lspsolvlem  18420  lspsolv  18421  lssacsex  18422  lspsnat  18423  lsppratlem1  18425  lsppratlem3  18427  lsppratlem4  18428  lbsextlem2  18437  lbsextlem4  18439  sralmod  18465  2idlcpbl  18513  unitrrg  18572  assa2ass  18601  issubassa  18603  sraassa  18604  asclghm  18617  asclmul1  18618  asclmul2  18619  asclrhm  18621  assamulgscmlem2  18628  psrbagcon  18650  psrbagconcl  18652  psrbagconf1o  18653  gsumbagdiaglem  18654  psrmulcllem  18666  psrlidm  18682  psrridm  18683  psrass1  18684  psrdi  18685  psrdir  18686  psrass23l  18687  psrcom  18688  mplmon2mul  18779  evlslem1  18793  coe1subfv  18914  lply1binomsc  18956  mulgrhm  19124  cygznlem3  19195  evpmodpmf1o  19219  ipdi  19262  ip2di  19263  ipsubdir  19264  ipsubdi  19265  ip2subdi  19266  ipassr  19268  ipassr2  19269  ip2eq  19275  ocvlss  19290  lsmcss  19310  frlmphl  19394  frlmup1  19411  mamuass  19482  mamudi  19483  mamudir  19484  mamuvs1  19485  mamuvs2  19486  dmatmul  19577  dmatsubcl  19578  scmataddcl  19596  smatvscl  19604  scmatghm  19613  mavmulass  19629  mdetrlin  19682  mdetrsca  19683  mdetralt  19688  mdetunilem7  19698  mdetuni0  19701  matinv  19757  pm2mpghm  19895  chpscmatgsummon  19924  chfacfscmulgsum  19939  chfacfpmmulgsum  19943  chfacfpmmulgsum2  19944  cpmadugsumlemB  19953  cpmadugsumlemC  19954  cpmadugsumlemF  19955  iinopn  19987  subbascn  20325  cnhaus  20425  nrmsep2  20427  nrmsep  20428  regsep2  20447  isreg2  20448  hauscmplem  20476  1stcfb  20515  2ndcctbss  20525  ptbasfi  20651  pthaus  20708  txtube  20710  txhaus  20717  xkohaus  20723  kqnrmlem1  20813  kqnrmlem2  20814  nrmr0reg  20819  nrmhmph  20864  fbssint  20908  infil  20933  fgabs  20949  filcon  20953  filuni  20955  trfil2  20957  trfg  20961  ufprim  20979  elfm3  21020  rnelfm  21023  fmfnfmlem2  21025  fmfnfmlem4  21027  hausflimi  21050  hauspwpwf1  21057  fclsneii  21087  supnfcls  21090  flimfnfcls  21098  fclscmpi  21099  alexsublem  21114  ghmcnp  21184  qustgpopn  21189  psmetsym  21381  psmettri  21382  psmetge0  21383  psmetres2  21385  xmetge0  21414  xmetsym  21417  xmettri  21421  xmetres2  21431  prdsxmetlem  21438  prdsmet  21440  imasdsf1olem  21443  imasf1oxmet  21445  bldisj  21468  xblss2ps  21471  xblss2  21472  xmeter  21503  prdsbl  21561  metustexhalf  21626  metust  21628  nrmmetd  21644  ngpsubcan  21682  nmmtri  21690  nmrtri  21692  ngptgp  21699  nlmvscnlem2  21743  nrginvrcnlem  21748  metdcnlem  21909  clmmulg  22179  cvsmuleqdivd  22197  cvsdiveqd  22198  cphabscl  22218  cphsqrtcl2  22219  cphsqrtcl3  22220  cphnmf  22228  cph2ass  22245  ipcau2  22263  tchcphlem2  22265  ipcnlem2  22270  cfilfcls  22299  iscau3  22303  iscmet3lem2  22317  iscmet3  22318  relcmpcmet  22341  minveclem2  22423  minveclem4  22429  minveclem2OLD  22435  minveclem4OLD  22441  pjthlem1  22446  pjthlem2  22447  uniioombllem4  22600  dyadmax  22612  itg1addlem4  22713  itg1climres  22728  ply1divex  23143  aalioulem2  23345  amgmlem  23971  dvdsppwf1o  24171  perfect1  24212  perfectlem1  24213  perfectlem2  24214  dchrptlem2  24249  colline  24750  ttgcontlem1  24971  axcontlem9  25058  eengtrkg  25071  eengtrkge  25072  4cycl4dv4e  25452  el2spthonot0  25655  usg2spthonot1  25674  clwlknclwlkdifnum  25745  eupa0  25758  eupares  25759  eupap1  25760  frg2woteu  25839  numclwwlk5  25896  numclwwlk6  25897  grpoidinvlem4  25991  grpoasscan2  26022  grpoinvop  26025  grpopncan  26035  grponpcan  26036  grpopnpcan2  26037  grpodiveq  26040  gxcom  26053  gxnn0add  26058  ghgrpOLD  26152  rngo2  26172  rngolz  26185  rngorz  26186  zerdivemp1  26218  vcm  26246  nvmul0or  26329  nvpncan2  26333  nvnncan  26340  nvdif  26350  nvabs  26358  smcnlem  26389  lnomul  26457  minvecolem2  26573  minvecolem2OLD  26583  superpos  28063  ssnnssfz  28419  omndmul2  28526  omndmul3  28527  ogrpaddltbi  28533  ogrpaddltrbid  28535  ogrpsublt  28536  ogrpinvlt  28538  isarchi3  28555  archirngz  28557  archiabllem1a  28559  archiabllem1  28561  archiabllem2a  28562  archiabllem2c  28563  slmdvs0  28592  gsumvsca1  28596  gsumvsca2  28597  dvrdir  28604  rdivmuldivd  28605  dvrcan5  28607  ornglmullt  28621  isarchiofld  28631  rhmdvd  28635  rhmunitinv  28636  psgnfzto1stlem  28664  mdetpmtr1  28700  mdetpmtr12  28702  mdetlap  28709  locfinref  28719  metideq  28747  metider  28748  pstmxmet  28751  lmxrge0  28809  qqhghm  28843  qqhrhm  28844  ispisys2  29026  rossros  29053  measdivcst  29098  oddpwdc  29237  ballotlemiex  29384  ballotlemiexOLD  29422  wrdsplex  29477  cvmopnlem  30051  cvmliftmolem2  30055  cvmliftlem6  30063  cvmliftlem8  30065  cvmliftlem9  30066  cvmlift2lem9  30084  cvmlift3lem2  30093  cvmlift3lem6  30097  cvmlift3lem7  30098  cvmlift3lem9  30100  nodense  30628  cgrtriv  30819  cgrdegen  30821  cgrextend  30825  segconeq  30827  btwntriv2  30829  btwncomand  30832  btwntriv1  30833  btwnintr  30836  btwnexch3  30837  btwnouttr  30841  btwnexch  30842  trisegint  30845  ifscgr  30861  btwnxfr  30873  colineartriv1  30884  colineartriv2  30885  colinearxfr  30892  fscgr  30897  lineid  30900  idinside  30901  endofsegidand  30903  btwnconn1lem5  30908  btwnconn1lem7  30910  btwnconn1lem11  30914  btwnconn1lem12  30915  btwnconn1lem13  30916  brsegle2  30926  segleantisym  30932  broutsideof2  30939  btwnoutside  30942  outsideoftr  30946  outsideofeq  30947  outsideofeu  30948  outsidele  30949  lineunray  30964  lineelsb2  30965  linecom  30967  linethru  30970  neibastop1  31065  poimirlem28  32014  poimirlem32  32018  heicant  32021  mettrifi  32132  isbnd3  32162  heibor1lem  32187  bfplem2  32201  ghomdiv  32228  zerdivemp1x  32240  lfladdcl  32683  lflvscl  32689  eqlkr3  32713  lkrlsp  32714  lshpkrlem4  32725  oldmm1  32829  olj01  32837  latmassOLD  32841  latm32  32843  latmrot  32844  latm4  32845  olm01  32848  cmtcomlemN  32860  cmtbr3N  32866  cmtbr4N  32867  lecmtN  32868  omlfh1N  32870  atlen0  32922  atnle  32929  atlatmstc  32931  atlatle  32932  cvlexchb1  32942  cvlcvr1  32951  ishlat3N  32966  hlatjass  32981  hlatj12  32982  hlatj32  32983  hlsupr2  32998  hlhgt2  33000  hl0lt1N  33001  hlrelat  33013  hlrelat2  33014  exatleN  33015  hlrelat3  33023  cvrval5  33026  cvrexchlem  33030  cvratlem  33032  cvrat  33033  atcvr0eq  33037  lnnat  33038  atlt  33048  atlelt  33049  2atlt  33050  atexchltN  33052  cvrat3  33053  2atjm  33056  atbtwn  33057  4noncolr3  33064  athgt  33067  3dimlem3a  33071  3dimlem3OLDN  33073  3dimlem4a  33074  3dimlem4OLDN  33076  3dim1  33078  3dim2  33079  1cvratex  33084  ps-1  33088  ps-2  33089  hlatexch3N  33091  hlatexch4  33092  ps-2b  33093  3atlem1  33094  3atlem2  33095  3atlem5  33098  3atlem6  33099  llnnleat  33124  llncmp  33133  2at0mat0  33136  2atmat0  33137  2atm  33138  lplni2  33148  lvolex3N  33149  lplnnle2at  33152  lplnnleat  33153  lplnnlelln  33154  2atnelpln  33155  llncvrlpln  33169  2atmat  33172  lplncmp  33173  lplnexllnN  33175  2llnjaN  33177  2llnm4  33181  2llnmeqat  33182  lvolnle3at  33193  lvolnleat  33194  2atnelvolN  33198  islvol2aN  33203  4atlem3  33207  4atlem3a  33208  4atlem3b  33209  4atlem4a  33210  4atlem4b  33211  4atlem4c  33212  4atlem4d  33213  4atlem10  33217  4atlem11b  33219  4atlem11  33220  4atlem12b  33222  4atlem12  33223  4at2  33225  lplncvrlvol  33227  lvolcmp  33228  2lplnja  33230  dalemqrprot  33259  dalemply  33265  dalemsly  33266  dalemrot  33268  dalemrotyz  33269  dalem1  33270  dalemcea  33271  dalem3  33275  dalem5  33278  dalem8  33281  dalem-cly  33282  dalem11  33285  dalem12  33286  dalem16  33290  dalem17  33291  dalem18  33292  dalem21  33305  dalem24  33308  dalem25  33309  dalem38  33321  dalem39  33322  dalem44  33327  dalem54  33337  dalem55  33338  dalem57  33340  dalem58  33341  dalem59  33342  dalem60  33343  dath2  33348  2atm2atN  33396  2llnma1b  33397  2llnma3r  33399  cdlema1N  33402  cdlemblem  33404  paddasslem5  33435  paddasslem10  33440  paddasslem12  33442  paddasslem13  33443  paddass  33449  padd12N  33450  padd4N  33451  paddss  33456  pmodlem1  33457  pmodl42N  33462  pmapjoin  33463  pmapjlln1  33466  atmod1i2  33470  llnmod1i2  33471  llnexchb2  33480  dalawlem2  33483  dalawlem3  33484  dalawlem5  33486  dalawlem6  33487  dalawlem7  33488  dalawlem8  33489  dalawlem11  33492  dalawlem12  33493  dalawlem13  33494  pclunN  33509  osumcllem1N  33567  pexmidlem3N  33583  lhp2lt  33612  lhp0lt  33614  lhpexle2lem  33620  lhpexle3lem  33622  lhpocnle  33627  lhpj1  33633  lhpmcvr4N  33637  lhp2at0  33643  lhpat3  33657  4atexlemtlw  33678  4atexlemc  33680  4atexlemnclw  33681  4atexlemcnd  33683  lautcvr  33703  lautj  33704  lautm  33705  ltrnm  33742  ltrnj  33743  ltrncvr  33744  trlval3  33799  cdlemc5  33807  cdlemd2  33811  cdlemd3  33812  cdleme0e  33829  cdleme1  33839  cdleme3c  33842  cdleme3g  33846  cdleme3h  33847  cdleme3  33849  cdleme5  33852  cdleme7c  33857  cdleme7d  33858  cdleme7e  33859  cdleme7ga  33860  cdleme7  33861  cdleme9  33865  cdleme11c  33873  cdleme11g  33877  cdleme11k  33880  cdleme11  33882  cdleme12  33883  cdleme15b  33887  cdleme15d  33889  cdleme16d  33893  cdleme16e  33894  cdleme16f  33895  cdleme17b  33899  cdleme18b  33904  cdleme22gb  33906  cdlemednpq  33911  cdleme19a  33916  cdleme20aN  33922  cdleme20bN  33923  cdleme20c  33924  cdleme20d  33925  cdleme20j  33931  cdleme21c  33940  cdleme22aa  33952  cdleme22b  33954  cdleme22cN  33955  cdleme22d  33956  cdleme22e  33957  cdleme22eALTN  33958  cdleme23b  33963  cdleme23c  33964  cdleme28a  33983  cdleme30a  33991  cdlemefs29bpre0N  34029  cdlemefs29bpre1N  34030  cdlemefs29cpre1N  34031  cdlemefs29clN  34032  cdlemefs32fvaN  34035  cdlemefs32fva1  34036  cdleme32b  34055  cdleme32c  34056  cdleme32e  34058  cdleme35a  34061  cdleme35fnpq  34062  cdleme35b  34063  cdleme35f  34067  cdleme36a  34073  cdleme36m  34074  cdleme37m  34075  cdleme39a  34078  cdleme42c  34085  cdleme42i  34096  cdleme42keg  34099  cdleme42mgN  34101  cdleme48bw  34115  cdlemeg46fjgN  34134  cdlemeg46fjv  34136  cdlemeg46req  34142  cdleme50trn1  34162  cdlemf1  34174  cdlemf2  34175  cdlemg1cex  34201  cdlemg2fv2  34213  cdlemg7fvbwN  34220  cdlemg4c  34225  cdlemg4  34230  cdlemg6c  34233  cdlemg8b  34241  cdlemg10c  34252  cdlemg10  34254  cdlemg11b  34255  cdlemg12f  34261  cdlemg13a  34264  cdlemg17a  34274  cdlemg17dALTN  34277  cdlemg18b  34292  cdlemg19a  34296  cdlemg27a  34305  cdlemg27b  34309  cdlemg33b0  34314  cdlemg33a  34319  cdlemg35  34326  trlcolem  34339  cdlemg42  34342  cdlemg46  34348  trljco  34353  tendopltp  34393  cdlemh1  34428  cdlemh2  34429  cdlemi1  34431  cdlemi  34433  cdlemk3  34446  cdlemk10  34456  cdlemk11  34462  cdlemk15  34468  cdlemk1u  34472  cdlemk5u  34474  cdlemk11u  34484  cdlemk39  34529  cdlemkid1  34535  cdlemk50  34565  cdlemk51  34566  erngdvlem3-rN  34611  tendocnv  34635  tendospcanN  34637  dialss  34660  dia2dimlem1  34678  dia2dimlem2  34679  dia2dimlem3  34680  dia2dimlem10  34687  dia2dimlem12  34689  dvhvaddass  34711  dvhlveclem  34722  cdlemm10N  34732  doca2N  34740  djajN  34751  dib1dim2  34782  diblss  34784  diclspsn  34808  cdlemn2  34809  cdlemn10  34820  dihjustlem  34830  dihord1  34832  dihord2a  34833  dihord2pre2  34840  dib2dim  34857  dih2dimb  34858  dih2dimbALTN  34859  dihopelvalcpre  34862  dihord5b  34873  dihord6b  34874  dihord5apre  34876  dihmeetlem1N  34904  dihglblem5apreN  34905  dihglblem2N  34908  dihglbcpreN  34914  dihmeetbclemN  34918  dihmeetlem3N  34919  dihmeetlem6  34923  dih1dimatlem  34943  djhcvat42  35029  dihjatcclem1  35032  dihjatcclem4  35035  dvh4dimat  35052  lcfl7lem  35113  lclkrlem2m  35133  lcfrlem1  35156  lcdvsass  35221  baerlem3lem1  35321  baerlem5alem1  35322  baerlem5blem1  35323  mapdh6gN  35356  mapdh6hN  35357  hdmap1l6g  35431  hdmap1l6h  35432  hdmapneg  35463  hdmap14lem8  35492  hgmapadd  35511  hgmapmul  35512  hgmapvvlem1  35540  irrapxlem5  35716  aomclem2  35959  isnumbasgrplem2  36009  mpaaeu  36062  mendring  36104  mendlmod  36105  relexpnul  36316  caofcan  36717  disjiun2  37437  wessf1ornlem  37513  stoweidlem18  37979  stoweidlem41  38003  stoweidlem45  38007  stoweidlem55  38017  fourierdlem25  38095  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem37  38108  fourierdlem42  38113  fourierdlem42OLD  38114  etransclem48OLD  38248  etransclem48  38249  issalgend  38298  sge0iunmptlemfi  38358  hoicvr  38477  hoidmvlelem2  38525  perfectALTVlem1  38978  perfectALTVlem2  38979  nbfusgrlevtxm2  39598  nbusgrvtxm1  39599  rnglz  40253  ssnn0ssfz  40499  zlmodzxzsub  40510  invginvrid  40521  lmodvsmdi  40536  ply1sclrmsm  40544  lincsum  40591  lincscm  40592  lindslinindimp2lem4  40623  lindslinindsimp2lem5  40624  ldepsprlem  40634  lincresunit3lem1  40641  lincresunit3lem2  40642  isldepslvec2  40647  relogbmulbexp  40741
  Copyright terms: Public domain W3C validator