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

Theorem syl13anc 1266
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 1185 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 665 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  syl23anc  1271  syl33anc  1279  pm2.61da3neOLD  2743  disjxiun  4414  wereu2  4842  ordelord  5455  caovassd  6473  caovcand  6476  caovordid  6480  caovordd  6482  caovdid  6489  caovdird  6492  swoer  7390  swoord1  7391  swoord2  7392  frfi  7813  indexfi  7879  ssfii  7930  elfiun  7941  suplub2  7972  supgtoreq  7983  infltoreq  8009  wemaplem2  8053  htalem  8357  cofsmo  8688  alephsing  8695  sornom  8696  axdc3lem4  8872  zorn2lem1  8915  ttukeylem6  8933  ttukeylem7  8934  prlem934  9447  supfirege  10587  suprfinzcl  11039  fzosubel3  11961  fsuppmapnn0fiublem  12188  seqsplit  12232  seqcaopr  12236  ccatass  12708  wrdcctswrd  12795  wrdeqcats1OLD  12804  wrdeqs1cat  12805  splid  12834  spllen  12835  splfv1  12836  splfv2a  12837  splval2  12838  swrds2  12988  isercolllem2  13696  fsumiun  13848  zprod  13958  lcmftp  14569  pcgcd1  14778  cshwsidrepswmod0  15017  cshwshashlem2  15019  cshwsdisj  15021  firest  15283  iscatd2  15531  posasymb  16142  joinle  16204  meetle  16218  lattrd  16248  latleeqj1  16253  latjlej1  16255  latjlej12  16257  latnlej2  16261  latjidm  16264  latleeqm1  16269  latmlem1  16271  latmlem12  16273  latmidm  16276  latledi  16279  latjass  16285  latj12  16286  latj13  16288  latj31  16289  latjrot  16290  latj4  16291  mod1ile  16295  lubun  16313  clatleglb  16316  latdisdlem  16379  mnd32g  16495  mnd12g  16496  mnd4g  16497  ismndd  16503  prdsmndd  16513  imasmnd  16518  mrcmndind  16557  gsumspl  16572  grpidrcan  16663  grpidlcan  16664  grpinvinv  16665  grplmulf1o  16672  grpinvssd  16675  grpinvadd  16676  grpsubrcan  16679  grpsubadd  16686  grpaddsubass  16688  grppncan  16689  grpsubsub4  16691  grppnpcan2  16692  grpnpncan  16693  grpnpncan0  16694  grpnnncan2  16695  grplactcnv  16698  mulgnn0dir  16725  mulgdirlem  16726  mulgneg2  16729  mulgnnass  16730  mulgnn0ass  16731  mulgass  16732  imasgrp  16746  mhmmnd  16752  nsgconj  16794  isnsg3  16795  nmzsubg  16802  ssnmz  16803  eqger  16811  eqgcpbl  16815  conjghm  16857  conjnmz  16860  conjnmzb  16861  subgga  16898  gass  16899  gasubg  16900  galcan  16902  gacan  16903  gapm  16904  gaorber  16906  gastacl  16907  gastacos  16908  cntzsubm  16933  cntzsubg  16934  oppgmnd  16949  symggen  17055  odmodnn0  17124  mndodconglem  17125  odmod  17130  odcong  17133  odmulgid  17136  odbezout  17140  gexdvdsi  17163  gexdvds  17164  sylow1lem2  17179  sylow1lem4  17181  sylow2blem1  17200  sylow2blem2  17201  sylow2blem3  17202  sylow3lem1  17207  sylow3lem2  17208  lsmass  17248  lsmmod  17253  lsmdisj2  17260  subgdisj1  17269  efgredleme  17321  efgredlemc  17323  efgcpbllemb  17333  frgp0  17338  frgpuplem  17350  abl32  17379  abladdsub4  17384  abladdsub  17385  ablpncan2  17386  ablsubsub  17388  mulgdi  17395  mulgsubdi  17398  odadd1  17414  odadd2  17415  gex2abl  17417  oddvdssubg  17421  cygabl  17453  telgsumfzslem  17546  ablfacrp  17627  pgpfac1lem2  17636  pgpfac1lem3a  17637  pgpfac1lem3  17638  pgpfac1lem4  17639  srgmulgass  17692  srgpcomp  17693  srgpcompp  17694  srgpcomppsc  17695  srgbinomlem3  17703  srgbinomlem4  17704  srgbinomlem  17705  csrgbinom  17707  ringcom  17737  ringlz  17745  ringrz  17746  ringnegl  17750  rngnegr  17751  ringmneg1  17752  ringmneg2  17753  ringsubdi  17755  rngsubdir  17756  mulgass2  17757  prdsringd  17768  imasring  17775  opprring  17787  mulgass3  17793  dvdsrtr  17808  dvdsrmul1  17809  unitgrp  17823  dvrass  17846  dvrcan1  17847  dvrcan3  17848  irredrmul  17863  drngmul0or  17924  subrginv  17952  cntzsubr  17968  lmod0vs  18052  lmodvs0  18053  lmodvsmmulgdi  18054  lmodvneg1  18059  lmodvsneg  18060  lmodcom  18062  lmodsubvs  18072  lmodsubdi  18073  lmodsubdir  18074  lssvsubcl  18095  lssvacl  18105  lssvscl  18106  islss3  18110  lss1d  18114  lssintcl  18115  prdslmodd  18120  lmodvsinv  18187  lmodvsinv2  18188  lmhmplusg  18195  lmhmvsca  18196  lsmcl  18234  pj1lmhm  18251  lvecvs0or  18259  lssvs0or  18261  lvecinv  18264  lspsnvs  18265  lspfixed  18279  lspexch  18280  lspsolvlem  18293  lspsolv  18294  lssacsex  18295  lspsnat  18296  lsppratlem1  18298  lsppratlem3  18300  lsppratlem4  18301  lbsextlem2  18310  lbsextlem4  18312  sralmod  18338  2idlcpbl  18386  unitrrg  18445  assa2ass  18474  issubassa  18476  sraassa  18477  asclghm  18490  asclmul1  18491  asclmul2  18492  asclrhm  18494  assamulgscmlem2  18501  psrbagcon  18523  psrbagconcl  18525  psrbagconf1o  18526  gsumbagdiaglem  18527  psrmulcllem  18539  psrlidm  18555  psrridm  18556  psrass1  18557  psrdi  18558  psrdir  18559  psrass23l  18560  psrcom  18561  mplmon2mul  18652  evlslem1  18666  coe1subfv  18787  lply1binomsc  18829  mulgrhm  18993  cygznlem3  19064  evpmodpmf1o  19088  ipdi  19131  ip2di  19132  ipsubdir  19133  ipsubdi  19134  ip2subdi  19135  ipassr  19137  ipassr2  19138  ip2eq  19144  ocvlss  19159  lsmcss  19179  frlmphl  19263  frlmup1  19280  mamuass  19351  mamudi  19352  mamudir  19353  mamuvs1  19354  mamuvs2  19355  dmatmul  19446  dmatsubcl  19447  scmataddcl  19465  smatvscl  19473  scmatghm  19482  mavmulass  19498  mdetrlin  19551  mdetrsca  19552  mdetralt  19557  mdetunilem7  19567  mdetuni0  19570  matinv  19626  pm2mpghm  19764  chpscmatgsummon  19793  chfacfscmulgsum  19808  chfacfpmmulgsum  19812  chfacfpmmulgsum2  19813  cpmadugsumlemB  19822  cpmadugsumlemC  19823  cpmadugsumlemF  19824  iinopn  19856  subbascn  20194  cnhaus  20294  nrmsep2  20296  nrmsep  20297  regsep2  20316  isreg2  20317  hauscmplem  20345  1stcfb  20384  2ndcctbss  20394  ptbasfi  20520  pthaus  20577  txtube  20579  txhaus  20586  xkohaus  20592  kqnrmlem1  20682  kqnrmlem2  20683  nrmr0reg  20688  nrmhmph  20733  fbssint  20777  infil  20802  fgabs  20818  filcon  20822  filuni  20824  trfil2  20826  trfg  20830  ufprim  20848  elfm3  20889  rnelfm  20892  fmfnfmlem2  20894  fmfnfmlem4  20896  hausflimi  20919  hauspwpwf1  20926  fclsneii  20956  supnfcls  20959  flimfnfcls  20967  fclscmpi  20968  alexsublem  20983  ghmcnp  21053  qustgpopn  21058  psmetsym  21250  psmettri  21251  psmetge0  21252  psmetres2  21254  xmetge0  21283  xmetsym  21286  xmettri  21290  xmetres2  21300  prdsxmetlem  21307  prdsmet  21309  imasdsf1olem  21312  imasf1oxmet  21314  bldisj  21337  xblss2ps  21340  xblss2  21341  xmeter  21372  prdsbl  21430  metustexhalf  21495  metust  21497  nrmmetd  21513  ngpsubcan  21551  nmmtri  21559  nmrtri  21561  ngptgp  21568  nlmvscnlem2  21612  nrginvrcnlem  21617  metdcnlem  21758  clmmulg  22010  cvsmuleqdivd  22028  cvsdiveqd  22029  cphabscl  22049  cphsqrtcl2  22050  cphsqrtcl3  22051  cphnmf  22059  cph2ass  22076  ipcau2  22094  tchcphlem2  22096  ipcnlem2  22101  cfilfcls  22130  iscau3  22134  iscmet3lem2  22148  iscmet3  22149  relcmpcmet  22172  minveclem2  22254  minveclem4  22260  pjthlem1  22265  pjthlem2  22266  uniioombllem4  22418  dyadmax  22430  itg1addlem4  22531  itg1climres  22546  ply1divex  22959  aalioulem2  23151  amgmlem  23777  dvdsppwf1o  23975  perfect1  24016  perfectlem1  24017  perfectlem2  24018  dchrptlem2  24053  colline  24551  ttgcontlem1  24758  axcontlem9  24845  eengtrkg  24858  eengtrkge  24859  4cycl4dv4e  25238  el2spthonot0  25441  usg2spthonot1  25460  clwlknclwlkdifnum  25531  eupa0  25544  eupares  25545  eupap1  25546  frg2woteu  25625  numclwwlk5  25682  numclwwlk6  25683  grpoidinvlem4  25777  grpoasscan2  25808  grpoinvop  25811  grpopncan  25821  grponpcan  25822  grpopnpcan2  25823  grpodiveq  25826  gxcom  25839  gxnn0add  25844  ghgrpOLD  25938  rngo2  25958  rngolz  25971  rngorz  25972  zerdivemp1  26004  vcm  26032  nvmul0or  26115  nvpncan2  26119  nvnncan  26126  nvdif  26136  nvabs  26144  smcnlem  26175  lnomul  26243  minvecolem2  26359  superpos  27839  ssnnssfz  28200  omndmul2  28310  omndmul3  28311  ogrpaddltbi  28317  ogrpaddltrbid  28319  ogrpsublt  28320  ogrpinvlt  28322  isarchi3  28339  archirngz  28341  archiabllem1a  28343  archiabllem1  28345  archiabllem2a  28346  archiabllem2c  28347  slmdvs0  28376  gsumvsca1  28381  gsumvsca2  28382  dvrdir  28389  rdivmuldivd  28390  dvrcan5  28392  ornglmullt  28406  isarchiofld  28416  rhmdvd  28420  rhmunitinv  28421  psgnfzto1stlem  28449  mdetpmtr1  28485  mdetpmtr12  28487  mdetlap  28494  locfinref  28504  metideq  28532  metider  28533  pstmxmet  28536  lmxrge0  28594  qqhghm  28628  qqhrhm  28629  ispisys2  28811  rossros  28838  measdivcst  28883  oddpwdc  29010  ballotlemiex  29157  wrdsplex  29212  cvmopnlem  29786  cvmliftmolem2  29790  cvmliftlem6  29798  cvmliftlem8  29800  cvmliftlem9  29801  cvmlift2lem9  29819  cvmlift3lem2  29828  cvmlift3lem6  29832  cvmlift3lem7  29833  cvmlift3lem9  29835  nodense  30360  cgrtriv  30551  cgrdegen  30553  cgrextend  30557  segconeq  30559  btwntriv2  30561  btwncomand  30564  btwntriv1  30565  btwnintr  30568  btwnexch3  30569  btwnouttr  30573  btwnexch  30574  trisegint  30577  ifscgr  30593  btwnxfr  30605  colineartriv1  30616  colineartriv2  30617  colinearxfr  30624  fscgr  30629  lineid  30632  idinside  30633  endofsegidand  30635  btwnconn1lem5  30640  btwnconn1lem7  30642  btwnconn1lem11  30646  btwnconn1lem12  30647  btwnconn1lem13  30648  brsegle2  30658  segleantisym  30664  broutsideof2  30671  btwnoutside  30674  outsideoftr  30678  outsideofeq  30679  outsideofeu  30680  outsidele  30681  lineunray  30696  lineelsb2  30697  linecom  30699  linethru  30702  neibastop1  30797  poimirlem28  31672  poimirlem32  31676  heicant  31679  mettrifi  31790  isbnd3  31820  heibor1lem  31845  bfplem2  31859  ghomdiv  31886  zerdivemp1x  31898  lfladdcl  32346  lflvscl  32352  eqlkr3  32376  lkrlsp  32377  lshpkrlem4  32388  oldmm1  32492  olj01  32500  latmassOLD  32504  latm32  32506  latmrot  32507  latm4  32508  olm01  32511  cmtcomlemN  32523  cmtbr3N  32529  cmtbr4N  32530  lecmtN  32531  omlfh1N  32533  atlen0  32585  atnle  32592  atlatmstc  32594  atlatle  32595  cvlexchb1  32605  cvlcvr1  32614  ishlat3N  32629  hlatjass  32644  hlatj12  32645  hlatj32  32646  hlsupr2  32661  hlhgt2  32663  hl0lt1N  32664  hlrelat  32676  hlrelat2  32677  exatleN  32678  hlrelat3  32686  cvrval5  32689  cvrexchlem  32693  cvratlem  32695  cvrat  32696  atcvr0eq  32700  lnnat  32701  atlt  32711  atlelt  32712  2atlt  32713  atexchltN  32715  cvrat3  32716  2atjm  32719  atbtwn  32720  4noncolr3  32727  athgt  32730  3dimlem3a  32734  3dimlem3OLDN  32736  3dimlem4a  32737  3dimlem4OLDN  32739  3dim1  32741  3dim2  32742  1cvratex  32747  ps-1  32751  ps-2  32752  hlatexch3N  32754  hlatexch4  32755  ps-2b  32756  3atlem1  32757  3atlem2  32758  3atlem5  32761  3atlem6  32762  llnnleat  32787  llncmp  32796  2at0mat0  32799  2atmat0  32800  2atm  32801  lplni2  32811  lvolex3N  32812  lplnnle2at  32815  lplnnleat  32816  lplnnlelln  32817  2atnelpln  32818  llncvrlpln  32832  2atmat  32835  lplncmp  32836  lplnexllnN  32838  2llnjaN  32840  2llnm4  32844  2llnmeqat  32845  lvolnle3at  32856  lvolnleat  32857  2atnelvolN  32861  islvol2aN  32866  4atlem3  32870  4atlem3a  32871  4atlem3b  32872  4atlem4a  32873  4atlem4b  32874  4atlem4c  32875  4atlem4d  32876  4atlem10  32880  4atlem11b  32882  4atlem11  32883  4atlem12b  32885  4atlem12  32886  4at2  32888  lplncvrlvol  32890  lvolcmp  32891  2lplnja  32893  dalemqrprot  32922  dalemply  32928  dalemsly  32929  dalemrot  32931  dalemrotyz  32932  dalem1  32933  dalemcea  32934  dalem3  32938  dalem5  32941  dalem8  32944  dalem-cly  32945  dalem11  32948  dalem12  32949  dalem16  32953  dalem17  32954  dalem18  32955  dalem21  32968  dalem24  32971  dalem25  32972  dalem38  32984  dalem39  32985  dalem44  32990  dalem54  33000  dalem55  33001  dalem57  33003  dalem58  33004  dalem59  33005  dalem60  33006  dath2  33011  2atm2atN  33059  2llnma1b  33060  2llnma3r  33062  cdlema1N  33065  cdlemblem  33067  paddasslem5  33098  paddasslem10  33103  paddasslem12  33105  paddasslem13  33106  paddass  33112  padd12N  33113  padd4N  33114  paddss  33119  pmodlem1  33120  pmodl42N  33125  pmapjoin  33126  pmapjlln1  33129  atmod1i2  33133  llnmod1i2  33134  llnexchb2  33143  dalawlem2  33146  dalawlem3  33147  dalawlem5  33149  dalawlem6  33150  dalawlem7  33151  dalawlem8  33152  dalawlem11  33155  dalawlem12  33156  dalawlem13  33157  pclunN  33172  osumcllem1N  33230  pexmidlem3N  33246  lhp2lt  33275  lhp0lt  33277  lhpexle2lem  33283  lhpexle3lem  33285  lhpocnle  33290  lhpj1  33296  lhpmcvr4N  33300  lhp2at0  33306  lhpat3  33320  4atexlemtlw  33341  4atexlemc  33343  4atexlemnclw  33344  4atexlemcnd  33346  lautcvr  33366  lautj  33367  lautm  33368  ltrnm  33405  ltrnj  33406  ltrncvr  33407  trlval3  33462  cdlemc5  33470  cdlemd2  33474  cdlemd3  33475  cdleme0e  33492  cdleme1  33502  cdleme3c  33505  cdleme3g  33509  cdleme3h  33510  cdleme3  33512  cdleme5  33515  cdleme7c  33520  cdleme7d  33521  cdleme7e  33522  cdleme7ga  33523  cdleme7  33524  cdleme9  33528  cdleme11c  33536  cdleme11g  33540  cdleme11k  33543  cdleme11  33545  cdleme12  33546  cdleme15b  33550  cdleme15d  33552  cdleme16d  33556  cdleme16e  33557  cdleme16f  33558  cdleme17b  33562  cdleme18b  33567  cdleme22gb  33569  cdlemednpq  33574  cdleme19a  33579  cdleme20aN  33585  cdleme20bN  33586  cdleme20c  33587  cdleme20d  33588  cdleme20j  33594  cdleme21c  33603  cdleme22aa  33615  cdleme22b  33617  cdleme22cN  33618  cdleme22d  33619  cdleme22e  33620  cdleme22eALTN  33621  cdleme23b  33626  cdleme23c  33627  cdleme28a  33646  cdleme30a  33654  cdlemefs29bpre0N  33692  cdlemefs29bpre1N  33693  cdlemefs29cpre1N  33694  cdlemefs29clN  33695  cdlemefs32fvaN  33698  cdlemefs32fva1  33699  cdleme32b  33718  cdleme32c  33719  cdleme32e  33721  cdleme35a  33724  cdleme35fnpq  33725  cdleme35b  33726  cdleme35f  33730  cdleme36a  33736  cdleme36m  33737  cdleme37m  33738  cdleme39a  33741  cdleme42c  33748  cdleme42i  33759  cdleme42keg  33762  cdleme42mgN  33764  cdleme48bw  33778  cdlemeg46fjgN  33797  cdlemeg46fjv  33799  cdlemeg46req  33805  cdleme50trn1  33825  cdlemf1  33837  cdlemf2  33838  cdlemg1cex  33864  cdlemg2fv2  33876  cdlemg7fvbwN  33883  cdlemg4c  33888  cdlemg4  33893  cdlemg6c  33896  cdlemg8b  33904  cdlemg10c  33915  cdlemg10  33917  cdlemg11b  33918  cdlemg12f  33924  cdlemg13a  33927  cdlemg17a  33937  cdlemg17dALTN  33940  cdlemg18b  33955  cdlemg19a  33959  cdlemg27a  33968  cdlemg27b  33972  cdlemg33b0  33977  cdlemg33a  33982  cdlemg35  33989  trlcolem  34002  cdlemg42  34005  cdlemg46  34011  trljco  34016  tendopltp  34056  cdlemh1  34091  cdlemh2  34092  cdlemi1  34094  cdlemi  34096  cdlemk3  34109  cdlemk10  34119  cdlemk11  34125  cdlemk15  34131  cdlemk1u  34135  cdlemk5u  34137  cdlemk11u  34147  cdlemk39  34192  cdlemkid1  34198  cdlemk50  34228  cdlemk51  34229  erngdvlem3-rN  34274  tendocnv  34298  tendospcanN  34300  dialss  34323  dia2dimlem1  34341  dia2dimlem2  34342  dia2dimlem3  34343  dia2dimlem10  34350  dia2dimlem12  34352  dvhvaddass  34374  dvhlveclem  34385  cdlemm10N  34395  doca2N  34403  djajN  34414  dib1dim2  34445  diblss  34447  diclspsn  34471  cdlemn2  34472  cdlemn10  34483  dihjustlem  34493  dihord1  34495  dihord2a  34496  dihord2pre2  34503  dib2dim  34520  dih2dimb  34521  dih2dimbALTN  34522  dihopelvalcpre  34525  dihord5b  34536  dihord6b  34537  dihord5apre  34539  dihmeetlem1N  34567  dihglblem5apreN  34568  dihglblem2N  34571  dihglbcpreN  34577  dihmeetbclemN  34581  dihmeetlem3N  34582  dihmeetlem6  34586  dih1dimatlem  34606  djhcvat42  34692  dihjatcclem1  34695  dihjatcclem4  34698  dvh4dimat  34715  lcfl7lem  34776  lclkrlem2m  34796  lcfrlem1  34819  lcdvsass  34884  baerlem3lem1  34984  baerlem5alem1  34985  baerlem5blem1  34986  mapdh6gN  35019  mapdh6hN  35020  hdmap1l6g  35094  hdmap1l6h  35095  hdmapneg  35126  hdmap14lem8  35155  hgmapadd  35174  hgmapmul  35175  hgmapvvlem1  35203  irrapxlem5  35380  aomclem2  35623  isnumbasgrplem2  35673  mpaaeu  35719  mendring  35761  mendlmod  35762  relexpnul  35913  caofcan  36313  disjiun2  37043  wessf1ornlem  37086  stoweidlem18  37451  stoweidlem41  37475  stoweidlem45  37479  stoweidlem55  37489  fourierdlem25  37567  fourierdlem31  37573  fourierdlem37  37579  fourierdlem42  37584  etransclem48  37718  sge0iunmptlemfi  37793  perfectALTVlem1  38246  perfectALTVlem2  38247  rnglz  38655  ssnn0ssfz  38903  zlmodzxzsub  38914  invginvrid  38925  lmodvsmdi  38940  ply1sclrmsm  38948  lincsum  38995  lincscm  38996  lindslinindimp2lem4  39027  lindslinindsimp2lem5  39028  ldepsprlem  39038  lincresunit3lem1  39045  lincresunit3lem2  39046  isldepslvec2  39051  relogbmulbexp  39146
  Copyright terms: Public domain W3C validator