Theorem syl121anc 1377

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

Hypotheses

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

Assertion

Ref	Expression
syl121anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl121anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1373	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl122anc  1381  fsnunf2  7126  tfisi  7799  fnsuppeq0  8132  ttrclss  9635  ttrclselem2  9641  axdc4lem  10368  div32d  11941  div13d  11942  expdivd  14085  swrdsbslen  14589  sumeven  16316  sumodd  16317  pcqmul  16783  pcid  16803  pcneg  16804  pc2dvds  16809  pcz  16811  pcaddlem  16818  pcadd  16819  pcmpt2  16823  pcbc  16830  qexpz  16831  expnprm  16832  sylow1lem1  19495  omndmul3  20031  ringurd  20088  lspsneleq  21040  lspsneq  21047  lspfixed  21053  frlmsslss2  21700  chmatval  22732  chpmat1dlem  22738  chpdmatlem2  22742  ucncn  24188  ucnextcn  24207  ssblex  24332  prdsxmslem2  24433  ncvs1  25073  voliunlem1  25467  deg1mul3le  26038  deg1pw  26042  fta1blem  26092  bcmono  27204  dchrisum0flblem1  27435  dchrisum0flblem2  27436  pntibndlem1  27516  pntlemr  27529  nosupbnd1  27642  noinfbnd1  27657  noetalem1  27669  slerec  27748  finsumvtxdg2sstep  29513  umgr3cyclex  30145  nv1  30637  resf1o  32686  symgcntz  33040  cycpmco2lem6  33086  tocyccntz  33099  deg1vr  33534  rtelextdg2lem  33692  measun  34177  measvuni  34180  measunl  34182  btwnconn1lem14  36073  segcon2  36078  seglelin  36089  neibastop3  36335  upixp  37708  fdc  37724  eqlkr3  39079  lkrshp  39083  lfl1dim  39099  lfl1dim2N  39100  eqlkr4  39143  2llnneN  39388  3dim2  39447  4atlem3  39575  4atlem11  39588  4atlem12  39591  pexmidlem4N  39952  lhp2at0nle  40014  lhple  40021  ltrnideq  40154  cdlemd9  40185  cdleme0ex2N  40203  cdleme0moN  40204  cdleme11a  40239  cdleme30a  40357  cdlemefs32sn1aw  40393  cdleme43fsv1snlem  40399  cdlemefs31fv1  40403  cdlemefs45eN  40410  cdleme41sn3a  40412  cdleme35h  40435  cdleme36a  40439  cdleme40m  40446  cdleme40n  40447  cdleme41sn3aw  40453  cdleme42h  40461  cdleme42k  40463  cdleme42mN  40466  cdleme43cN  40470  cdleme17d3  40475  cdleme48fvg  40479  cdlemeg47rv2  40489  cdlemeg46c  40492  cdlemeg46sfg  40499  cdlemeg46rjgN  40501  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemeg46gfv  40509  cdlemeg46gfre  40511  cdlemeg49lebilem  40518  cdleme50trn2  40530  cdlemg2kq  40581  cdlemb3  40585  cdlemg4f  40594  cdlemg9a  40611  cdlemg9b  40612  cdlemg9  40613  cdlemg11aq  40617  cdlemg12a  40622  cdlemg12b  40623  cdlemg12c  40624  cdlemg12d  40625  cdlemg12f  40627  cdlemg12g  40628  cdlemg12  40629  cdlemg13a  40630  cdlemg16  40636  cdlemg17e  40644  cdlemg17f  40645  cdlemg17g  40646  cdlemg17ir  40649  cdlemg17  40656  cdlemg18b  40658  cdlemg18c  40659  cdlemg33e  40689  trlcoabs2N  40701  trlcocnvat  40703  trlcolem  40705  trlco  40706  cdlemg44  40712  cdlemg47  40715  ltrncom  40717  tendococl  40751  tendoplcl  40760  tendoplcom  40761  tendoplass  40762  tendodi1  40763  tendodi2  40764  tendo0pl  40770  tendoipl  40776  cdlemh1  40794  cdlemi2  40798  tendo0mul  40805  tendo0mulr  40806  cdlemk2  40811  cdlemk3  40812  cdlemk4  40813  cdlemk6  40816  cdlemk8  40817  cdlemk12  40829  cdlemkole  40832  cdlemk14  40833  cdlemk15  40834  cdlemk5u  40840  cdlemk6u  40841  cdlemk12u  40851  cdlemkfid1N  40900  cdlemk19x  40922  cdlemk48  40929  cdlemk53a  40934  cdlemk56  40950  cdleml2N  40956  cdleml3N  40957  cdleml6  40960  cdleml7  40961  dva1dim  40964  dia2dimlem4  41046  dvhlveclem  41087  doca2N  41105  djajN  41116  cdlemn2a  41175  cdlemn3  41176  dihordlem6  41192  dihord5apre  41241  dihglbcpreN  41279  dihmeetcN  41281  dihmeetbN  41282  dihmeetlem10N  41295  dihmeetlem12N  41297  dihmeetlem15N  41300  dihmeetALTN  41306  dih1dimatlem0  41307  dihjatcclem3  41399  dihjatcclem4  41400  mapdpglem22  41672  hdmap14lem1a  41845  eldioph2b  42736  jm2.19lem4  42965  jm2.19  42966  jm2.26a  42973  jm2.26  42975  hbtlem2  43097  fnchoice  45007  stoweidlem42  46024  stoweidlem59  46041  fourierdlem42  46131  zplusmodne  47328  minusmod5ne  47334