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

Theorem syl121anc 1270
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 )
syl121anc.5  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl121anc  |-  ( ph  ->  et )

Proof of Theorem syl121anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
42, 3jca 535 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1265 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  syl122anc  1274  disjxiun  4418  fsnunf2  6116  tfisi  6697  fnsuppeq0  6952  axdc4lem  8887  div32d  10408  div13d  10409  expdivd  12431  swrdsbslen  12800  pcqmul  14796  pcid  14815  pcneg  14816  pc2dvds  14821  pcz  14823  pcaddlem  14826  pcadd  14827  pcmpt2  14831  pcbc  14838  qexpz  14839  expnprm  14840  sylow1lem1  17243  lspsneleq  18331  lspsneq  18338  lspfixed  18344  frlmsslss2  19325  chmatval  19845  chpmat1dlem  19851  chpdmatlem2  19855  ucncn  21292  ucnextcn  21311  ssblex  21435  prdsxmslem2  21536  voliunlem1  22495  deg1mul3le  23057  deg1pw  23061  fta1blem  23111  bcmono  24197  dchrisum0flblem1  24338  dchrisum0flblem2  24339  pntibndlem1  24419  pntlemr  24432  0wlkon  25269  0pthon  25301  clwlkfclwwlk  25564  nv1  26297  resf1o  28315  omndmul3  28477  rngurd  28553  measun  29035  measvuni  29038  measunl  29040  btwnconn1lem14  30866  segcon2  30871  seglelin  30882  neibastop3  31017  upixp  31976  fdc  31994  eqlkr3  32592  lkrshp  32596  lfl1dim  32612  lfl1dim2N  32613  eqlkr4  32656  2llnneN  32899  3dim2  32958  4atlem3  33086  4atlem11  33099  4atlem12  33102  pexmidlem4N  33463  lhp2at0nle  33525  lhple  33532  ltrnideq  33666  cdlemd9  33697  cdleme0ex2N  33715  cdleme0moN  33716  cdleme11a  33751  cdleme30a  33870  cdlemefs32sn1aw  33906  cdleme43fsv1snlem  33912  cdlemefs31fv1  33916  cdlemefs45eN  33923  cdleme41sn3a  33925  cdleme35h  33948  cdleme36a  33952  cdleme40m  33959  cdleme40n  33960  cdleme41sn3aw  33966  cdleme42h  33974  cdleme42k  33976  cdleme42mN  33979  cdleme43cN  33983  cdleme17d3  33988  cdleme48fvg  33992  cdlemeg47rv2  34002  cdlemeg46c  34005  cdlemeg46sfg  34012  cdlemeg46rjgN  34014  cdlemeg46rgv  34020  cdlemeg46req  34021  cdlemeg46gfv  34022  cdlemeg46gfre  34024  cdlemeg49lebilem  34031  cdleme50trn2  34043  cdlemg2kq  34094  cdlemb3  34098  cdlemg4f  34107  cdlemg9a  34124  cdlemg9b  34125  cdlemg9  34126  cdlemg11aq  34130  cdlemg12a  34135  cdlemg12b  34136  cdlemg12c  34137  cdlemg12d  34138  cdlemg12f  34140  cdlemg12g  34141  cdlemg12  34142  cdlemg13a  34143  cdlemg16  34149  cdlemg17e  34157  cdlemg17f  34158  cdlemg17g  34159  cdlemg17ir  34162  cdlemg17  34169  cdlemg18b  34171  cdlemg18c  34172  cdlemg33e  34202  trlcoabs2N  34214  trlcocnvat  34216  trlcolem  34218  trlco  34219  cdlemg44  34225  cdlemg47  34228  ltrncom  34230  tendococl  34264  tendoplcl  34273  tendoplcom  34274  tendoplass  34275  tendodi1  34276  tendodi2  34277  tendo0pl  34283  tendoipl  34289  cdlemh1  34307  cdlemi2  34311  tendo0mul  34318  tendo0mulr  34319  cdlemk2  34324  cdlemk3  34325  cdlemk4  34326  cdlemk6  34329  cdlemk8  34330  cdlemk12  34342  cdlemkole  34345  cdlemk14  34346  cdlemk15  34347  cdlemk5u  34353  cdlemk6u  34354  cdlemk12u  34364  cdlemkfid1N  34413  cdlemk19x  34435  cdlemk48  34442  cdlemk53a  34447  cdlemk56  34463  cdleml2N  34469  cdleml3N  34470  cdleml6  34473  cdleml7  34474  dva1dim  34477  dia2dimlem4  34560  dvhlveclem  34601  doca2N  34619  djajN  34630  cdlemn2a  34689  cdlemn3  34690  dihordlem6  34706  dihord5apre  34755  dihglbcpreN  34793  dihmeetcN  34795  dihmeetbN  34796  dihmeetlem10N  34809  dihmeetlem12N  34811  dihmeetlem15N  34814  dihmeetALTN  34820  dih1dimatlem0  34821  dihjatcclem3  34913  dihjatcclem4  34914  mapdpglem22  35186  hdmap14lem1a  35362  eldioph2b  35530  jm2.19lem4  35773  jm2.19  35774  jm2.26a  35781  jm2.26  35783  hbtlem2  35909  fnchoice  37217  stoweidlem42  37729  stoweidlem59  37746  fourierdlem42  37838  fourierdlem42OLD  37839
  Copyright terms: Public domain W3C validator