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  7141  tfisi  7810  fnsuppeq0  8142  ttrclss  9641  ttrclselem2  9647  axdc4lem  10377  div32d  11954  div13d  11955  expdivd  14122  swrdsbslen  14627  sumeven  16356  sumodd  16357  pcqmul  16824  pcid  16844  pcneg  16845  pc2dvds  16850  pcz  16852  pcaddlem  16859  pcadd  16860  pcmpt2  16864  pcbc  16871  qexpz  16872  expnprm  16873  sylow1lem1  19573  omndmul3  20109  ringurd  20166  lspsneleq  21113  lspsneq  21120  lspfixed  21126  frlmsslss2  21755  chmatval  22794  chpmat1dlem  22800  chpdmatlem2  22804  ucncn  24249  ucnextcn  24268  ssblex  24393  prdsxmslem2  24494  ncvs1  25124  voliunlem1  25517  deg1mul3le  26082  deg1pw  26086  fta1blem  26136  bcmono  27240  dchrisum0flblem1  27471  dchrisum0flblem2  27472  pntibndlem1  27552  pntlemr  27565  nosupbnd1  27678  noinfbnd1  27693  noetalem1  27705  lesrec  27791  finsumvtxdg2sstep  29618  umgr3cyclex  30253  nv1  30746  resf1o  32803  symgcntz  33146  cycpmco2lem6  33192  tocyccntz  33205  deg1vr  33652  rtelextdg2lem  33870  measun  34355  measvuni  34358  measunl  34360  btwnconn1lem14  36282  segcon2  36287  seglelin  36298  neibastop3  36544  upixp  38050  fdc  38066  eqlkr3  39547  lkrshp  39551  lfl1dim  39567  lfl1dim2N  39568  eqlkr4  39611  2llnneN  39855  3dim2  39914  4atlem3  40042  4atlem11  40055  4atlem12  40058  pexmidlem4N  40419  lhp2at0nle  40481  lhple  40488  ltrnideq  40621  cdlemd9  40652  cdleme0ex2N  40670  cdleme0moN  40671  cdleme11a  40706  cdleme30a  40824  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdlemefs31fv1  40870  cdlemefs45eN  40877  cdleme41sn3a  40879  cdleme35h  40902  cdleme36a  40906  cdleme40m  40913  cdleme40n  40914  cdleme41sn3aw  40920  cdleme42h  40928  cdleme42k  40930  cdleme42mN  40933  cdleme43cN  40937  cdleme17d3  40942  cdleme48fvg  40946  cdlemeg47rv2  40956  cdlemeg46c  40959  cdlemeg46sfg  40966  cdlemeg46rjgN  40968  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemeg46gfv  40976  cdlemeg46gfre  40978  cdlemeg49lebilem  40985  cdleme50trn2  40997  cdlemg2kq  41048  cdlemb3  41052  cdlemg4f  41061  cdlemg9a  41078  cdlemg9b  41079  cdlemg9  41080  cdlemg11aq  41084  cdlemg12a  41089  cdlemg12b  41090  cdlemg12c  41091  cdlemg12d  41092  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg16  41103  cdlemg17e  41111  cdlemg17f  41112  cdlemg17g  41113  cdlemg17ir  41116  cdlemg17  41123  cdlemg18b  41125  cdlemg18c  41126  cdlemg33e  41156  trlcoabs2N  41168  trlcocnvat  41170  trlcolem  41172  trlco  41173  cdlemg44  41179  cdlemg47  41182  ltrncom  41184  tendococl  41218  tendoplcl  41227  tendoplcom  41228  tendoplass  41229  tendodi1  41230  tendodi2  41231  tendo0pl  41237  tendoipl  41243  cdlemh1  41261  cdlemi2  41265  tendo0mul  41272  tendo0mulr  41273  cdlemk2  41278  cdlemk3  41279  cdlemk4  41280  cdlemk6  41283  cdlemk8  41284  cdlemk12  41296  cdlemkole  41299  cdlemk14  41300  cdlemk15  41301  cdlemk5u  41307  cdlemk6u  41308  cdlemk12u  41318  cdlemkfid1N  41367  cdlemk19x  41389  cdlemk48  41396  cdlemk53a  41401  cdlemk56  41417  cdleml2N  41423  cdleml3N  41424  cdleml6  41427  cdleml7  41428  dva1dim  41431  dia2dimlem4  41513  dvhlveclem  41554  doca2N  41572  djajN  41583  cdlemn2a  41642  cdlemn3  41643  dihordlem6  41659  dihord5apre  41708  dihglbcpreN  41746  dihmeetcN  41748  dihmeetbN  41749  dihmeetlem10N  41762  dihmeetlem12N  41764  dihmeetlem15N  41767  dihmeetALTN  41773  dih1dimatlem0  41774  dihjatcclem3  41866  dihjatcclem4  41867  mapdpglem22  42139  hdmap14lem1a  42312  eldioph2b  43195  jm2.19lem4  43420  jm2.19  43421  jm2.26a  43428  jm2.26  43430  hbtlem2  43552  fnchoice  45460  stoweidlem42  46470  stoweidlem59  46487  fourierdlem42  46577  zplusmodne  47797  minusmod5ne  47803