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

Theorem syl13anc 1220
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  1225  syl33anc  1233  pm2.61da3ne  2686  disjxiun  4284  wereu2  4712  ordelord  4736  caovassd  6257  caovcand  6260  caovordid  6264  caovordd  6266  caovdid  6273  caovdird  6276  swoer  7121  swoord1  7122  swoord2  7123  frfi  7549  indexfi  7611  ssfii  7661  elfiun  7672  suplub2  7703  wemaplem2  7753  htalem  8095  cofsmo  8430  alephsing  8437  sornom  8438  axdc3lem4  8614  zorn2lem1  8657  ttukeylem6  8675  ttukeylem7  8676  prlem934  9194  fzosubel3  11593  seqsplit  11831  seqcaopr  11835  ccatass  12278  wrdcctswrd  12351  wrdeqcats1  12360  wrdeqs1cat  12361  splid  12387  spllen  12388  splfv1  12389  splfv2a  12390  splval2  12391  swrds2  12537  isercolllem2  13135  fsumiun  13276  pcgcd1  13935  cshwsidrepswmod0  14113  cshwshashlem2  14115  cshwsdisj  14117  firest  14363  iscatd2  14611  posasymb  15114  joinle  15176  meetle  15190  lattrd  15220  latleeqj1  15225  latjlej1  15227  latjlej12  15229  latnlej2  15233  latjidm  15236  latleeqm1  15241  latmlem1  15243  latmlem12  15245  latmidm  15248  latledi  15251  latjass  15257  latj12  15258  latj13  15260  latj31  15261  latjrot  15262  latj4  15263  mod1ile  15267  lubun  15285  clatleglb  15288  latdisdlem  15351  mnd32g  15416  mnd12g  15417  mnd4g  15418  prdsmndd  15446  imasmnd  15451  mrcmndind  15485  gsumspl  15513  grpidrcan  15582  grpidlcan  15583  grpinvinv  15584  grplmulf1o  15591  grpinvssd  15594  grpinvadd  15595  grpsubrcan  15598  grpsubadd  15604  grpaddsubass  15606  grppncan  15607  grpsubsub4  15609  grppnpcan2  15610  grpnpncan  15611  grpnnncan2  15612  grplactcnv  15615  mulgnn0dir  15641  mulgdirlem  15642  mulgneg2  15645  mulgnnass  15646  mulgnn0ass  15647  mulgass  15648  imasgrp  15662  nsgconj  15705  isnsg3  15706  nmzsubg  15713  ssnmz  15714  eqger  15722  eqgcpbl  15726  conjghm  15768  conjnmz  15771  conjnmzb  15772  subgga  15809  gass  15810  gasubg  15811  galcan  15813  gacan  15814  gapm  15815  gaorber  15817  gastacl  15818  gastacos  15819  cntzsubm  15844  cntzsubg  15845  oppgmnd  15860  symggen  15967  odmodnn0  16034  mndodconglem  16035  odmod  16040  odcong  16043  odmulgid  16046  odbezout  16050  gexdvdsi  16073  gexdvds  16074  sylow1lem2  16089  sylow1lem4  16091  sylow2blem1  16110  sylow2blem2  16111  sylow2blem3  16112  sylow3lem1  16117  sylow3lem2  16118  lsmass  16158  lsmmod  16163  lsmdisj2  16170  subgdisj1  16179  efgredleme  16231  efgredlemc  16233  efgcpbllemb  16243  frgp0  16248  frgpuplem  16260  abl32  16289  abladdsub4  16294  abladdsub  16295  ablpncan2  16296  ablsubsub  16298  mulgdi  16305  mulgsubdi  16308  odadd1  16321  odadd2  16322  gex2abl  16324  oddvdssubg  16328  cygabl  16358  ablfacrp  16557  pgpfac1lem2  16566  pgpfac1lem3a  16567  pgpfac1lem3  16568  pgpfac1lem4  16569  srgmulgass  16620  srgpcomp  16621  srgpcompp  16622  srgpcomppsc  16623  srgbinomlem3  16630  srgbinomlem4  16631  srgbinomlem  16632  csrgbinom  16634  rngcom  16663  rnglz  16671  rngrz  16672  rngnegl  16675  rngnegr  16676  rngmneg1  16677  rngmneg2  16678  rngsubdi  16680  rngsubdir  16681  mulgass2  16682  prdsrngd  16694  imasrng  16701  opprrng  16713  mulgass3  16719  dvdsrtr  16734  dvdsrmul1  16735  unitgrp  16749  dvrass  16772  dvrcan1  16773  dvrcan3  16774  irredrmul  16789  drngmul0or  16833  subrginv  16861  cntzsubr  16877  lmod0vs  16961  lmodvs0  16962  lmodvneg1  16968  lmodvsneg  16969  lmodcom  16971  lmodsubvs  16981  lmodsubdi  16982  lmodsubdir  16983  lssvsubcl  17005  lssvacl  17015  lssvscl  17016  islss3  17020  lss1d  17024  lssintcl  17025  prdslmodd  17030  lmodvsinv  17097  lmodvsinv2  17098  lmhmplusg  17105  lmhmvsca  17106  lsmcl  17144  pj1lmhm  17161  lvecvs0or  17169  lssvs0or  17171  lvecinv  17174  lspsnvs  17175  lspfixed  17189  lspexch  17190  lspsolvlem  17203  lspsolv  17204  lssacsex  17205  lspsnat  17206  lsppratlem1  17208  lsppratlem3  17210  lsppratlem4  17211  lbsextlem2  17220  lbsextlem4  17222  sralmod  17248  2idlcpbl  17296  unitrrg  17345  issubassa  17375  sraassa  17376  asclghm  17389  asclmul1  17390  asclmul2  17391  asclrhm  17392  psrbagcon  17420  psrbagconcl  17423  psrbagconf1o  17424  gsumbagdiaglem  17425  psrmulcllem  17438  psrlidm  17454  psrlidmOLD  17455  psrridm  17456  psrridmOLD  17457  psrass1  17458  psrdi  17459  psrdir  17460  psrcom  17461  psrass23  17462  mplmon2mul  17563  evlslem1  17581  coe1subfv  17700  mulgrhm  17906  mulgrhmOLD  17909  cygznlem3  17982  evpmodpmf1o  18006  ipdi  18049  ip2di  18050  ipsubdir  18051  ipsubdi  18052  ip2subdi  18053  ipassr  18055  ipassr2  18056  ip2eq  18062  ocvlss  18077  lsmcss  18097  frlmphl  18186  frlmup1  18206  mamuass  18286  mamudi  18287  mamudir  18288  mamuvs1  18289  mamuvs2  18290  mavmulass  18340  mdetrlin  18389  mdetrsca  18390  mdetralt  18394  mdetunilem7  18404  mdetuni0  18407  matinv  18463  iinopn  18495  subbascn  18838  cnhaus  18938  nrmsep2  18940  nrmsep  18941  regsep2  18960  isreg2  18961  hauscmplem  18989  1stcfb  19029  2ndcctbss  19039  ptbasfi  19134  pthaus  19191  txtube  19193  txhaus  19200  xkohaus  19206  kqnrmlem1  19296  kqnrmlem2  19297  nrmr0reg  19302  nrmhmph  19347  fbssint  19391  infil  19416  fgabs  19432  filcon  19436  filuni  19438  trfil2  19440  trfg  19444  ufprim  19462  elfm3  19503  rnelfm  19506  fmfnfmlem2  19508  fmfnfmlem4  19510  hausflimi  19533  hauspwpwf1  19540  fclsneii  19570  supnfcls  19573  flimfnfcls  19581  fclscmpi  19582  alexsublem  19596  ghmcnp  19665  divstgpopn  19670  psmetsym  19866  psmettri  19867  psmetge0  19868  psmetres2  19870  xmetge0  19899  xmetsym  19902  xmettri  19906  xmetres2  19916  prdsxmetlem  19923  prdsmet  19925  imasdsf1olem  19928  imasf1oxmet  19930  bldisj  19953  xblss2ps  19956  xblss2  19957  xmeter  19988  prdsbl  20046  metustexhalfOLD  20118  metustexhalf  20119  metustOLD  20122  metust  20123  nrmmetd  20147  ngpsubcan  20185  nmmtri  20193  nmrtri  20195  ngptgp  20202  nlmvscnlem2  20246  nrginvrcnlem  20251  metdcnlem  20393  clmmulg  20645  cvsmuleqdivd  20663  cvsdiveqd  20664  cphabscl  20684  cphsqrcl2  20685  cphsqrcl3  20686  cphnmf  20694  cph2ass  20711  ipcau2  20729  tchcphlem2  20731  ipcnlem2  20736  cfilfcls  20765  iscau3  20769  iscmet3lem2  20783  iscmet3  20784  relcmpcmet  20807  minveclem2  20893  minveclem4  20899  pjthlem1  20904  pjthlem2  20905  uniioombllem4  21046  dyadmax  21058  itg1addlem4  21157  itg1climres  21172  ply1divex  21588  aalioulem2  21779  amgmlem  22363  dvdsppwf1o  22506  perfect1  22547  perfectlem1  22548  perfectlem2  22549  dchrptlem2  22584  colline  23032  ttgcontlem1  23099  axcontlem9  23186  eengtrkg  23199  eengtrkge  23200  4cycl4dv4e  23522  eupa0  23563  eupares  23564  eupap1  23565  grpoidinvlem4  23662  grpoasscan2  23693  grpoinvop  23696  grpopncan  23706  grponpcan  23707  grpopnpcan2  23708  grpodiveq  23711  gxcom  23724  gxnn0add  23729  ghgrp  23823  rngo2  23843  rngolz  23856  rngorz  23857  zerdivemp1  23889  vcm  23917  nvmul0or  24000  nvpncan2  24004  nvnncan  24011  nvdif  24021  nvabs  24029  smcnlem  24060  lnomul  24128  minvecolem2  24244  superpos  25726  ssnnssfz  26044  omndmul2  26143  omndmul3  26144  ogrpaddltbi  26150  ogrpaddltrbid  26152  ogrpsublt  26153  ogrpinvlt  26155  isarchi3  26172  archirngz  26174  archiabllem1a  26176  archiabllem1  26178  archiabllem2a  26179  archiabllem2c  26180  slmdvs0  26209  gsumvsca1  26219  gsumvsca2  26220  dvrdir  26226  rdivmuldivd  26227  dvrcan5  26229  ornglmullt  26243  isarchiofld  26253  rhmdvd  26257  rhmunitinv  26258  metideq  26289  metider  26290  pstmxmet  26293  lmxrge0  26351  qqhghm  26386  qqhrhm  26387  oddpwdc  26706  ballotlemiex  26853  wrdsplex  26908  cvmopnlem  27136  cvmliftmolem2  27140  cvmliftlem6  27148  cvmliftlem8  27150  cvmliftlem9  27151  cvmlift2lem9  27169  cvmlift3lem2  27178  cvmlift3lem6  27182  cvmlift3lem7  27183  cvmlift3lem9  27185  zprod  27419  nodense  27799  cgrtriv  28002  cgrdegen  28004  cgrextend  28008  segconeq  28010  btwntriv2  28012  btwncomand  28015  btwntriv1  28016  btwnintr  28019  btwnexch3  28020  btwnouttr  28024  btwnexch  28025  trisegint  28028  ifscgr  28044  btwnxfr  28056  colineartriv1  28067  colineartriv2  28068  colinearxfr  28075  fscgr  28080  lineid  28083  idinside  28084  endofsegidand  28086  btwnconn1lem5  28091  btwnconn1lem7  28093  btwnconn1lem11  28097  btwnconn1lem12  28098  btwnconn1lem13  28099  brsegle2  28109  segleantisym  28115  broutsideof2  28122  btwnoutside  28125  outsideoftr  28129  outsideofeq  28130  outsideofeu  28131  outsidele  28132  lineunray  28147  lineelsb2  28148  linecom  28150  linethru  28153  heicant  28397  neibastop1  28551  mettrifi  28624  isbnd3  28654  heibor1lem  28679  bfplem2  28693  ghomdiv  28720  zerdivemp1x  28732  irrapxlem5  29138  aomclem2  29379  isnumbasgrplem2  29431  mpaaeu  29478  mendrng  29520  mendlmod  29521  caofcan  29568  stoweidlem18  29784  stoweidlem41  29807  stoweidlem45  29811  stoweidlem55  29821  el2spthonot0  30361  usg2spthonot1  30380  clwlknclwlkdifnum  30550  frg2woteu  30619  numclwwlk5  30676  numclwwlk6  30677  ssnn0ssfz  30711  supgtoreq  30712  supfirege  30713  suprfinzcl  30714  zlmodzxzsub  30726  invginvrid  30741  fsuppmapnn0fiublem  30767  lmodvsmdi  30778  lmodvsmmulgdi  30779  assa2ass  30785  assamulgscmlem2  30787  psrass23l  30790  ply1sclrmsm  30795  lply1binomsc  30812  dmatmul  30836  dmatsubcl  30837  lincsum  30894  lincscm  30895  lindslinindimp2lem4  30926  lindslinindsimp2lem5  30927  ldepsprlem  30937  lincresunit3lem1  30944  lincresunit3lem2  30945  isldepslvec2  30950  lfladdcl  32609  lflvscl  32615  eqlkr3  32639  lkrlsp  32640  lshpkrlem4  32651  oldmm1  32755  olj01  32763  latmassOLD  32767  latm32  32769  latmrot  32770  latm4  32771  olm01  32774  cmtcomlemN  32786  cmtbr3N  32792  cmtbr4N  32793  lecmtN  32794  omlfh1N  32796  atlen0  32848  atnle  32855  atlatmstc  32857  atlatle  32858  cvlexchb1  32868  cvlcvr1  32877  ishlat3N  32892  hlatjass  32907  hlatj12  32908  hlatj32  32909  hlsupr2  32924  hlhgt2  32926  hl0lt1N  32927  hlrelat  32939  hlrelat2  32940  exatleN  32941  hlrelat3  32949  cvrval5  32952  cvrexchlem  32956  cvratlem  32958  cvrat  32959  atcvr0eq  32963  lnnat  32964  atlt  32974  atlelt  32975  2atlt  32976  atexchltN  32978  cvrat3  32979  2atjm  32982  atbtwn  32983  4noncolr3  32990  athgt  32993  3dimlem3a  32997  3dimlem3OLDN  32999  3dimlem4a  33000  3dimlem4OLDN  33002  3dim1  33004  3dim2  33005  1cvratex  33010  ps-1  33014  ps-2  33015  hlatexch3N  33017  hlatexch4  33018  ps-2b  33019  3atlem1  33020  3atlem2  33021  3atlem5  33024  3atlem6  33025  llnnleat  33050  llncmp  33059  2at0mat0  33062  2atmat0  33063  2atm  33064  lplni2  33074  lvolex3N  33075  lplnnle2at  33078  lplnnleat  33079  lplnnlelln  33080  2atnelpln  33081  llncvrlpln  33095  2atmat  33098  lplncmp  33099  lplnexllnN  33101  2llnjaN  33103  2llnm4  33107  2llnmeqat  33108  lvolnle3at  33119  lvolnleat  33120  2atnelvolN  33124  islvol2aN  33129  4atlem3  33133  4atlem3a  33134  4atlem3b  33135  4atlem4a  33136  4atlem4b  33137  4atlem4c  33138  4atlem4d  33139  4atlem10  33143  4atlem11b  33145  4atlem11  33146  4atlem12b  33148  4atlem12  33149  4at2  33151  lplncvrlvol  33153  lvolcmp  33154  2lplnja  33156  dalemqrprot  33185  dalemply  33191  dalemsly  33192  dalemrot  33194  dalemrotyz  33195  dalem1  33196  dalemcea  33197  dalem3  33201  dalem5  33204  dalem8  33207  dalem-cly  33208  dalem11  33211  dalem12  33212  dalem16  33216  dalem17  33217  dalem18  33218  dalem21  33231  dalem24  33234  dalem25  33235  dalem38  33247  dalem39  33248  dalem44  33253  dalem54  33263  dalem55  33264  dalem57  33266  dalem58  33267  dalem59  33268  dalem60  33269  dath2  33274  2atm2atN  33322  2llnma1b  33323  2llnma3r  33325  cdlema1N  33328  cdlemblem  33330  paddasslem5  33361  paddasslem10  33366  paddasslem12  33368  paddasslem13  33369  paddass  33375  padd12N  33376  padd4N  33377  paddss  33382  pmodlem1  33383  pmodl42N  33388  pmapjoin  33389  pmapjlln1  33392  atmod1i2  33396  llnmod1i2  33397  llnexchb2  33406  dalawlem2  33409  dalawlem3  33410  dalawlem5  33412  dalawlem6  33413  dalawlem7  33414  dalawlem8  33415  dalawlem11  33418  dalawlem12  33419  dalawlem13  33420  pclunN  33435  osumcllem1N  33493  pexmidlem3N  33509  lhp2lt  33538  lhp0lt  33540  lhpexle2lem  33546  lhpexle3lem  33548  lhpocnle  33553  lhpj1  33559  lhpmcvr4N  33563  lhp2at0  33569  lhpat3  33583  4atexlemtlw  33604  4atexlemc  33606  4atexlemnclw  33607  4atexlemcnd  33609  lautcvr  33629  lautj  33630  lautm  33631  ltrnm  33668  ltrnj  33669  ltrncvr  33670  trlval3  33724  cdlemc5  33732  cdlemd2  33736  cdlemd3  33737  cdleme0e  33754  cdleme1  33764  cdleme3c  33767  cdleme3g  33771  cdleme3h  33772  cdleme3  33774  cdleme5  33777  cdleme7c  33782  cdleme7d  33783  cdleme7e  33784  cdleme7ga  33785  cdleme7  33786  cdleme9  33790  cdleme11c  33798  cdleme11g  33802  cdleme11k  33805  cdleme11  33807  cdleme12  33808  cdleme15b  33812  cdleme15d  33814  cdleme16d  33818  cdleme16e  33819  cdleme16f  33820  cdleme17b  33824  cdleme18b  33829  cdleme22gb  33831  cdlemednpq  33836  cdleme19a  33840  cdleme20aN  33846  cdleme20bN  33847  cdleme20c  33848  cdleme20d  33849  cdleme20j  33855  cdleme21c  33864  cdleme22aa  33876  cdleme22b  33878  cdleme22cN  33879  cdleme22d  33880  cdleme22e  33881  cdleme22eALTN  33882  cdleme23b  33887  cdleme23c  33888  cdleme28a  33907  cdleme30a  33915  cdlemefs29bpre0N  33953  cdlemefs29bpre1N  33954  cdlemefs29cpre1N  33955  cdlemefs29clN  33956  cdlemefs32fvaN  33959  cdlemefs32fva1  33960  cdleme32b  33979  cdleme32c  33980  cdleme32e  33982  cdleme35a  33985  cdleme35fnpq  33986  cdleme35b  33987  cdleme35f  33991  cdleme36a  33997  cdleme36m  33998  cdleme37m  33999  cdleme39a  34002  cdleme42c  34009  cdleme42i  34020  cdleme42keg  34023  cdleme42mgN  34025  cdleme48bw  34039  cdlemeg46fjgN  34058  cdlemeg46fjv  34060  cdlemeg46req  34066  cdleme50trn1  34086  cdlemf1  34098  cdlemf2  34099  cdlemg1cex  34125  cdlemg2fv2  34137  cdlemg7fvbwN  34144  cdlemg4c  34149  cdlemg4  34154  cdlemg6c  34157  cdlemg8b  34165  cdlemg10c  34176  cdlemg10  34178  cdlemg11b  34179  cdlemg12f  34185  cdlemg13a  34188  cdlemg17a  34198  cdlemg17dALTN  34201  cdlemg18b  34216  cdlemg19a  34220  cdlemg27a  34229  cdlemg27b  34233  cdlemg33b0  34238  cdlemg33a  34243  cdlemg35  34250  trlcolem  34263  cdlemg42  34266  cdlemg46  34272  trljco  34277  tendopltp  34317  cdlemh1  34352  cdlemh2  34353  cdlemi1  34355  cdlemi  34357  cdlemk3  34370  cdlemk10  34380  cdlemk11  34386  cdlemk15  34392  cdlemk1u  34396  cdlemk5u  34398  cdlemk11u  34408  cdlemk39  34453  cdlemkid1  34459  cdlemk50  34489  cdlemk51  34490  erngdvlem3-rN  34535  tendocnv  34559  tendospcanN  34561  dialss  34584  dia2dimlem1  34602  dia2dimlem2  34603  dia2dimlem3  34604  dia2dimlem10  34611  dia2dimlem12  34613  dvhvaddass  34635  dvhlveclem  34646  cdlemm10N  34656  doca2N  34664  djajN  34675  dib1dim2  34706  diblss  34708  diclspsn  34732  cdlemn2  34733  cdlemn10  34744  dihjustlem  34754  dihord1  34756  dihord2a  34757  dihord2pre2  34764  dib2dim  34781  dih2dimb  34782  dih2dimbALTN  34783  dihopelvalcpre  34786  dihord5b  34797  dihord6b  34798  dihord5apre  34800  dihmeetlem1N  34828  dihglblem5apreN  34829  dihglblem2N  34832  dihglbcpreN  34838  dihmeetbclemN  34842  dihmeetlem3N  34843  dihmeetlem6  34847  dih1dimatlem  34867  djhcvat42  34953  dihjatcclem1  34956  dihjatcclem4  34959  dvh4dimat  34976  lcfl7lem  35037  lclkrlem2m  35057  lcfrlem1  35080  lcdvsass  35145  baerlem3lem1  35245  baerlem5alem1  35246  baerlem5blem1  35247  mapdh6gN  35280  mapdh6hN  35281  hdmap1l6g  35355  hdmap1l6h  35356  hdmapneg  35387  hdmap14lem8  35416  hgmapadd  35435  hgmapmul  35436  hgmapvvlem1  35464
  Copyright terms: Public domain W3C validator