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  28256  2cshw  28258  2cshwmod  28259  cshwssizelem4a  28285  cshwsdisj  28287  el2spthonot0  28340  usg2spthonot1  28359  frg2woteu  28446  lubunNEW  29773  lfladdcl  29871  lflvscl  29877  eqlkr3  29901  lkrlsp  29902  lshpkrlem4  29913  oldmm1  30017  olj01  30025  latmassOLD  30029  latm32  30031  latmrot  30032  latm4  30033  olm01  30036  cmtcomlemN  30048  cmtbr3N  30054  cmtbr4N  30055  lecmtN  30056  omlfh1N  30058  atlen0  30110  atnle  30117  atlatmstc  30119  atlatle  30120  cvlexchb1  30130  cvlcvr1  30139  ishlat3N  30154  hlatjass  30169  hlatj12  30170  hlatj32  30171  hlsupr2  30186  hlhgt2  30188  hl0lt1N  30189  hlrelat  30201  hlrelat2  30202  exatleN  30203  hlrelat3  30211  cvrval5  30214  cvrexchlem  30218  cvratlem  30220  cvrat  30221  atcvr0eq  30225  lnnat  30226  atlt  30236  atlelt  30237  2atlt  30238  atexchltN  30240  cvrat3  30241  2atjm  30244  atbtwn  30245  4noncolr3  30252  athgt  30255  3dimlem3a  30259  3dimlem3OLDN  30261  3dimlem4a  30262  3dimlem4OLDN  30264  3dim1  30266  3dim2  30267  1cvratex  30272  ps-1  30276  ps-2  30277  hlatexch3N  30279  hlatexch4  30280  ps-2b  30281  3atlem1  30282  3atlem2  30283  3atlem5  30286  3atlem6  30287  llnnleat  30312  llncmp  30321  2at0mat0  30324  2atmat0  30325  2atm  30326  lplni2  30336  lvolex3N  30337  lplnnle2at  30340  lplnnleat  30341  lplnnlelln  30342  2atnelpln  30343  llncvrlpln  30357  2atmat  30360  lplncmp  30361  lplnexllnN  30363  2llnjaN  30365  2llnm4  30369  2llnmeqat  30370  lvolnle3at  30381  lvolnleat  30382  2atnelvolN  30386  islvol2aN  30391  4atlem3  30395  4atlem3a  30396  4atlem3b  30397  4atlem4a  30398  4atlem4b  30399  4atlem4c  30400  4atlem4d  30401  4atlem10  30405  4atlem11b  30407  4atlem11  30408  4atlem12b  30410  4atlem12  30411  4at2  30413  lplncvrlvol  30415  lvolcmp  30416  2lplnja  30418  dalemqrprot  30447  dalemply  30453  dalemsly  30454  dalemrot  30456  dalemrotyz  30457  dalem1  30458  dalemcea  30459  dalem3  30463  dalem5  30466  dalem8  30469  dalem-cly  30470  dalem11  30473  dalem12  30474  dalem16  30478  dalem17  30479  dalem18  30480  dalem21  30493  dalem24  30496  dalem25  30497  dalem38  30509  dalem39  30510  dalem44  30515  dalem54  30525  dalem55  30526  dalem57  30528  dalem58  30529  dalem59  30530  dalem60  30531  dath2  30536  2atm2atN  30584  2llnma1b  30585  2llnma3r  30587  cdlema1N  30590  cdlemblem  30592  paddasslem5  30623  paddasslem10  30628  paddasslem12  30630  paddasslem13  30631  paddass  30637  padd12N  30638  padd4N  30639  paddss  30644  pmodlem1  30645  pmodl42N  30650  pmapjoin  30651  pmapjlln1  30654  atmod1i2  30658  llnmod1i2  30659  llnexchb2  30668  dalawlem2  30671  dalawlem3  30672  dalawlem5  30674  dalawlem6  30675  dalawlem7  30676  dalawlem8  30677  dalawlem11  30680  dalawlem12  30681  dalawlem13  30682  pclunN  30697  osumcllem1N  30755  pexmidlem3N  30771  lhp2lt  30800  lhp0lt  30802  lhpexle2lem  30808  lhpexle3lem  30810  lhpocnle  30815  lhpj1  30821  lhpmcvr4N  30825  lhp2at0  30831  lhpat3  30845  4atexlemtlw  30866  4atexlemc  30868  4atexlemnclw  30869  4atexlemcnd  30871  lautcvr  30891  lautj  30892  lautm  30893  ltrnm  30930  ltrnj  30931  ltrncvr  30932  trlval3  30986  cdlemc5  30994  cdlemd2  30998  cdlemd3  30999  cdleme0e  31016  cdleme1  31026  cdleme3c  31029  cdleme3g  31033  cdleme3h  31034  cdleme3  31036  cdleme5  31039  cdleme7c  31044  cdleme7d  31045  cdleme7e  31046  cdleme7ga  31047  cdleme7  31048  cdleme9  31052  cdleme11c  31060  cdleme11g  31064  cdleme11k  31067  cdleme11  31069  cdleme12  31070  cdleme15b  31074  cdleme15d  31076  cdleme16d  31080  cdleme16e  31081  cdleme16f  31082  cdleme17b  31086  cdleme18b  31091  cdleme22gb  31093  cdlemednpq  31098  cdleme19a  31102  cdleme20aN  31108  cdleme20bN  31109  cdleme20c  31110  cdleme20d  31111  cdleme20j  31117  cdleme21c  31126  cdleme22aa  31138  cdleme22b  31140  cdleme22cN  31141  cdleme22d  31142  cdleme22e  31143  cdleme22eALTN  31144  cdleme23b  31149  cdleme23c  31150  cdleme28a  31169  cdleme30a  31177  cdlemefs29bpre0N  31215  cdlemefs29bpre1N  31216  cdlemefs29cpre1N  31217  cdlemefs29clN  31218  cdlemefs32fvaN  31221  cdlemefs32fva1  31222  cdleme32b  31241  cdleme32c  31242  cdleme32e  31244  cdleme35a  31247  cdleme35fnpq  31248  cdleme35b  31249  cdleme35f  31253  cdleme36a  31259  cdleme36m  31260  cdleme37m  31261  cdleme39a  31264  cdleme42c  31271  cdleme42i  31282  cdleme42keg  31285  cdleme42mgN  31287  cdleme48bw  31301  cdlemeg46fjgN  31320  cdlemeg46fjv  31322  cdlemeg46req  31328  cdleme50trn1  31348  cdlemf1  31360  cdlemf2  31361  cdlemg1cex  31387  cdlemg2fv2  31399  cdlemg7fvbwN  31406  cdlemg4c  31411  cdlemg4  31416  cdlemg6c  31419  cdlemg8b  31427  cdlemg10c  31438  cdlemg10  31440  cdlemg11b  31441  cdlemg12f  31447  cdlemg13a  31450  cdlemg17a  31460  cdlemg17dALTN  31463  cdlemg18b  31478  cdlemg19a  31482  cdlemg27a  31491  cdlemg27b  31495  cdlemg33b0  31500  cdlemg33a  31505  cdlemg35  31512  trlcolem  31525  cdlemg42  31528  cdlemg46  31534  trljco  31539  tendopltp  31579  cdlemh1  31614  cdlemh2  31615  cdlemi1  31617  cdlemi  31619  cdlemk3  31632  cdlemk10  31642  cdlemk11  31648  cdlemk15  31654  cdlemk1u  31658  cdlemk5u  31660  cdlemk11u  31670  cdlemk39  31715  cdlemkid1  31721  cdlemk50  31751  cdlemk51  31752  erngdvlem3-rN  31797  tendocnv  31821  tendospcanN  31823  dialss  31846  dia2dimlem1  31864  dia2dimlem2  31865  dia2dimlem3  31866  dia2dimlem10  31873  dia2dimlem12  31875  dvhvaddass  31897  dvhlveclem  31908  cdlemm10N  31918  doca2N  31926  djajN  31937  dib1dim2  31968  diblss  31970  diclspsn  31994  cdlemn2  31995  cdlemn10  32006  dihjustlem  32016  dihord1  32018  dihord2a  32019  dihord2pre2  32026  dib2dim  32043  dih2dimb  32044  dih2dimbALTN  32045  dihopelvalcpre  32048  dihord5b  32059  dihord6b  32060  dihord5apre  32062  dihmeetlem1N  32090  dihglblem5apreN  32091  dihglblem2N  32094  dihglbcpreN  32100  dihmeetbclemN  32104  dihmeetlem3N  32105  dihmeetlem6  32109  dih1dimatlem  32129  djhcvat42  32215  dihjatcclem1  32218  dihjatcclem4  32221  dvh4dimat  32238  lcfl7lem  32299  lclkrlem2m  32319  lcfrlem1  32342  lcdvsass  32407  baerlem3lem1  32507  baerlem5alem1  32508  baerlem5blem1  32509  mapdh6gN  32542  mapdh6hN  32543  hdmap1l6g  32617  hdmap1l6h  32618  hdmapneg  32649  hdmap14lem8  32678  hgmapadd  32697  hgmapmul  32698  hgmapvvlem1  32726
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