Theorem syl121anc 1374

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 512	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1370	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl122anc  1378  fsnunf2  7095  tfisi  7748  fnsuppeq0  8053  ttrclss  9546  ttrclselem2  9552  axdc4lem  10281  div32d  11844  div13d  11845  expdivd  13948  swrdsbslen  14446  sumeven  16165  sumodd  16166  pcqmul  16621  pcid  16641  pcneg  16642  pc2dvds  16647  pcz  16649  pcaddlem  16656  pcadd  16657  pcmpt2  16661  pcbc  16668  qexpz  16669  expnprm  16670  sylow1lem1  19270  lspsneleq  20448  lspsneq  20455  lspfixed  20461  frlmsslss2  21053  chmatval  22049  chpmat1dlem  22055  chpdmatlem2  22059  ucncn  23508  ucnextcn  23527  ssblex  23652  prdsxmslem2  23756  ncvs1  24392  voliunlem1  24785  deg1mul3le  25352  deg1pw  25356  fta1blem  25404  bcmono  26496  dchrisum0flblem1  26727  dchrisum0flblem2  26728  pntibndlem1  26808  pntlemr  26821  finsumvtxdg2sstep  28024  umgr3cyclex  28655  nv1  29145  resf1o  31173  omndmul3  31447  symgcntz  31462  cycpmco2lem6  31506  tocyccntz  31519  rngurd  31590  measun  32285  measvuni  32288  measunl  32290  nosupbnd1  33978  noinfbnd1  33993  noetalem1  34005  slerec  34074  btwnconn1lem14  34463  segcon2  34468  seglelin  34479  neibastop3  34612  upixp  35947  fdc  35963  eqlkr3  37327  lkrshp  37331  lfl1dim  37347  lfl1dim2N  37348  eqlkr4  37391  2llnneN  37635  3dim2  37694  4atlem3  37822  4atlem11  37835  4atlem12  37838  pexmidlem4N  38199  lhp2at0nle  38261  lhple  38268  ltrnideq  38401  cdlemd9  38432  cdleme0ex2N  38450  cdleme0moN  38451  cdleme11a  38486  cdleme30a  38604  cdlemefs32sn1aw  38640  cdleme43fsv1snlem  38646  cdlemefs31fv1  38650  cdlemefs45eN  38657  cdleme41sn3a  38659  cdleme35h  38682  cdleme36a  38686  cdleme40m  38693  cdleme40n  38694  cdleme41sn3aw  38700  cdleme42h  38708  cdleme42k  38710  cdleme42mN  38713  cdleme43cN  38717  cdleme17d3  38722  cdleme48fvg  38726  cdlemeg47rv2  38736  cdlemeg46c  38739  cdlemeg46sfg  38746  cdlemeg46rjgN  38748  cdlemeg46rgv  38754  cdlemeg46req  38755  cdlemeg46gfv  38756  cdlemeg46gfre  38758  cdlemeg49lebilem  38765  cdleme50trn2  38777  cdlemg2kq  38828  cdlemb3  38832  cdlemg4f  38841  cdlemg9a  38858  cdlemg9b  38859  cdlemg9  38860  cdlemg11aq  38864  cdlemg12a  38869  cdlemg12b  38870  cdlemg12c  38871  cdlemg12d  38872  cdlemg12f  38874  cdlemg12g  38875  cdlemg12  38876  cdlemg13a  38877  cdlemg16  38883  cdlemg17e  38891  cdlemg17f  38892  cdlemg17g  38893  cdlemg17ir  38896  cdlemg17  38903  cdlemg18b  38905  cdlemg18c  38906  cdlemg33e  38936  trlcoabs2N  38948  trlcocnvat  38950  trlcolem  38952  trlco  38953  cdlemg44  38959  cdlemg47  38962  ltrncom  38964  tendococl  38998  tendoplcl  39007  tendoplcom  39008  tendoplass  39009  tendodi1  39010  tendodi2  39011  tendo0pl  39017  tendoipl  39023  cdlemh1  39041  cdlemi2  39045  tendo0mul  39052  tendo0mulr  39053  cdlemk2  39058  cdlemk3  39059  cdlemk4  39060  cdlemk6  39063  cdlemk8  39064  cdlemk12  39076  cdlemkole  39079  cdlemk14  39080  cdlemk15  39081  cdlemk5u  39087  cdlemk6u  39088  cdlemk12u  39098  cdlemkfid1N  39147  cdlemk19x  39169  cdlemk48  39176  cdlemk53a  39181  cdlemk56  39197  cdleml2N  39203  cdleml3N  39204  cdleml6  39207  cdleml7  39208  dva1dim  39211  dia2dimlem4  39293  dvhlveclem  39334  doca2N  39352  djajN  39363  cdlemn2a  39422  cdlemn3  39423  dihordlem6  39439  dihord5apre  39488  dihglbcpreN  39526  dihmeetcN  39528  dihmeetbN  39529  dihmeetlem10N  39542  dihmeetlem12N  39544  dihmeetlem15N  39547  dihmeetALTN  39553  dih1dimatlem0  39554  dihjatcclem3  39646  dihjatcclem4  39647  mapdpglem22  39919  hdmap14lem1a  40092  eldioph2b  40795  jm2.19lem4  41025  jm2.19  41026  jm2.26a  41033  jm2.26  41035  hbtlem2  41160  fnchoice  42800  stoweidlem42  43827  stoweidlem59  43844  fourierdlem42  43934