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  7795  fnsuppeq0  8128  ttrclss  9617  ttrclselem2  9623  axdc4lem  10353  div32d  11927  div13d  11928  expdivd  14069  swrdsbslen  14574  sumeven  16300  sumodd  16301  pcqmul  16767  pcid  16787  pcneg  16788  pc2dvds  16793  pcz  16795  pcaddlem  16802  pcadd  16803  pcmpt2  16807  pcbc  16814  qexpz  16815  expnprm  16816  sylow1lem1  19512  omndmul3  20048  ringurd  20105  lspsneleq  21054  lspsneq  21061  lspfixed  21067  frlmsslss2  21714  chmatval  22745  chpmat1dlem  22751  chpdmatlem2  22755  ucncn  24200  ucnextcn  24219  ssblex  24344  prdsxmslem2  24445  ncvs1  25085  voliunlem1  25479  deg1mul3le  26050  deg1pw  26054  fta1blem  26104  bcmono  27216  dchrisum0flblem1  27447  dchrisum0flblem2  27448  pntibndlem1  27528  pntlemr  27541  nosupbnd1  27654  noinfbnd1  27669  noetalem1  27681  slerec  27761  finsumvtxdg2sstep  29530  umgr3cyclex  30165  nv1  30657  resf1o  32717  symgcntz  33061  cycpmco2lem6  33107  tocyccntz  33120  deg1vr  33560  rtelextdg2lem  33760  measun  34245  measvuni  34248  measunl  34250  btwnconn1lem14  36165  segcon2  36170  seglelin  36181  neibastop3  36427  upixp  37789  fdc  37805  eqlkr3  39220  lkrshp  39224  lfl1dim  39240  lfl1dim2N  39241  eqlkr4  39284  2llnneN  39528  3dim2  39587  4atlem3  39715  4atlem11  39728  4atlem12  39731  pexmidlem4N  40092  lhp2at0nle  40154  lhple  40161  ltrnideq  40294  cdlemd9  40325  cdleme0ex2N  40343  cdleme0moN  40344  cdleme11a  40379  cdleme30a  40497  cdlemefs32sn1aw  40533  cdleme43fsv1snlem  40539  cdlemefs31fv1  40543  cdlemefs45eN  40550  cdleme41sn3a  40552  cdleme35h  40575  cdleme36a  40579  cdleme40m  40586  cdleme40n  40587  cdleme41sn3aw  40593  cdleme42h  40601  cdleme42k  40603  cdleme42mN  40606  cdleme43cN  40610  cdleme17d3  40615  cdleme48fvg  40619  cdlemeg47rv2  40629  cdlemeg46c  40632  cdlemeg46sfg  40639  cdlemeg46rjgN  40641  cdlemeg46rgv  40647  cdlemeg46req  40648  cdlemeg46gfv  40649  cdlemeg46gfre  40651  cdlemeg49lebilem  40658  cdleme50trn2  40670  cdlemg2kq  40721  cdlemb3  40725  cdlemg4f  40734  cdlemg9a  40751  cdlemg9b  40752  cdlemg9  40753  cdlemg11aq  40757  cdlemg12a  40762  cdlemg12b  40763  cdlemg12c  40764  cdlemg12d  40765  cdlemg12f  40767  cdlemg12g  40768  cdlemg12  40769  cdlemg13a  40770  cdlemg16  40776  cdlemg17e  40784  cdlemg17f  40785  cdlemg17g  40786  cdlemg17ir  40789  cdlemg17  40796  cdlemg18b  40798  cdlemg18c  40799  cdlemg33e  40829  trlcoabs2N  40841  trlcocnvat  40843  trlcolem  40845  trlco  40846  cdlemg44  40852  cdlemg47  40855  ltrncom  40857  tendococl  40891  tendoplcl  40900  tendoplcom  40901  tendoplass  40902  tendodi1  40903  tendodi2  40904  tendo0pl  40910  tendoipl  40916  cdlemh1  40934  cdlemi2  40938  tendo0mul  40945  tendo0mulr  40946  cdlemk2  40951  cdlemk3  40952  cdlemk4  40953  cdlemk6  40956  cdlemk8  40957  cdlemk12  40969  cdlemkole  40972  cdlemk14  40973  cdlemk15  40974  cdlemk5u  40980  cdlemk6u  40981  cdlemk12u  40991  cdlemkfid1N  41040  cdlemk19x  41062  cdlemk48  41069  cdlemk53a  41074  cdlemk56  41090  cdleml2N  41096  cdleml3N  41097  cdleml6  41100  cdleml7  41101  dva1dim  41104  dia2dimlem4  41186  dvhlveclem  41227  doca2N  41245  djajN  41256  cdlemn2a  41315  cdlemn3  41316  dihordlem6  41332  dihord5apre  41381  dihglbcpreN  41419  dihmeetcN  41421  dihmeetbN  41422  dihmeetlem10N  41435  dihmeetlem12N  41437  dihmeetlem15N  41440  dihmeetALTN  41446  dih1dimatlem0  41447  dihjatcclem3  41539  dihjatcclem4  41540  mapdpglem22  41812  hdmap14lem1a  41985  eldioph2b  42880  jm2.19lem4  43109  jm2.19  43110  jm2.26a  43117  jm2.26  43119  hbtlem2  43241  fnchoice  45150  stoweidlem42  46164  stoweidlem59  46181  fourierdlem42  46271  zplusmodne  47467  minusmod5ne  47473