Theorem syl121anc 1323

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl121anc.5	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl121anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl121anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 553	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1318	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl122anc  1327  disjxiunOLD  4580  fsnunf2  6357  tfisi  6950  fnsuppeq0  7210  axdc4lem  9160  div32d  10703  div13d  10704  expdivd  12884  swrdsbslen  13300  pcqmul  15396  pcid  15415  pcneg  15416  pc2dvds  15421  pcz  15423  pcaddlem  15430  pcadd  15431  pcmpt2  15435  pcbc  15442  qexpz  15443  expnprm  15444  sylow1lem1  17836  lspsneleq  18936  lspsneq  18943  lspfixed  18949  frlmsslss2  19933  chmatval  20453  chpmat1dlem  20459  chpdmatlem2  20463  ucncn  21899  ucnextcn  21918  ssblex  22043  prdsxmslem2  22144  ncvs1  22765  voliunlem1  23125  deg1mul3le  23680  deg1pw  23684  fta1blem  23732  bcmono  24802  dchrisum0flblem1  24997  dchrisum0flblem2  24998  pntibndlem1  25078  pntlemr  25091  0wlkon  26077  0pthon  26109  clwlkfclwwlk  26371  nv1  26914  resf1o  28893  omndmul3  29044  rngurd  29119  measun  29601  measvuni  29604  measunl  29606  btwnconn1lem14  31377  segcon2  31382  seglelin  31393  neibastop3  31527  upixp  32694  fdc  32711  eqlkr3  33406  lkrshp  33410  lfl1dim  33426  lfl1dim2N  33427  eqlkr4  33470  2llnneN  33713  3dim2  33772  4atlem3  33900  4atlem11  33913  4atlem12  33916  pexmidlem4N  34277  lhp2at0nle  34339  lhple  34346  ltrnideq  34480  cdlemd9  34511  cdleme0ex2N  34529  cdleme0moN  34530  cdleme11a  34565  cdleme30a  34684  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdlemefs31fv1  34730  cdlemefs45eN  34737  cdleme41sn3a  34739  cdleme35h  34762  cdleme36a  34766  cdleme40m  34773  cdleme40n  34774  cdleme41sn3aw  34780  cdleme42h  34788  cdleme42k  34790  cdleme42mN  34793  cdleme43cN  34797  cdleme17d3  34802  cdleme48fvg  34806  cdlemeg47rv2  34816  cdlemeg46c  34819  cdlemeg46sfg  34826  cdlemeg46rjgN  34828  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemeg46gfv  34836  cdlemeg46gfre  34838  cdlemeg49lebilem  34845  cdleme50trn2  34857  cdlemg2kq  34908  cdlemb3  34912  cdlemg4f  34921  cdlemg9a  34938  cdlemg9b  34939  cdlemg9  34940  cdlemg11aq  34944  cdlemg12a  34949  cdlemg12b  34950  cdlemg12c  34951  cdlemg12d  34952  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg16  34963  cdlemg17e  34971  cdlemg17f  34972  cdlemg17g  34973  cdlemg17ir  34976  cdlemg17  34983  cdlemg18b  34985  cdlemg18c  34986  cdlemg33e  35016  trlcoabs2N  35028  trlcocnvat  35030  trlcolem  35032  trlco  35033  cdlemg44  35039  cdlemg47  35042  ltrncom  35044  tendococl  35078  tendoplcl  35087  tendoplcom  35088  tendoplass  35089  tendodi1  35090  tendodi2  35091  tendo0pl  35097  tendoipl  35103  cdlemh1  35121  cdlemi2  35125  tendo0mul  35132  tendo0mulr  35133  cdlemk2  35138  cdlemk3  35139  cdlemk4  35140  cdlemk6  35143  cdlemk8  35144  cdlemk12  35156  cdlemkole  35159  cdlemk14  35160  cdlemk15  35161  cdlemk5u  35167  cdlemk6u  35168  cdlemk12u  35178  cdlemkfid1N  35227  cdlemk19x  35249  cdlemk48  35256  cdlemk53a  35261  cdlemk56  35277  cdleml2N  35283  cdleml3N  35284  cdleml6  35287  cdleml7  35288  dva1dim  35291  dia2dimlem4  35374  dvhlveclem  35415  doca2N  35433  djajN  35444  cdlemn2a  35503  cdlemn3  35504  dihordlem6  35520  dihord5apre  35569  dihglbcpreN  35607  dihmeetcN  35609  dihmeetbN  35610  dihmeetlem10N  35623  dihmeetlem12N  35625  dihmeetlem15N  35628  dihmeetALTN  35634  dih1dimatlem0  35635  dihjatcclem3  35727  dihjatcclem4  35728  mapdpglem22  36000  hdmap14lem1a  36176  eldioph2b  36344  jm2.19lem4  36577  jm2.19  36578  jm2.26a  36585  jm2.26  36587  hbtlem2  36713  fnchoice  38211  stoweidlem42  38935  stoweidlem59  38952  fourierdlem42  39042  clwlksfclwwlk  41269  umgr3cyclex  41350