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

Theorem syl13anc 1186
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 1134 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 643 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl23anc  1191  syl33anc  1199  pm2.61da3ne  2647  disjxiun  4169  wereu2  4539  ordelord  4563  caovassd  6205  caovcand  6208  caovordid  6212  caovordd  6214  caovdid  6221  caovdird  6224  swoer  6892  swoord1  6893  swoord2  6894  frfi  7311  indexfi  7372  ssfii  7382  elfiun  7393  suplub2  7422  wemaplem2  7472  htalem  7776  cofsmo  8105  alephsing  8112  sornom  8113  axdc3lem4  8289  zorn2lem1  8332  ttukeylem6  8350  ttukeylem7  8351  prlem934  8866  fzosubel3  11134  seqsplit  11311  seqcaopr  11315  ccatass  11705  splid  11737  spllen  11738  splfv1  11739  splfv2a  11740  splval2  11741  wrdeqcats1  11743  wrdeqs1cat  11744  swrds2  11835  isercolllem2  12414  fsumiun  12555  pcgcd1  13205  firest  13615  iscatd2  13861  posasymb  14364  meetle  14412  lattrd  14442  latleeqj1  14447  latjlej1  14449  latjlej12  14451  latnlej2  14455  latjidm  14458  latleeqm1  14463  latmlem1  14465  latmlem12  14467  latmidm  14470  latledi  14473  latjass  14479  latj12  14480  latj13  14482  latj31  14483  latjrot  14484  latj4  14485  mod1ile  14489  lubun  14505  clatleglb  14508  latdisdlem  14570  mnd32g  14654  mnd12g  14655  mnd4g  14656  prdsmndd  14683  imasmnd  14688  gsumspl  14744  grpinvinv  14813  grplmulf1o  14820  grpinvadd  14822  grpsubrcan  14825  grpsubadd  14831  grpaddsubass  14833  grppncan  14834  grpsubsub4  14836  grppnpcan2  14837  grpnpncan  14838  grpnnncan2  14839  grplactcnv  14842  mulgnn0dir  14868  mulgdirlem  14869  mulgneg2  14872  mulgnnass  14873  mulgnn0ass  14874  mulgass  14875  imasgrp  14889  nsgconj  14928  isnsg3  14929  nmzsubg  14936  ssnmz  14937  eqger  14945  eqgcpbl  14949  conjghm  14991  conjnmz  14994  conjnmzb  14995  subgga  15032  gass  15033  gasubg  15034  galcan  15036  gacan  15037  gapm  15038  gaorber  15040  gastacl  15041  gastacos  15042  cntzsubm  15089  cntzsubg  15090  oppgmnd  15105  odmodnn0  15133  mndodconglem  15134  odmod  15139  odcong  15142  odmulgid  15145  odbezout  15149  gexdvdsi  15172  gexdvds  15173  sylow1lem2  15188  sylow1lem4  15190  sylow2blem1  15209  sylow2blem2  15210  sylow2blem3  15211  sylow3lem1  15216  sylow3lem2  15217  lsmass  15257  lsmmod  15262  lsmdisj2  15269  subgdisj1  15278  efgredleme  15330  efgredlemc  15332  efgcpbllemb  15342  frgp0  15347  frgpuplem  15359  abl32  15388  abladdsub4  15393  abladdsub  15394  ablpncan2  15395  ablsubsub  15397  mulgdi  15404  mulgsubdi  15407  odadd1  15418  odadd2  15419  gex2abl  15421  oddvdssubg  15425  cygabl  15455  ablfacrp  15579  pgpfac1lem2  15588  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfac1lem4  15591  rngcom  15647  rnglz  15655  rngrz  15656  rngnegl  15658  rngnegr  15659  rngmneg1  15660  rngmneg2  15661  rngsubdi  15663  rngsubdir  15664  mulgass2  15665  prdsrngd  15673  imasrng  15680  opprrng  15691  mulgass3  15697  dvdsrtr  15712  dvdsrmul1  15713  unitgrp  15727  dvrass  15750  dvrcan1  15751  dvrcan3  15752  irredrmul  15767  drngmul0or  15811  subrginv  15839  cntzsubr  15855  lmod0vs  15938  lmodvs0  15939  lmodvneg1  15942  lmodvsneg  15943  lmodcom  15945  lmodsubvs  15955  lmodsubdi  15956  lmodsubdir  15957  lssvsubcl  15975  lssvacl  15985  lssvscl  15986  islss3  15990  lss1d  15994  lssintcl  15995  prdslmodd  16000  lmodvsinv  16067  lmodvsinv2  16068  lmhmplusg  16075  lmhmvsca  16076  lsmcl  16110  pj1lmhm  16127  lvecvs0or  16135  lssvs0or  16137  lvecinv  16140  lspsnvs  16141  lspfixed  16155  lspexch  16156  lspsolvlem  16169  lspsolv  16170  lssacsex  16171  lspsnat  16172  lsppratlem1  16174  lsppratlem3  16176  lsppratlem4  16177  lbsextlem2  16186  lbsextlem4  16188  sralmod  16213  2idlcpbl  16260  unitrrg  16308  issubassa  16338  sraassa  16339  asclghm  16352  asclmul1  16353  asclmul2  16354  asclrhm  16355  psrbagcon  16391  psrbagconcl  16393  psrbagconf1o  16394  gsumbagdiaglem  16395  psrmulcllem  16406  psrlidm  16422  psrridm  16423  psrass1  16424  psrdi  16425  psrdir  16426  psrcom  16427  psrass23  16428  mplmon2mul  16516  coe1subfv  16614  mulgrhm  16742  cygznlem3  16805  ipdi  16826  ip2di  16827  ipsubdir  16828  ipsubdi  16829  ip2subdi  16830  ipassr  16832  ipassr2  16833  ip2eq  16839  ocvlss  16854  lsmcss  16874  iinopn  16930  subbascn  17272  cnhaus  17372  nrmsep2  17374  nrmsep  17375  regsep2  17394  isreg2  17395  hauscmplem  17423  1stcfb  17461  2ndcctbss  17471  ptbasfi  17566  pthaus  17623  txtube  17625  txhaus  17632  xkohaus  17638  kqnrmlem1  17728  kqnrmlem2  17729  nrmr0reg  17734  nrmhmph  17779  fbssint  17823  infil  17848  fgabs  17864  filcon  17868  filuni  17870  trfil2  17872  trfg  17876  ufprim  17894  elfm3  17935  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  hausflimi  17965  hauspwpwf1  17972  fclsneii  18002  supnfcls  18005  flimfnfcls  18013  fclscmpi  18014  alexsublem  18028  ghmcnp  18097  divstgpopn  18102  psmetsym  18294  psmettri  18295  psmetge0  18296  psmetres2  18298  xmetge0  18327  xmetsym  18330  xmettri  18334  xmetres2  18344  prdsxmetlem  18351  prdsmet  18353  imasdsf1olem  18356  imasf1oxmet  18358  bldisj  18381  xblss2ps  18384  xblss2  18385  xmeter  18416  prdsbl  18474  metustexhalfOLD  18546  metustexhalf  18547  metustOLD  18550  metust  18551  nrmmetd  18575  ngpsubcan  18613  nmmtri  18621  nmrtri  18623  ngptgp  18630  nlmvscnlem2  18674  nrginvrcnlem  18679  metdcnlem  18820  clmmulg  19071  cphabscl  19101  cphsqrcl2  19102  cphsqrcl3  19103  cphnmf  19111  cph2ass  19128  ipcau2  19144  tchcphlem2  19146  ipcnlem2  19151  cfilfcls  19180  iscau3  19184  iscmet3lem2  19198  iscmet3  19199  relcmpcmet  19222  minveclem2  19280  minveclem4  19286  pjthlem1  19291  pjthlem2  19292  uniioombllem4  19431  dyadmax  19443  itg1addlem4  19544  itg1climres  19559  evlslem1  19889  ply1divex  20012  aalioulem2  20203  amgmlem  20781  dvdsppwf1o  20924  perfect1  20965  perfectlem1  20966  perfectlem2  20967  dchrptlem2  21002  4cycl4dv4e  21608  eupa0  21649  eupares  21650  eupap1  21651  grpoidinvlem4  21748  grpoasscan2  21779  grpoinvop  21782  grpopncan  21792  grponpcan  21793  grpopnpcan2  21794  grpodiveq  21797  gxcom  21810  gxnn0add  21815  ghgrp  21909  rngo2  21929  rngolz  21942  rngorz  21943  zerdivemp1  21975  vcm  22003  nvmul0or  22086  nvpncan2  22090  nvnncan  22097  nvdif  22107  nvabs  22115  smcnlem  22146  lnomul  22214  minvecolem2  22330  superpos  23810  ssnnssfz  24101  dvrdir  24179  rdivmuldivd  24180  dvrcan5  24182  rhmdvd  24212  rhmunitinv  24213  metideq  24241  metider  24242  pstmxmet  24245  lmxrge0  24290  qqhghm  24325  qqhrhm  24326  ballotlemiex  24712  cvmopnlem  24918  cvmliftmolem2  24922  cvmliftlem6  24930  cvmliftlem8  24932  cvmliftlem9  24933  cvmlift2lem9  24951  cvmlift3lem2  24960  cvmlift3lem6  24964  cvmlift3lem7  24965  cvmlift3lem9  24967  zprod  25216  nodense  25557  axcontlem9  25815  cgrtriv  25840  cgrdegen  25842  cgrextend  25846  segconeq  25848  btwntriv2  25850  btwncomand  25853  btwntriv1  25854  btwnintr  25857  btwnexch3  25858  btwnouttr  25862  btwnexch  25863  trisegint  25866  ifscgr  25882  btwnxfr  25894  colineartriv1  25905  colineartriv2  25906  colinearxfr  25913  fscgr  25918  lineid  25921  idinside  25922  endofsegidand  25924  btwnconn1lem5  25929  btwnconn1lem7  25931  btwnconn1lem11  25935  btwnconn1lem12  25936  btwnconn1lem13  25937  brsegle2  25947  segleantisym  25953  broutsideof2  25960  btwnoutside  25963  outsideoftr  25967  outsideofeq  25968  outsideofeu  25969  outsidele  25970  lineunray  25985  lineelsb2  25986  linecom  25988  linethru  25991  neibastop1  26278  mettrifi  26353  isbnd3  26383  heibor1lem  26408  bfplem2  26422  ghomdiv  26449  zerdivemp1x  26461  irrapxlem5  26779  aomclem2  27020  frlmup1  27118  isnumbasgrplem2  27137  mpaaeu  27223  symggen  27279  mamuass  27328  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  mendrng  27368  mendlmod  27369  caofcan  27408  stoweidlem18  27634  stoweidlem41  27657  stoweidlem45  27661  stoweidlem55  27671  swrdccatin2  28018  el2spthonot0  28068  usg2spthonot1  28087  frg2woteu  28158  lubunNEW  29456  lfladdcl  29554  lflvscl  29560  eqlkr3  29584  lkrlsp  29585  lshpkrlem4  29596  oldmm1  29700  olj01  29708  latmassOLD  29712  latm32  29714  latmrot  29715  latm4  29716  olm01  29719  cmtcomlemN  29731  cmtbr3N  29737  cmtbr4N  29738  lecmtN  29739  omlfh1N  29741  atlen0  29793  atnle  29800  atlatmstc  29802  atlatle  29803  cvlexchb1  29813  cvlcvr1  29822  ishlat3N  29837  hlatjass  29852  hlatj12  29853  hlatj32  29854  hlsupr2  29869  hlhgt2  29871  hl0lt1N  29872  hlrelat  29884  hlrelat2  29885  exatleN  29886  hlrelat3  29894  cvrval5  29897  cvrexchlem  29901  cvratlem  29903  cvrat  29904  atcvr0eq  29908  lnnat  29909  atlt  29919  atlelt  29920  2atlt  29921  atexchltN  29923  cvrat3  29924  2atjm  29927  atbtwn  29928  4noncolr3  29935  athgt  29938  3dimlem3a  29942  3dimlem3OLDN  29944  3dimlem4a  29945  3dimlem4OLDN  29947  3dim1  29949  3dim2  29950  1cvratex  29955  ps-1  29959  ps-2  29960  hlatexch3N  29962  hlatexch4  29963  ps-2b  29964  3atlem1  29965  3atlem2  29966  3atlem5  29969  3atlem6  29970  llnnleat  29995  llncmp  30004  2at0mat0  30007  2atmat0  30008  2atm  30009  lplni2  30019  lvolex3N  30020  lplnnle2at  30023  lplnnleat  30024  lplnnlelln  30025  2atnelpln  30026  llncvrlpln  30040  2atmat  30043  lplncmp  30044  lplnexllnN  30046  2llnjaN  30048  2llnm4  30052  2llnmeqat  30053  lvolnle3at  30064  lvolnleat  30065  2atnelvolN  30069  islvol2aN  30074  4atlem3  30078  4atlem3a  30079  4atlem3b  30080  4atlem4a  30081  4atlem4b  30082  4atlem4c  30083  4atlem4d  30084  4atlem10  30088  4atlem11b  30090  4atlem11  30091  4atlem12b  30093  4atlem12  30094  4at2  30096  lplncvrlvol  30098  lvolcmp  30099  2lplnja  30101  dalemqrprot  30130  dalemply  30136  dalemsly  30137  dalemrot  30139  dalemrotyz  30140  dalem1  30141  dalemcea  30142  dalem3  30146  dalem5  30149  dalem8  30152  dalem-cly  30153  dalem11  30156  dalem12  30157  dalem16  30161  dalem17  30162  dalem18  30163  dalem21  30176  dalem24  30179  dalem25  30180  dalem38  30192  dalem39  30193  dalem44  30198  dalem54  30208  dalem55  30209  dalem57  30211  dalem58  30212  dalem59  30213  dalem60  30214  dath2  30219  2atm2atN  30267  2llnma1b  30268  2llnma3r  30270  cdlema1N  30273  cdlemblem  30275  paddasslem5  30306  paddasslem10  30311  paddasslem12  30313  paddasslem13  30314  paddass  30320  padd12N  30321  padd4N  30322  paddss  30327  pmodlem1  30328  pmodl42N  30333  pmapjoin  30334  pmapjlln1  30337  atmod1i2  30341  llnmod1i2  30342  llnexchb2  30351  dalawlem2  30354  dalawlem3  30355  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem11  30363  dalawlem12  30364  dalawlem13  30365  pclunN  30380  osumcllem1N  30438  pexmidlem3N  30454  lhp2lt  30483  lhp0lt  30485  lhpexle2lem  30491  lhpexle3lem  30493  lhpocnle  30498  lhpj1  30504  lhpmcvr4N  30508  lhp2at0  30514  lhpat3  30528  4atexlemtlw  30549  4atexlemc  30551  4atexlemnclw  30552  4atexlemcnd  30554  lautcvr  30574  lautj  30575  lautm  30576  ltrnm  30613  ltrnj  30614  ltrncvr  30615  trlval3  30669  cdlemc5  30677  cdlemd2  30681  cdlemd3  30682  cdleme0e  30699  cdleme1  30709  cdleme3c  30712  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme5  30722  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme9  30735  cdleme11c  30743  cdleme11g  30747  cdleme11k  30750  cdleme11  30752  cdleme12  30753  cdleme15b  30757  cdleme15d  30759  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme17b  30769  cdleme18b  30774  cdleme22gb  30776  cdlemednpq  30781  cdleme19a  30785  cdleme20aN  30791  cdleme20bN  30792  cdleme20c  30793  cdleme20d  30794  cdleme20j  30800  cdleme21c  30809  cdleme22aa  30821  cdleme22b  30823  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22eALTN  30827  cdleme23b  30832  cdleme23c  30833  cdleme28a  30852  cdleme30a  30860  cdlemefs29bpre0N  30898  cdlemefs29bpre1N  30899  cdlemefs29cpre1N  30900  cdlemefs29clN  30901  cdlemefs32fvaN  30904  cdlemefs32fva1  30905  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35a  30930  cdleme35fnpq  30931  cdleme35b  30932  cdleme35f  30936  cdleme36a  30942  cdleme36m  30943  cdleme37m  30944  cdleme39a  30947  cdleme42c  30954  cdleme42i  30965  cdleme42keg  30968  cdleme42mgN  30970  cdleme48bw  30984  cdlemeg46fjgN  31003  cdlemeg46fjv  31005  cdlemeg46req  31011  cdleme50trn1  31031  cdlemf1  31043  cdlemf2  31044  cdlemg1cex  31070  cdlemg2fv2  31082  cdlemg7fvbwN  31089  cdlemg4c  31094  cdlemg4  31099  cdlemg6c  31102  cdlemg8b  31110  cdlemg10c  31121  cdlemg10  31123  cdlemg11b  31124  cdlemg12f  31130  cdlemg13a  31133  cdlemg17a  31143  cdlemg17dALTN  31146  cdlemg18b  31161  cdlemg19a  31165  cdlemg27a  31174  cdlemg27b  31178  cdlemg33b0  31183  cdlemg33a  31188  cdlemg35  31195  trlcolem  31208  cdlemg42  31211  cdlemg46  31217  trljco  31222  tendopltp  31262  cdlemh1  31297  cdlemh2  31298  cdlemi1  31300  cdlemi  31302  cdlemk3  31315  cdlemk10  31325  cdlemk11  31331  cdlemk15  31337  cdlemk1u  31341  cdlemk5u  31343  cdlemk11u  31353  cdlemk39  31398  cdlemkid1  31404  cdlemk50  31434  cdlemk51  31435  erngdvlem3-rN  31480  tendocnv  31504  tendospcanN  31506  dialss  31529  dia2dimlem1  31547  dia2dimlem2  31548  dia2dimlem3  31549  dia2dimlem10  31556  dia2dimlem12  31558  dvhvaddass  31580  dvhlveclem  31591  cdlemm10N  31601  doca2N  31609  djajN  31620  dib1dim2  31651  diblss  31653  diclspsn  31677  cdlemn2  31678  cdlemn10  31689  dihjustlem  31699  dihord1  31701  dihord2a  31702  dihord2pre2  31709  dib2dim  31726  dih2dimb  31727  dih2dimbALTN  31728  dihopelvalcpre  31731  dihord5b  31742  dihord6b  31743  dihord5apre  31745  dihmeetlem1N  31773  dihglblem5apreN  31774  dihglblem2N  31777  dihglbcpreN  31783  dihmeetbclemN  31787  dihmeetlem3N  31788  dihmeetlem6  31792  dih1dimatlem  31812  djhcvat42  31898  dihjatcclem1  31901  dihjatcclem4  31904  dvh4dimat  31921  lcfl7lem  31982  lclkrlem2m  32002  lcfrlem1  32025  lcdvsass  32090  baerlem3lem1  32190  baerlem5alem1  32191  baerlem5blem1  32192  mapdh6gN  32225  mapdh6hN  32226  hdmap1l6g  32300  hdmap1l6h  32301  hdmapneg  32332  hdmap14lem8  32361  hgmapadd  32380  hgmapmul  32381  hgmapvvlem1  32409
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator