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

Theorem syl13anc 1187
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 1135 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 644 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  syl23anc  1192  syl33anc  1200  pm2.61da3ne  2686  disjxiun  4211  wereu2  4581  ordelord  4605  caovassd  6248  caovcand  6251  caovordid  6255  caovordd  6257  caovdid  6264  caovdird  6267  swoer  6935  swoord1  6936  swoord2  6937  frfi  7354  indexfi  7416  ssfii  7426  elfiun  7437  suplub2  7468  wemaplem2  7518  htalem  7822  cofsmo  8151  alephsing  8158  sornom  8159  axdc3lem4  8335  zorn2lem1  8378  ttukeylem6  8396  ttukeylem7  8397  prlem934  8912  fzosubel3  11181  seqsplit  11358  seqcaopr  11362  ccatass  11752  splid  11784  spllen  11785  splfv1  11786  splfv2a  11787  splval2  11788  wrdeqcats1  11790  wrdeqs1cat  11791  swrds2  11882  isercolllem2  12461  fsumiun  12602  pcgcd1  13252  firest  13662  iscatd2  13908  posasymb  14411  meetle  14459  lattrd  14489  latleeqj1  14494  latjlej1  14496  latjlej12  14498  latnlej2  14502  latjidm  14505  latleeqm1  14510  latmlem1  14512  latmlem12  14514  latmidm  14517  latledi  14520  latjass  14526  latj12  14527  latj13  14529  latj31  14530  latjrot  14531  latj4  14532  mod1ile  14536  lubun  14552  clatleglb  14555  latdisdlem  14617  mnd32g  14701  mnd12g  14702  mnd4g  14703  prdsmndd  14730  imasmnd  14735  gsumspl  14791  grpinvinv  14860  grplmulf1o  14867  grpinvadd  14869  grpsubrcan  14872  grpsubadd  14878  grpaddsubass  14880  grppncan  14881  grpsubsub4  14883  grppnpcan2  14884  grpnpncan  14885  grpnnncan2  14886  grplactcnv  14889  mulgnn0dir  14915  mulgdirlem  14916  mulgneg2  14919  mulgnnass  14920  mulgnn0ass  14921  mulgass  14922  imasgrp  14936  nsgconj  14975  isnsg3  14976  nmzsubg  14983  ssnmz  14984  eqger  14992  eqgcpbl  14996  conjghm  15038  conjnmz  15041  conjnmzb  15042  subgga  15079  gass  15080  gasubg  15081  galcan  15083  gacan  15084  gapm  15085  gaorber  15087  gastacl  15088  gastacos  15089  cntzsubm  15136  cntzsubg  15137  oppgmnd  15152  odmodnn0  15180  mndodconglem  15181  odmod  15186  odcong  15189  odmulgid  15192  odbezout  15196  gexdvdsi  15219  gexdvds  15220  sylow1lem2  15235  sylow1lem4  15237  sylow2blem1  15256  sylow2blem2  15257  sylow2blem3  15258  sylow3lem1  15263  sylow3lem2  15264  lsmass  15304  lsmmod  15309  lsmdisj2  15316  subgdisj1  15325  efgredleme  15377  efgredlemc  15379  efgcpbllemb  15389  frgp0  15394  frgpuplem  15406  abl32  15435  abladdsub4  15440  abladdsub  15441  ablpncan2  15442  ablsubsub  15444  mulgdi  15451  mulgsubdi  15454  odadd1  15465  odadd2  15466  gex2abl  15468  oddvdssubg  15472  cygabl  15502  ablfacrp  15626  pgpfac1lem2  15635  pgpfac1lem3a  15636  pgpfac1lem3  15637  pgpfac1lem4  15638  rngcom  15694  rnglz  15702  rngrz  15703  rngnegl  15705  rngnegr  15706  rngmneg1  15707  rngmneg2  15708  rngsubdi  15710  rngsubdir  15711  mulgass2  15712  prdsrngd  15720  imasrng  15727  opprrng  15738  mulgass3  15744  dvdsrtr  15759  dvdsrmul1  15760  unitgrp  15774  dvrass  15797  dvrcan1  15798  dvrcan3  15799  irredrmul  15814  drngmul0or  15858  subrginv  15886  cntzsubr  15902  lmod0vs  15985  lmodvs0  15986  lmodvneg1  15989  lmodvsneg  15990  lmodcom  15992  lmodsubvs  16002  lmodsubdi  16003  lmodsubdir  16004  lssvsubcl  16022  lssvacl  16032  lssvscl  16033  islss3  16037  lss1d  16041  lssintcl  16042  prdslmodd  16047  lmodvsinv  16114  lmodvsinv2  16115  lmhmplusg  16122  lmhmvsca  16123  lsmcl  16157  pj1lmhm  16174  lvecvs0or  16182  lssvs0or  16184  lvecinv  16187  lspsnvs  16188  lspfixed  16202  lspexch  16203  lspsolvlem  16216  lspsolv  16217  lssacsex  16218  lspsnat  16219  lsppratlem1  16221  lsppratlem3  16223  lsppratlem4  16224  lbsextlem2  16233  lbsextlem4  16235  sralmod  16260  2idlcpbl  16307  unitrrg  16355  issubassa  16385  sraassa  16386  asclghm  16399  asclmul1  16400  asclmul2  16401  asclrhm  16402  psrbagcon  16438  psrbagconcl  16440  psrbagconf1o  16441  gsumbagdiaglem  16442  psrmulcllem  16453  psrlidm  16469  psrridm  16470  psrass1  16471  psrdi  16472  psrdir  16473  psrcom  16474  psrass23  16475  mplmon2mul  16563  coe1subfv  16661  mulgrhm  16789  cygznlem3  16852  ipdi  16873  ip2di  16874  ipsubdir  16875  ipsubdi  16876  ip2subdi  16877  ipassr  16879  ipassr2  16880  ip2eq  16886  ocvlss  16901  lsmcss  16921  iinopn  16977  subbascn  17320  cnhaus  17420  nrmsep2  17422  nrmsep  17423  regsep2  17442  isreg2  17443  hauscmplem  17471  1stcfb  17510  2ndcctbss  17520  ptbasfi  17615  pthaus  17672  txtube  17674  txhaus  17681  xkohaus  17687  kqnrmlem1  17777  kqnrmlem2  17778  nrmr0reg  17783  nrmhmph  17828  fbssint  17872  infil  17897  fgabs  17913  filcon  17917  filuni  17919  trfil2  17921  trfg  17925  ufprim  17943  elfm3  17984  rnelfm  17987  fmfnfmlem2  17989  fmfnfmlem4  17991  hausflimi  18014  hauspwpwf1  18021  fclsneii  18051  supnfcls  18054  flimfnfcls  18062  fclscmpi  18063  alexsublem  18077  ghmcnp  18146  divstgpopn  18151  psmetsym  18343  psmettri  18344  psmetge0  18345  psmetres2  18347  xmetge0  18376  xmetsym  18379  xmettri  18383  xmetres2  18393  prdsxmetlem  18400  prdsmet  18402  imasdsf1olem  18405  imasf1oxmet  18407  bldisj  18430  xblss2ps  18433  xblss2  18434  xmeter  18465  prdsbl  18523  metustexhalfOLD  18595  metustexhalf  18596  metustOLD  18599  metust  18600  nrmmetd  18624  ngpsubcan  18662  nmmtri  18670  nmrtri  18672  ngptgp  18679  nlmvscnlem2  18723  nrginvrcnlem  18728  metdcnlem  18869  clmmulg  19120  cphabscl  19150  cphsqrcl2  19151  cphsqrcl3  19152  cphnmf  19160  cph2ass  19177  ipcau2  19193  tchcphlem2  19195  ipcnlem2  19200  cfilfcls  19229  iscau3  19233  iscmet3lem2  19247  iscmet3  19248  relcmpcmet  19271  minveclem2  19329  minveclem4  19335  pjthlem1  19340  pjthlem2  19341  uniioombllem4  19480  dyadmax  19492  itg1addlem4  19593  itg1climres  19608  evlslem1  19938  ply1divex  20061  aalioulem2  20252  amgmlem  20830  dvdsppwf1o  20973  perfect1  21014  perfectlem1  21015  perfectlem2  21016  dchrptlem2  21051  4cycl4dv4e  21657  eupa0  21698  eupares  21699  eupap1  21700  grpoidinvlem4  21797  grpoasscan2  21828  grpoinvop  21831  grpopncan  21841  grponpcan  21842  grpopnpcan2  21843  grpodiveq  21846  gxcom  21859  gxnn0add  21864  ghgrp  21958  rngo2  21978  rngolz  21991  rngorz  21992  zerdivemp1  22024  vcm  22052  nvmul0or  22135  nvpncan2  22139  nvnncan  22146  nvdif  22156  nvabs  22164  smcnlem  22195  lnomul  22263  minvecolem2  22379  superpos  23859  ssnnssfz  24150  dvrdir  24228  rdivmuldivd  24229  dvrcan5  24231  rhmdvd  24261  rhmunitinv  24262  metideq  24290  metider  24291  pstmxmet  24294  lmxrge0  24339  qqhghm  24374  qqhrhm  24375  ballotlemiex  24761  cvmopnlem  24967  cvmliftmolem2  24971  cvmliftlem6  24979  cvmliftlem8  24981  cvmliftlem9  24982  cvmlift2lem9  25000  cvmlift3lem2  25009  cvmlift3lem6  25013  cvmlift3lem7  25014  cvmlift3lem9  25016  zprod  25265  nodense  25646  axcontlem9  25913  cgrtriv  25938  cgrdegen  25940  cgrextend  25944  segconeq  25946  btwntriv2  25948  btwncomand  25951  btwntriv1  25952  btwnintr  25955  btwnexch3  25956  btwnouttr  25960  btwnexch  25961  trisegint  25964  ifscgr  25980  btwnxfr  25992  colineartriv1  26003  colineartriv2  26004  colinearxfr  26011  fscgr  26016  lineid  26019  idinside  26020  endofsegidand  26022  btwnconn1lem5  26027  btwnconn1lem7  26029  btwnconn1lem11  26033  btwnconn1lem12  26034  btwnconn1lem13  26035  brsegle2  26045  segleantisym  26051  broutsideof2  26058  btwnoutside  26061  outsideoftr  26065  outsideofeq  26066  outsideofeu  26067  outsidele  26068  lineunray  26083  lineelsb2  26084  linecom  26086  linethru  26089  neibastop1  26390  mettrifi  26465  isbnd3  26495  heibor1lem  26520  bfplem2  26534  ghomdiv  26561  zerdivemp1x  26573  irrapxlem5  26891  aomclem2  27132  frlmup1  27229  isnumbasgrplem2  27248  mpaaeu  27334  symggen  27390  mamuass  27439  mamudi  27440  mamudir  27441  mamuvs1  27442  mamuvs2  27443  mendrng  27479  mendlmod  27480  caofcan  27519  stoweidlem18  27745  stoweidlem41  27768  stoweidlem45  27772  stoweidlem55  27782  2cshw2lem3  28276  2cshw  28278  2cshwmod  28279  cshwssizelem4a  28305  cshwsdisj  28307  el2spthonot0  28391  usg2spthonot1  28410  frg2woteu  28506  lubunNEW  29833  lfladdcl  29931  lflvscl  29937  eqlkr3  29961  lkrlsp  29962  lshpkrlem4  29973  oldmm1  30077  olj01  30085  latmassOLD  30089  latm32  30091  latmrot  30092  latm4  30093  olm01  30096  cmtcomlemN  30108  cmtbr3N  30114  cmtbr4N  30115  lecmtN  30116  omlfh1N  30118  atlen0  30170  atnle  30177  atlatmstc  30179  atlatle  30180  cvlexchb1  30190  cvlcvr1  30199  ishlat3N  30214  hlatjass  30229  hlatj12  30230  hlatj32  30231  hlsupr2  30246  hlhgt2  30248  hl0lt1N  30249  hlrelat  30261  hlrelat2  30262  exatleN  30263  hlrelat3  30271  cvrval5  30274  cvrexchlem  30278  cvratlem  30280  cvrat  30281  atcvr0eq  30285  lnnat  30286  atlt  30296  atlelt  30297  2atlt  30298  atexchltN  30300  cvrat3  30301  2atjm  30304  atbtwn  30305  4noncolr3  30312  athgt  30315  3dimlem3a  30319  3dimlem3OLDN  30321  3dimlem4a  30322  3dimlem4OLDN  30324  3dim1  30326  3dim2  30327  1cvratex  30332  ps-1  30336  ps-2  30337  hlatexch3N  30339  hlatexch4  30340  ps-2b  30341  3atlem1  30342  3atlem2  30343  3atlem5  30346  3atlem6  30347  llnnleat  30372  llncmp  30381  2at0mat0  30384  2atmat0  30385  2atm  30386  lplni2  30396  lvolex3N  30397  lplnnle2at  30400  lplnnleat  30401  lplnnlelln  30402  2atnelpln  30403  llncvrlpln  30417  2atmat  30420  lplncmp  30421  lplnexllnN  30423  2llnjaN  30425  2llnm4  30429  2llnmeqat  30430  lvolnle3at  30441  lvolnleat  30442  2atnelvolN  30446  islvol2aN  30451  4atlem3  30455  4atlem3a  30456  4atlem3b  30457  4atlem4a  30458  4atlem4b  30459  4atlem4c  30460  4atlem4d  30461  4atlem10  30465  4atlem11b  30467  4atlem11  30468  4atlem12b  30470  4atlem12  30471  4at2  30473  lplncvrlvol  30475  lvolcmp  30476  2lplnja  30478  dalemqrprot  30507  dalemply  30513  dalemsly  30514  dalemrot  30516  dalemrotyz  30517  dalem1  30518  dalemcea  30519  dalem3  30523  dalem5  30526  dalem8  30529  dalem-cly  30530  dalem11  30533  dalem12  30534  dalem16  30538  dalem17  30539  dalem18  30540  dalem21  30553  dalem24  30556  dalem25  30557  dalem38  30569  dalem39  30570  dalem44  30575  dalem54  30585  dalem55  30586  dalem57  30588  dalem58  30589  dalem59  30590  dalem60  30591  dath2  30596  2atm2atN  30644  2llnma1b  30645  2llnma3r  30647  cdlema1N  30650  cdlemblem  30652  paddasslem5  30683  paddasslem10  30688  paddasslem12  30690  paddasslem13  30691  paddass  30697  padd12N  30698  padd4N  30699  paddss  30704  pmodlem1  30705  pmodl42N  30710  pmapjoin  30711  pmapjlln1  30714  atmod1i2  30718  llnmod1i2  30719  llnexchb2  30728  dalawlem2  30731  dalawlem3  30732  dalawlem5  30734  dalawlem6  30735  dalawlem7  30736  dalawlem8  30737  dalawlem11  30740  dalawlem12  30741  dalawlem13  30742  pclunN  30757  osumcllem1N  30815  pexmidlem3N  30831  lhp2lt  30860  lhp0lt  30862  lhpexle2lem  30868  lhpexle3lem  30870  lhpocnle  30875  lhpj1  30881  lhpmcvr4N  30885  lhp2at0  30891  lhpat3  30905  4atexlemtlw  30926  4atexlemc  30928  4atexlemnclw  30929  4atexlemcnd  30931  lautcvr  30951  lautj  30952  lautm  30953  ltrnm  30990  ltrnj  30991  ltrncvr  30992  trlval3  31046  cdlemc5  31054  cdlemd2  31058  cdlemd3  31059  cdleme0e  31076  cdleme1  31086  cdleme3c  31089  cdleme3g  31093  cdleme3h  31094  cdleme3  31096  cdleme5  31099  cdleme7c  31104  cdleme7d  31105  cdleme7e  31106  cdleme7ga  31107  cdleme7  31108  cdleme9  31112  cdleme11c  31120  cdleme11g  31124  cdleme11k  31127  cdleme11  31129  cdleme12  31130  cdleme15b  31134  cdleme15d  31136  cdleme16d  31140  cdleme16e  31141  cdleme16f  31142  cdleme17b  31146  cdleme18b  31151  cdleme22gb  31153  cdlemednpq  31158  cdleme19a  31162  cdleme20aN  31168  cdleme20bN  31169  cdleme20c  31170  cdleme20d  31171  cdleme20j  31177  cdleme21c  31186  cdleme22aa  31198  cdleme22b  31200  cdleme22cN  31201  cdleme22d  31202  cdleme22e  31203  cdleme22eALTN  31204  cdleme23b  31209  cdleme23c  31210  cdleme28a  31229  cdleme30a  31237  cdlemefs29bpre0N  31275  cdlemefs29bpre1N  31276  cdlemefs29cpre1N  31277  cdlemefs29clN  31278  cdlemefs32fvaN  31281  cdlemefs32fva1  31282  cdleme32b  31301  cdleme32c  31302  cdleme32e  31304  cdleme35a  31307  cdleme35fnpq  31308  cdleme35b  31309  cdleme35f  31313  cdleme36a  31319  cdleme36m  31320  cdleme37m  31321  cdleme39a  31324  cdleme42c  31331  cdleme42i  31342  cdleme42keg  31345  cdleme42mgN  31347  cdleme48bw  31361  cdlemeg46fjgN  31380  cdlemeg46fjv  31382  cdlemeg46req  31388  cdleme50trn1  31408  cdlemf1  31420  cdlemf2  31421  cdlemg1cex  31447  cdlemg2fv2  31459  cdlemg7fvbwN  31466  cdlemg4c  31471  cdlemg4  31476  cdlemg6c  31479  cdlemg8b  31487  cdlemg10c  31498  cdlemg10  31500  cdlemg11b  31501  cdlemg12f  31507  cdlemg13a  31510  cdlemg17a  31520  cdlemg17dALTN  31523  cdlemg18b  31538  cdlemg19a  31542  cdlemg27a  31551  cdlemg27b  31555  cdlemg33b0  31560  cdlemg33a  31565  cdlemg35  31572  trlcolem  31585  cdlemg42  31588  cdlemg46  31594  trljco  31599  tendopltp  31639  cdlemh1  31674  cdlemh2  31675  cdlemi1  31677  cdlemi  31679  cdlemk3  31692  cdlemk10  31702  cdlemk11  31708  cdlemk15  31714  cdlemk1u  31718  cdlemk5u  31720  cdlemk11u  31730  cdlemk39  31775  cdlemkid1  31781  cdlemk50  31811  cdlemk51  31812  erngdvlem3-rN  31857  tendocnv  31881  tendospcanN  31883  dialss  31906  dia2dimlem1  31924  dia2dimlem2  31925  dia2dimlem3  31926  dia2dimlem10  31933  dia2dimlem12  31935  dvhvaddass  31957  dvhlveclem  31968  cdlemm10N  31978  doca2N  31986  djajN  31997  dib1dim2  32028  diblss  32030  diclspsn  32054  cdlemn2  32055  cdlemn10  32066  dihjustlem  32076  dihord1  32078  dihord2a  32079  dihord2pre2  32086  dib2dim  32103  dih2dimb  32104  dih2dimbALTN  32105  dihopelvalcpre  32108  dihord5b  32119  dihord6b  32120  dihord5apre  32122  dihmeetlem1N  32150  dihglblem5apreN  32151  dihglblem2N  32154  dihglbcpreN  32160  dihmeetbclemN  32164  dihmeetlem3N  32165  dihmeetlem6  32169  dih1dimatlem  32189  djhcvat42  32275  dihjatcclem1  32278  dihjatcclem4  32281  dvh4dimat  32298  lcfl7lem  32359  lclkrlem2m  32379  lcfrlem1  32402  lcdvsass  32467  baerlem3lem1  32567  baerlem5alem1  32568  baerlem5blem1  32569  mapdh6gN  32602  mapdh6hN  32603  hdmap1l6g  32677  hdmap1l6h  32678  hdmapneg  32709  hdmap14lem8  32738  hgmapadd  32757  hgmapmul  32758  hgmapvvlem1  32786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator