Theorem syl121anc 1378

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 1374	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl122anc  1382  fsnunf2  7142  tfisi  7811  fnsuppeq0  8144  ttrclss  9641  ttrclselem2  9647  axdc4lem  10377  div32d  11952  div13d  11953  expdivd  14095  swrdsbslen  14600  sumeven  16326  sumodd  16327  pcqmul  16793  pcid  16813  pcneg  16814  pc2dvds  16819  pcz  16821  pcaddlem  16828  pcadd  16829  pcmpt2  16833  pcbc  16840  qexpz  16841  expnprm  16842  sylow1lem1  19539  omndmul3  20075  ringurd  20132  lspsneleq  21082  lspsneq  21089  lspfixed  21095  frlmsslss2  21742  chmatval  22785  chpmat1dlem  22791  chpdmatlem2  22795  ucncn  24240  ucnextcn  24259  ssblex  24384  prdsxmslem2  24485  ncvs1  25125  voliunlem1  25519  deg1mul3le  26090  deg1pw  26094  fta1blem  26144  bcmono  27256  dchrisum0flblem1  27487  dchrisum0flblem2  27488  pntibndlem1  27568  pntlemr  27581  nosupbnd1  27694  noinfbnd1  27709  noetalem1  27721  lesrec  27807  finsumvtxdg2sstep  29635  umgr3cyclex  30270  nv1  30762  resf1o  32819  symgcntz  33178  cycpmco2lem6  33224  tocyccntz  33237  deg1vr  33684  rtelextdg2lem  33903  measun  34388  measvuni  34391  measunl  34393  btwnconn1lem14  36313  segcon2  36318  seglelin  36329  neibastop3  36575  upixp  37974  fdc  37990  eqlkr3  39471  lkrshp  39475  lfl1dim  39491  lfl1dim2N  39492  eqlkr4  39535  2llnneN  39779  3dim2  39838  4atlem3  39966  4atlem11  39979  4atlem12  39982  pexmidlem4N  40343  lhp2at0nle  40405  lhple  40412  ltrnideq  40545  cdlemd9  40576  cdleme0ex2N  40594  cdleme0moN  40595  cdleme11a  40630  cdleme30a  40748  cdlemefs32sn1aw  40784  cdleme43fsv1snlem  40790  cdlemefs31fv1  40794  cdlemefs45eN  40801  cdleme41sn3a  40803  cdleme35h  40826  cdleme36a  40830  cdleme40m  40837  cdleme40n  40838  cdleme41sn3aw  40844  cdleme42h  40852  cdleme42k  40854  cdleme42mN  40857  cdleme43cN  40861  cdleme17d3  40866  cdleme48fvg  40870  cdlemeg47rv2  40880  cdlemeg46c  40883  cdlemeg46sfg  40890  cdlemeg46rjgN  40892  cdlemeg46rgv  40898  cdlemeg46req  40899  cdlemeg46gfv  40900  cdlemeg46gfre  40902  cdlemeg49lebilem  40909  cdleme50trn2  40921  cdlemg2kq  40972  cdlemb3  40976  cdlemg4f  40985  cdlemg9a  41002  cdlemg9b  41003  cdlemg9  41004  cdlemg11aq  41008  cdlemg12a  41013  cdlemg12b  41014  cdlemg12c  41015  cdlemg12d  41016  cdlemg12f  41018  cdlemg12g  41019  cdlemg12  41020  cdlemg13a  41021  cdlemg16  41027  cdlemg17e  41035  cdlemg17f  41036  cdlemg17g  41037  cdlemg17ir  41040  cdlemg17  41047  cdlemg18b  41049  cdlemg18c  41050  cdlemg33e  41080  trlcoabs2N  41092  trlcocnvat  41094  trlcolem  41096  trlco  41097  cdlemg44  41103  cdlemg47  41106  ltrncom  41108  tendococl  41142  tendoplcl  41151  tendoplcom  41152  tendoplass  41153  tendodi1  41154  tendodi2  41155  tendo0pl  41161  tendoipl  41167  cdlemh1  41185  cdlemi2  41189  tendo0mul  41196  tendo0mulr  41197  cdlemk2  41202  cdlemk3  41203  cdlemk4  41204  cdlemk6  41207  cdlemk8  41208  cdlemk12  41220  cdlemkole  41223  cdlemk14  41224  cdlemk15  41225  cdlemk5u  41231  cdlemk6u  41232  cdlemk12u  41242  cdlemkfid1N  41291  cdlemk19x  41313  cdlemk48  41320  cdlemk53a  41325  cdlemk56  41341  cdleml2N  41347  cdleml3N  41348  cdleml6  41351  cdleml7  41352  dva1dim  41355  dia2dimlem4  41437  dvhlveclem  41478  doca2N  41496  djajN  41507  cdlemn2a  41566  cdlemn3  41567  dihordlem6  41583  dihord5apre  41632  dihglbcpreN  41670  dihmeetcN  41672  dihmeetbN  41673  dihmeetlem10N  41686  dihmeetlem12N  41688  dihmeetlem15N  41691  dihmeetALTN  41697  dih1dimatlem0  41698  dihjatcclem3  41790  dihjatcclem4  41791  mapdpglem22  42063  hdmap14lem1a  42236  eldioph2b  43114  jm2.19lem4  43343  jm2.19  43344  jm2.26a  43351  jm2.26  43353  hbtlem2  43475  fnchoice  45383  stoweidlem42  46394  stoweidlem59  46411  fourierdlem42  46501  zplusmodne  47697  minusmod5ne  47703