Theorem syl121anc 1331

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl121anc.5	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl121anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl121anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 554	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1326	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl122anc  1335  disjxiunOLD  4650  fsnunf2  6452  tfisi  7058  fnsuppeq0  7323  axdc4lem  9277  div32d  10824  div13d  10825  expdivd  13022  swrdsbslen  13448  sumeven  15110  sumodd  15111  pcqmul  15558  pcid  15577  pcneg  15578  pc2dvds  15583  pcz  15585  pcaddlem  15592  pcadd  15593  pcmpt2  15597  pcbc  15604  qexpz  15605  expnprm  15606  sylow1lem1  18013  lspsneleq  19115  lspsneq  19122  lspfixed  19128  frlmsslss2  20114  chmatval  20634  chpmat1dlem  20640  chpdmatlem2  20644  ucncn  22089  ucnextcn  22108  ssblex  22233  prdsxmslem2  22334  ncvs1  22957  voliunlem1  23318  deg1mul3le  23876  deg1pw  23880  fta1blem  23928  bcmono  25002  dchrisum0flblem1  25197  dchrisum0flblem2  25198  pntibndlem1  25278  pntlemr  25291  finsumvtxdg2sstep  26445  clwlksfclwwlk  26962  umgr3cyclex  27043  nv1  27530  resf1o  29505  omndmul3  29713  rngurd  29788  measun  30274  measvuni  30277  measunl  30279  nosupbnd1  31860  slerec  31923  btwnconn1lem14  32207  segcon2  32212  seglelin  32223  neibastop3  32357  upixp  33524  fdc  33541  eqlkr3  34388  lkrshp  34392  lfl1dim  34408  lfl1dim2N  34409  eqlkr4  34452  2llnneN  34695  3dim2  34754  4atlem3  34882  4atlem11  34895  4atlem12  34898  pexmidlem4N  35259  lhp2at0nle  35321  lhple  35328  ltrnideq  35462  cdlemd9  35493  cdleme0ex2N  35511  cdleme0moN  35512  cdleme11a  35547  cdleme30a  35666  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdlemefs31fv1  35712  cdlemefs45eN  35719  cdleme41sn3a  35721  cdleme35h  35744  cdleme36a  35748  cdleme40m  35755  cdleme40n  35756  cdleme41sn3aw  35762  cdleme42h  35770  cdleme42k  35772  cdleme42mN  35775  cdleme43cN  35779  cdleme17d3  35784  cdleme48fvg  35788  cdlemeg47rv2  35798  cdlemeg46c  35801  cdlemeg46sfg  35808  cdlemeg46rjgN  35810  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemeg46gfv  35818  cdlemeg46gfre  35820  cdlemeg49lebilem  35827  cdleme50trn2  35839  cdlemg2kq  35890  cdlemb3  35894  cdlemg4f  35903  cdlemg9a  35920  cdlemg9b  35921  cdlemg9  35922  cdlemg11aq  35926  cdlemg12a  35931  cdlemg12b  35932  cdlemg12c  35933  cdlemg12d  35934  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg16  35945  cdlemg17e  35953  cdlemg17f  35954  cdlemg17g  35955  cdlemg17ir  35958  cdlemg17  35965  cdlemg18b  35967  cdlemg18c  35968  cdlemg33e  35998  trlcoabs2N  36010  trlcocnvat  36012  trlcolem  36014  trlco  36015  cdlemg44  36021  cdlemg47  36024  ltrncom  36026  tendococl  36060  tendoplcl  36069  tendoplcom  36070  tendoplass  36071  tendodi1  36072  tendodi2  36073  tendo0pl  36079  tendoipl  36085  cdlemh1  36103  cdlemi2  36107  tendo0mul  36114  tendo0mulr  36115  cdlemk2  36120  cdlemk3  36121  cdlemk4  36122  cdlemk6  36125  cdlemk8  36126  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk5u  36149  cdlemk6u  36150  cdlemk12u  36160  cdlemkfid1N  36209  cdlemk19x  36231  cdlemk48  36238  cdlemk53a  36243  cdlemk56  36259  cdleml2N  36265  cdleml3N  36266  cdleml6  36269  cdleml7  36270  dva1dim  36273  dia2dimlem4  36356  dvhlveclem  36397  doca2N  36415  djajN  36426  cdlemn2a  36485  cdlemn3  36486  dihordlem6  36502  dihord5apre  36551  dihglbcpreN  36589  dihmeetcN  36591  dihmeetbN  36592  dihmeetlem10N  36605  dihmeetlem12N  36607  dihmeetlem15N  36610  dihmeetALTN  36616  dih1dimatlem0  36617  dihjatcclem3  36709  dihjatcclem4  36710  mapdpglem22  36982  hdmap14lem1a  37158  eldioph2b  37326  jm2.19lem4  37559  jm2.19  37560  jm2.26a  37567  jm2.26  37569  hbtlem2  37694  fnchoice  39188  stoweidlem42  40259  stoweidlem59  40276  fourierdlem42  40366