Theorem syl121anc 1400

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl122anc  1404  fsnunf2  7185  tfisi  7855  fnsuppeq0  8188  ttrclss  9689  ttrclselem2  9695  axdc4lem  10439  div32d  12014  div13d  12015  expdivd  14196  swrdsbslen  14702  sumeven  16445  sumodd  16446  pcqmul  16913  pcid  16933  pcneg  16934  pc2dvds  16939  pcz  16941  pcaddlem  16948  pcadd  16949  pcmpt2  16953  pcbc  16960  qexpz  16961  expnprm  16962  sylow1lem1  19668  omndmul3  20204  ringurd  20267  lspsneleq  21217  lspsneq  21224  lspfixed  21230  frlmsslss2  21894  chmatval  22955  chpmat1dlem  22961  chpdmatlem2  22965  ucncn  24410  ucnextcn  24429  ssblex  24554  prdsxmslem2  24655  ncvs1  25285  voliunlem1  25678  deg1mul3le  26243  deg1pw  26247  fta1blem  26297  bcmono  27407  dchrisum0flblem1  27638  dchrisum0flblem2  27639  pntibndlem1  27719  pntlemr  27732  nosupbnd1  27844  noinfbnd1  27859  noetalem1  27871  lesrec  27958  finsumvtxdg2sstep  29840  umgr3cyclex  30475  nv1  30968  resf1o  33016  symgcntz  33346  cycpmco2lem6  33392  tocyccntz  33405  deg1vr  33827  rtelextdg2lem  34061  measun  34546  measvuni  34549  measunl  34551  btwnconn1lem14  36491  segcon2  36496  seglelin  36507  neibastop3  36762  upixp  38268  fdc  38284  eqlkr3  39765  lkrshp  39769  lfl1dim  39785  lfl1dim2N  39786  eqlkr4  39829  2llnneN  40073  3dim2  40132  4atlem3  40260  4atlem11  40273  4atlem12  40276  pexmidlem4N  40637  lhp2at0nle  40699  lhple  40706  ltrnideq  40839  cdlemd9  40870  cdleme0ex2N  40888  cdleme0moN  40889  cdleme11a  40924  cdleme30a  41042  cdlemefs32sn1aw  41078  cdleme43fsv1snlem  41084  cdlemefs31fv1  41088  cdlemefs45eN  41095  cdleme41sn3a  41097  cdleme35h  41120  cdleme36a  41124  cdleme40m  41131  cdleme40n  41132  cdleme41sn3aw  41138  cdleme42h  41146  cdleme42k  41148  cdleme42mN  41151  cdleme43cN  41155  cdleme17d3  41160  cdleme48fvg  41164  cdlemeg47rv2  41174  cdlemeg46c  41177  cdlemeg46sfg  41184  cdlemeg46rjgN  41186  cdlemeg46rgv  41192  cdlemeg46req  41193  cdlemeg46gfv  41194  cdlemeg46gfre  41196  cdlemeg49lebilem  41203  cdleme50trn2  41215  cdlemg2kq  41266  cdlemb3  41270  cdlemg4f  41279  cdlemg9a  41296  cdlemg9b  41297  cdlemg9  41298  cdlemg11aq  41302  cdlemg12a  41307  cdlemg12b  41308  cdlemg12c  41309  cdlemg12d  41310  cdlemg12f  41312  cdlemg12g  41313  cdlemg12  41314  cdlemg13a  41315  cdlemg16  41321  cdlemg17e  41329  cdlemg17f  41330  cdlemg17g  41331  cdlemg17ir  41334  cdlemg17  41341  cdlemg18b  41343  cdlemg18c  41344  cdlemg33e  41374  trlcoabs2N  41386  trlcocnvat  41388  trlcolem  41390  trlco  41391  cdlemg44  41397  cdlemg47  41400  ltrncom  41402  tendococl  41436  tendoplcl  41445  tendoplcom  41446  tendoplass  41447  tendodi1  41448  tendodi2  41449  tendo0pl  41455  tendoipl  41461  cdlemh1  41479  cdlemi2  41483  tendo0mul  41490  tendo0mulr  41491  cdlemk2  41496  cdlemk3  41497  cdlemk4  41498  cdlemk6  41501  cdlemk8  41502  cdlemk12  41514  cdlemkole  41517  cdlemk14  41518  cdlemk15  41519  cdlemk5u  41525  cdlemk6u  41526  cdlemk12u  41536  cdlemkfid1N  41585  cdlemk19x  41607  cdlemk48  41614  cdlemk53a  41619  cdlemk56  41635  cdleml2N  41641  cdleml3N  41642  cdleml6  41645  cdleml7  41646  dva1dim  41649  dia2dimlem4  41731  dvhlveclem  41772  doca2N  41790  djajN  41801  cdlemn2a  41860  cdlemn3  41861  dihordlem6  41877  dihord5apre  41926  dihglbcpreN  41964  dihmeetcN  41966  dihmeetbN  41967  dihmeetlem10N  41980  dihmeetlem12N  41982  dihmeetlem15N  41985  dihmeetALTN  41991  dih1dimatlem0  41992  dihjatcclem3  42084  dihjatcclem4  42085  mapdpglem22  42357  hdmap14lem1a  42530  eldioph2b  43386  jm2.19lem4  43611  jm2.19  43612  jm2.26a  43619  jm2.26  43621  hbtlem2  43743  fnchoice  45641  stoweidlem42  46648  stoweidlem59  46665  fourierdlem42  46755  zplusmodne  47975  minusmod5ne  47981