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  7132  tfisi  7801  fnsuppeq0  8134  ttrclss  9629  ttrclselem2  9635  axdc4lem  10365  div32d  11940  div13d  11941  expdivd  14083  swrdsbslen  14588  sumeven  16314  sumodd  16315  pcqmul  16781  pcid  16801  pcneg  16802  pc2dvds  16807  pcz  16809  pcaddlem  16816  pcadd  16817  pcmpt2  16821  pcbc  16828  qexpz  16829  expnprm  16830  sylow1lem1  19527  omndmul3  20063  ringurd  20120  lspsneleq  21070  lspsneq  21077  lspfixed  21083  frlmsslss2  21730  chmatval  22773  chpmat1dlem  22779  chpdmatlem2  22783  ucncn  24228  ucnextcn  24247  ssblex  24372  prdsxmslem2  24473  ncvs1  25113  voliunlem1  25507  deg1mul3le  26078  deg1pw  26082  fta1blem  26132  bcmono  27244  dchrisum0flblem1  27475  dchrisum0flblem2  27476  pntibndlem1  27556  pntlemr  27569  nosupbnd1  27682  noinfbnd1  27697  noetalem1  27709  lesrec  27795  finsumvtxdg2sstep  29623  umgr3cyclex  30258  nv1  30750  resf1o  32809  symgcntz  33167  cycpmco2lem6  33213  tocyccntz  33226  deg1vr  33673  rtelextdg2lem  33883  measun  34368  measvuni  34371  measunl  34373  btwnconn1lem14  36294  segcon2  36299  seglelin  36310  neibastop3  36556  upixp  37926  fdc  37942  eqlkr3  39357  lkrshp  39361  lfl1dim  39377  lfl1dim2N  39378  eqlkr4  39421  2llnneN  39665  3dim2  39724  4atlem3  39852  4atlem11  39865  4atlem12  39868  pexmidlem4N  40229  lhp2at0nle  40291  lhple  40298  ltrnideq  40431  cdlemd9  40462  cdleme0ex2N  40480  cdleme0moN  40481  cdleme11a  40516  cdleme30a  40634  cdlemefs32sn1aw  40670  cdleme43fsv1snlem  40676  cdlemefs31fv1  40680  cdlemefs45eN  40687  cdleme41sn3a  40689  cdleme35h  40712  cdleme36a  40716  cdleme40m  40723  cdleme40n  40724  cdleme41sn3aw  40730  cdleme42h  40738  cdleme42k  40740  cdleme42mN  40743  cdleme43cN  40747  cdleme17d3  40752  cdleme48fvg  40756  cdlemeg47rv2  40766  cdlemeg46c  40769  cdlemeg46sfg  40776  cdlemeg46rjgN  40778  cdlemeg46rgv  40784  cdlemeg46req  40785  cdlemeg46gfv  40786  cdlemeg46gfre  40788  cdlemeg49lebilem  40795  cdleme50trn2  40807  cdlemg2kq  40858  cdlemb3  40862  cdlemg4f  40871  cdlemg9a  40888  cdlemg9b  40889  cdlemg9  40890  cdlemg11aq  40894  cdlemg12a  40899  cdlemg12b  40900  cdlemg12c  40901  cdlemg12d  40902  cdlemg12f  40904  cdlemg12g  40905  cdlemg12  40906  cdlemg13a  40907  cdlemg16  40913  cdlemg17e  40921  cdlemg17f  40922  cdlemg17g  40923  cdlemg17ir  40926  cdlemg17  40933  cdlemg18b  40935  cdlemg18c  40936  cdlemg33e  40966  trlcoabs2N  40978  trlcocnvat  40980  trlcolem  40982  trlco  40983  cdlemg44  40989  cdlemg47  40992  ltrncom  40994  tendococl  41028  tendoplcl  41037  tendoplcom  41038  tendoplass  41039  tendodi1  41040  tendodi2  41041  tendo0pl  41047  tendoipl  41053  cdlemh1  41071  cdlemi2  41075  tendo0mul  41082  tendo0mulr  41083  cdlemk2  41088  cdlemk3  41089  cdlemk4  41090  cdlemk6  41093  cdlemk8  41094  cdlemk12  41106  cdlemkole  41109  cdlemk14  41110  cdlemk15  41111  cdlemk5u  41117  cdlemk6u  41118  cdlemk12u  41128  cdlemkfid1N  41177  cdlemk19x  41199  cdlemk48  41206  cdlemk53a  41211  cdlemk56  41227  cdleml2N  41233  cdleml3N  41234  cdleml6  41237  cdleml7  41238  dva1dim  41241  dia2dimlem4  41323  dvhlveclem  41364  doca2N  41382  djajN  41393  cdlemn2a  41452  cdlemn3  41453  dihordlem6  41469  dihord5apre  41518  dihglbcpreN  41556  dihmeetcN  41558  dihmeetbN  41559  dihmeetlem10N  41572  dihmeetlem12N  41574  dihmeetlem15N  41577  dihmeetALTN  41583  dih1dimatlem0  41584  dihjatcclem3  41676  dihjatcclem4  41677  mapdpglem22  41949  hdmap14lem1a  42122  eldioph2b  43001  jm2.19lem4  43230  jm2.19  43231  jm2.26a  43238  jm2.26  43240  hbtlem2  43362  fnchoice  45270  stoweidlem42  46282  stoweidlem59  46299  fourierdlem42  46389  zplusmodne  47585  minusmod5ne  47591