Theorem syl121anc 1375

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 1371	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  1379  fsnunf2  7220  tfisi  7896  fnsuppeq0  8233  ttrclss  9789  ttrclselem2  9795  axdc4lem  10524  div32d  12093  div13d  12094  expdivd  14210  swrdsbslen  14712  sumeven  16435  sumodd  16436  pcqmul  16900  pcid  16920  pcneg  16921  pc2dvds  16926  pcz  16928  pcaddlem  16935  pcadd  16936  pcmpt2  16940  pcbc  16947  qexpz  16948  expnprm  16949  sylow1lem1  19640  ringurd  20212  lspsneleq  21140  lspsneq  21147  lspfixed  21153  frlmsslss2  21818  chmatval  22856  chpmat1dlem  22862  chpdmatlem2  22866  ucncn  24315  ucnextcn  24334  ssblex  24459  prdsxmslem2  24563  ncvs1  25210  voliunlem1  25604  deg1mul3le  26176  deg1pw  26180  fta1blem  26230  bcmono  27339  dchrisum0flblem1  27570  dchrisum0flblem2  27571  pntibndlem1  27651  pntlemr  27664  nosupbnd1  27777  noinfbnd1  27792  noetalem1  27804  slerec  27882  finsumvtxdg2sstep  29585  umgr3cyclex  30215  nv1  30707  resf1o  32744  omndmul3  33063  symgcntz  33078  cycpmco2lem6  33124  tocyccntz  33137  deg1vr  33579  rtelextdg2lem  33717  measun  34175  measvuni  34178  measunl  34180  btwnconn1lem14  36064  segcon2  36069  seglelin  36080  neibastop3  36328  upixp  37689  fdc  37705  eqlkr3  39057  lkrshp  39061  lfl1dim  39077  lfl1dim2N  39078  eqlkr4  39121  2llnneN  39366  3dim2  39425  4atlem3  39553  4atlem11  39566  4atlem12  39569  pexmidlem4N  39930  lhp2at0nle  39992  lhple  39999  ltrnideq  40132  cdlemd9  40163  cdleme0ex2N  40181  cdleme0moN  40182  cdleme11a  40217  cdleme30a  40335  cdlemefs32sn1aw  40371  cdleme43fsv1snlem  40377  cdlemefs31fv1  40381  cdlemefs45eN  40388  cdleme41sn3a  40390  cdleme35h  40413  cdleme36a  40417  cdleme40m  40424  cdleme40n  40425  cdleme41sn3aw  40431  cdleme42h  40439  cdleme42k  40441  cdleme42mN  40444  cdleme43cN  40448  cdleme17d3  40453  cdleme48fvg  40457  cdlemeg47rv2  40467  cdlemeg46c  40470  cdlemeg46sfg  40477  cdlemeg46rjgN  40479  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemeg46gfv  40487  cdlemeg46gfre  40489  cdlemeg49lebilem  40496  cdleme50trn2  40508  cdlemg2kq  40559  cdlemb3  40563  cdlemg4f  40572  cdlemg9a  40589  cdlemg9b  40590  cdlemg9  40591  cdlemg11aq  40595  cdlemg12a  40600  cdlemg12b  40601  cdlemg12c  40602  cdlemg12d  40603  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg13a  40608  cdlemg16  40614  cdlemg17e  40622  cdlemg17f  40623  cdlemg17g  40624  cdlemg17ir  40627  cdlemg17  40634  cdlemg18b  40636  cdlemg18c  40637  cdlemg33e  40667  trlcoabs2N  40679  trlcocnvat  40681  trlcolem  40683  trlco  40684  cdlemg44  40690  cdlemg47  40693  ltrncom  40695  tendococl  40729  tendoplcl  40738  tendoplcom  40739  tendoplass  40740  tendodi1  40741  tendodi2  40742  tendo0pl  40748  tendoipl  40754  cdlemh1  40772  cdlemi2  40776  tendo0mul  40783  tendo0mulr  40784  cdlemk2  40789  cdlemk3  40790  cdlemk4  40791  cdlemk6  40794  cdlemk8  40795  cdlemk12  40807  cdlemkole  40810  cdlemk14  40811  cdlemk15  40812  cdlemk5u  40818  cdlemk6u  40819  cdlemk12u  40829  cdlemkfid1N  40878  cdlemk19x  40900  cdlemk48  40907  cdlemk53a  40912  cdlemk56  40928  cdleml2N  40934  cdleml3N  40935  cdleml6  40938  cdleml7  40939  dva1dim  40942  dia2dimlem4  41024  dvhlveclem  41065  doca2N  41083  djajN  41094  cdlemn2a  41153  cdlemn3  41154  dihordlem6  41170  dihord5apre  41219  dihglbcpreN  41257  dihmeetcN  41259  dihmeetbN  41260  dihmeetlem10N  41273  dihmeetlem12N  41275  dihmeetlem15N  41278  dihmeetALTN  41284  dih1dimatlem0  41285  dihjatcclem3  41377  dihjatcclem4  41378  mapdpglem22  41650  hdmap14lem1a  41823  eldioph2b  42719  jm2.19lem4  42949  jm2.19  42950  jm2.26a  42957  jm2.26  42959  hbtlem2  43081  fnchoice  44929  stoweidlem42  45963  stoweidlem59  45980  fourierdlem42  46070