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  7163  tfisi  7838  fnsuppeq0  8174  ttrclss  9680  ttrclselem2  9686  axdc4lem  10415  div32d  11988  div13d  11989  expdivd  14132  swrdsbslen  14636  sumeven  16364  sumodd  16365  pcqmul  16831  pcid  16851  pcneg  16852  pc2dvds  16857  pcz  16859  pcaddlem  16866  pcadd  16867  pcmpt2  16871  pcbc  16878  qexpz  16879  expnprm  16880  sylow1lem1  19535  ringurd  20101  lspsneleq  21032  lspsneq  21039  lspfixed  21045  frlmsslss2  21691  chmatval  22723  chpmat1dlem  22729  chpdmatlem2  22733  ucncn  24179  ucnextcn  24198  ssblex  24323  prdsxmslem2  24424  ncvs1  25064  voliunlem1  25458  deg1mul3le  26029  deg1pw  26033  fta1blem  26083  bcmono  27195  dchrisum0flblem1  27426  dchrisum0flblem2  27427  pntibndlem1  27507  pntlemr  27520  nosupbnd1  27633  noinfbnd1  27648  noetalem1  27660  slerec  27738  finsumvtxdg2sstep  29484  umgr3cyclex  30119  nv1  30611  resf1o  32660  omndmul3  33034  symgcntz  33049  cycpmco2lem6  33095  tocyccntz  33108  deg1vr  33565  rtelextdg2lem  33723  measun  34208  measvuni  34211  measunl  34213  btwnconn1lem14  36095  segcon2  36100  seglelin  36111  neibastop3  36357  upixp  37730  fdc  37746  eqlkr3  39101  lkrshp  39105  lfl1dim  39121  lfl1dim2N  39122  eqlkr4  39165  2llnneN  39410  3dim2  39469  4atlem3  39597  4atlem11  39610  4atlem12  39613  pexmidlem4N  39974  lhp2at0nle  40036  lhple  40043  ltrnideq  40176  cdlemd9  40207  cdleme0ex2N  40225  cdleme0moN  40226  cdleme11a  40261  cdleme30a  40379  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdlemefs31fv1  40425  cdlemefs45eN  40432  cdleme41sn3a  40434  cdleme35h  40457  cdleme36a  40461  cdleme40m  40468  cdleme40n  40469  cdleme41sn3aw  40475  cdleme42h  40483  cdleme42k  40485  cdleme42mN  40488  cdleme43cN  40492  cdleme17d3  40497  cdleme48fvg  40501  cdlemeg47rv2  40511  cdlemeg46c  40514  cdlemeg46sfg  40521  cdlemeg46rjgN  40523  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemeg46gfv  40531  cdlemeg46gfre  40533  cdlemeg49lebilem  40540  cdleme50trn2  40552  cdlemg2kq  40603  cdlemb3  40607  cdlemg4f  40616  cdlemg9a  40633  cdlemg9b  40634  cdlemg9  40635  cdlemg11aq  40639  cdlemg12a  40644  cdlemg12b  40645  cdlemg12c  40646  cdlemg12d  40647  cdlemg12f  40649  cdlemg12g  40650  cdlemg12  40651  cdlemg13a  40652  cdlemg16  40658  cdlemg17e  40666  cdlemg17f  40667  cdlemg17g  40668  cdlemg17ir  40671  cdlemg17  40678  cdlemg18b  40680  cdlemg18c  40681  cdlemg33e  40711  trlcoabs2N  40723  trlcocnvat  40725  trlcolem  40727  trlco  40728  cdlemg44  40734  cdlemg47  40737  ltrncom  40739  tendococl  40773  tendoplcl  40782  tendoplcom  40783  tendoplass  40784  tendodi1  40785  tendodi2  40786  tendo0pl  40792  tendoipl  40798  cdlemh1  40816  cdlemi2  40820  tendo0mul  40827  tendo0mulr  40828  cdlemk2  40833  cdlemk3  40834  cdlemk4  40835  cdlemk6  40838  cdlemk8  40839  cdlemk12  40851  cdlemkole  40854  cdlemk14  40855  cdlemk15  40856  cdlemk5u  40862  cdlemk6u  40863  cdlemk12u  40873  cdlemkfid1N  40922  cdlemk19x  40944  cdlemk48  40951  cdlemk53a  40956  cdlemk56  40972  cdleml2N  40978  cdleml3N  40979  cdleml6  40982  cdleml7  40983  dva1dim  40986  dia2dimlem4  41068  dvhlveclem  41109  doca2N  41127  djajN  41138  cdlemn2a  41197  cdlemn3  41198  dihordlem6  41214  dihord5apre  41263  dihglbcpreN  41301  dihmeetcN  41303  dihmeetbN  41304  dihmeetlem10N  41317  dihmeetlem12N  41319  dihmeetlem15N  41322  dihmeetALTN  41328  dih1dimatlem0  41329  dihjatcclem3  41421  dihjatcclem4  41422  mapdpglem22  41694  hdmap14lem1a  41867  eldioph2b  42758  jm2.19lem4  42988  jm2.19  42989  jm2.26a  42996  jm2.26  42998  hbtlem2  43120  fnchoice  45030  stoweidlem42  46047  stoweidlem59  46064  fourierdlem42  46154  zplusmodne  47348  minusmod5ne  47354