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  7134  tfisi  7803  fnsuppeq0  8135  ttrclss  9632  ttrclselem2  9638  axdc4lem  10368  div32d  11945  div13d  11946  expdivd  14113  swrdsbslen  14618  sumeven  16347  sumodd  16348  pcqmul  16815  pcid  16835  pcneg  16836  pc2dvds  16841  pcz  16843  pcaddlem  16850  pcadd  16851  pcmpt2  16855  pcbc  16862  qexpz  16863  expnprm  16864  sylow1lem1  19564  omndmul3  20100  ringurd  20157  lspsneleq  21105  lspsneq  21112  lspfixed  21118  frlmsslss2  21765  chmatval  22804  chpmat1dlem  22810  chpdmatlem2  22814  ucncn  24259  ucnextcn  24278  ssblex  24403  prdsxmslem2  24504  ncvs1  25134  voliunlem1  25527  deg1mul3le  26092  deg1pw  26096  fta1blem  26146  bcmono  27254  dchrisum0flblem1  27485  dchrisum0flblem2  27486  pntibndlem1  27566  pntlemr  27579  nosupbnd1  27692  noinfbnd1  27707  noetalem1  27719  lesrec  27805  finsumvtxdg2sstep  29633  umgr3cyclex  30268  nv1  30761  resf1o  32818  symgcntz  33161  cycpmco2lem6  33207  tocyccntz  33220  deg1vr  33667  rtelextdg2lem  33886  measun  34371  measvuni  34374  measunl  34376  btwnconn1lem14  36298  segcon2  36303  seglelin  36314  neibastop3  36560  upixp  38064  fdc  38080  eqlkr3  39561  lkrshp  39565  lfl1dim  39581  lfl1dim2N  39582  eqlkr4  39625  2llnneN  39869  3dim2  39928  4atlem3  40056  4atlem11  40069  4atlem12  40072  pexmidlem4N  40433  lhp2at0nle  40495  lhple  40502  ltrnideq  40635  cdlemd9  40666  cdleme0ex2N  40684  cdleme0moN  40685  cdleme11a  40720  cdleme30a  40838  cdlemefs32sn1aw  40874  cdleme43fsv1snlem  40880  cdlemefs31fv1  40884  cdlemefs45eN  40891  cdleme41sn3a  40893  cdleme35h  40916  cdleme36a  40920  cdleme40m  40927  cdleme40n  40928  cdleme41sn3aw  40934  cdleme42h  40942  cdleme42k  40944  cdleme42mN  40947  cdleme43cN  40951  cdleme17d3  40956  cdleme48fvg  40960  cdlemeg47rv2  40970  cdlemeg46c  40973  cdlemeg46sfg  40980  cdlemeg46rjgN  40982  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemeg46gfv  40990  cdlemeg46gfre  40992  cdlemeg49lebilem  40999  cdleme50trn2  41011  cdlemg2kq  41062  cdlemb3  41066  cdlemg4f  41075  cdlemg9a  41092  cdlemg9b  41093  cdlemg9  41094  cdlemg11aq  41098  cdlemg12a  41103  cdlemg12b  41104  cdlemg12c  41105  cdlemg12d  41106  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg13a  41111  cdlemg16  41117  cdlemg17e  41125  cdlemg17f  41126  cdlemg17g  41127  cdlemg17ir  41130  cdlemg17  41137  cdlemg18b  41139  cdlemg18c  41140  cdlemg33e  41170  trlcoabs2N  41182  trlcocnvat  41184  trlcolem  41186  trlco  41187  cdlemg44  41193  cdlemg47  41196  ltrncom  41198  tendococl  41232  tendoplcl  41241  tendoplcom  41242  tendoplass  41243  tendodi1  41244  tendodi2  41245  tendo0pl  41251  tendoipl  41257  cdlemh1  41275  cdlemi2  41279  tendo0mul  41286  tendo0mulr  41287  cdlemk2  41292  cdlemk3  41293  cdlemk4  41294  cdlemk6  41297  cdlemk8  41298  cdlemk12  41310  cdlemkole  41313  cdlemk14  41314  cdlemk15  41315  cdlemk5u  41321  cdlemk6u  41322  cdlemk12u  41332  cdlemkfid1N  41381  cdlemk19x  41403  cdlemk48  41410  cdlemk53a  41415  cdlemk56  41431  cdleml2N  41437  cdleml3N  41438  cdleml6  41441  cdleml7  41442  dva1dim  41445  dia2dimlem4  41527  dvhlveclem  41568  doca2N  41586  djajN  41597  cdlemn2a  41656  cdlemn3  41657  dihordlem6  41673  dihord5apre  41722  dihglbcpreN  41760  dihmeetcN  41762  dihmeetbN  41763  dihmeetlem10N  41776  dihmeetlem12N  41778  dihmeetlem15N  41781  dihmeetALTN  41787  dih1dimatlem0  41788  dihjatcclem3  41880  dihjatcclem4  41881  mapdpglem22  42153  hdmap14lem1a  42326  eldioph2b  43209  jm2.19lem4  43438  jm2.19  43439  jm2.26a  43446  jm2.26  43448  hbtlem2  43570  fnchoice  45478  stoweidlem42  46488  stoweidlem59  46505  fourierdlem42  46595  zplusmodne  47809  minusmod5ne  47815