Theorem syl121anc 1403

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 521	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1399	1 ⊢ (𝜑 → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl122anc  1407  fsnunf2  7211  tfisi  7891  fnsuppeq0  8234  ttrclss  9745  ttrclselem2  9751  axdc4lem  10557  div32d  12140  div13d  12141  expdivd  14327  swrdsbslen  14839  sumeven  16583  sumodd  16584  pcqmul  17057  pcid  17077  pcneg  17078  pc2dvds  17083  pcz  17085  pcaddlem  17092  pcadd  17093  pcmpt2  17097  pcbc  17104  qexpz  17105  expnprm  17106  sylow1lem1  19839  omndmul3  20375  ringurd  20438  lspsneleq  21420  lspsneq  21427  lspfixed  21433  frlmsslss2  22108  chmatval  23174  chpmat1dlem  23180  chpdmatlem2  23184  ucncn  24630  ucnextcn  24649  ssblex  24774  prdsxmslem2  24875  ncvs1  25505  voliunlem1  25898  deg1mul3le  26462  deg1pw  26466  fta1blem  26516  bcmono  27631  dchrisum0flblem1  27862  dchrisum0flblem2  27863  pntibndlem1  27943  pntlemr  27956  nosupbnd1  28098  noinfbnd1  28113  noetalem1  28125  lesrec  28212  finsumvtxdg2sstep  30157  umgr3cyclex  30811  nv1  31304  resf1o  33389  symgcntz  33713  cycpmco2lem6  33759  tocyccntz  33772  deg1vr  34191  rtelextdg2lem  34425  measun  34911  measvuni  34914  measunl  34916  btwnconn1lem14  37042  segcon2  37047  seglelin  37058  neibastop3  37327  upixp  38854  fdc  38870  eqlkr3  40349  lkrshp  40353  lfl1dim  40369  lfl1dim2N  40370  eqlkr4  40413  2llnneN  40657  3dim2  40716  4atlem3  40844  4atlem11  40857  4atlem12  40860  pexmidlem4N  41221  lhp2at0nle  41283  lhple  41290  ltrnideq  41423  cdlemd9  41454  cdleme0ex2N  41472  cdleme0moN  41473  cdleme11a  41508  cdleme30a  41626  cdlemefs32sn1aw  41662  cdleme43fsv1snlem  41668  cdlemefs31fv1  41672  cdlemefs45eN  41679  cdleme41sn3a  41681  cdleme35h  41704  cdleme36a  41708  cdleme40m  41715  cdleme40n  41716  cdleme41sn3aw  41722  cdleme42h  41730  cdleme42k  41732  cdleme42mN  41735  cdleme43cN  41739  cdleme17d3  41744  cdleme48fvg  41748  cdlemeg47rv2  41758  cdlemeg46c  41761  cdlemeg46sfg  41768  cdlemeg46rjgN  41770  cdlemeg46rgv  41776  cdlemeg46req  41777  cdlemeg46gfv  41778  cdlemeg46gfre  41780  cdlemeg49lebilem  41787  cdleme50trn2  41799  cdlemg2kq  41850  cdlemb3  41854  cdlemg4f  41863  cdlemg9a  41880  cdlemg9b  41881  cdlemg9  41882  cdlemg11aq  41886  cdlemg12a  41891  cdlemg12b  41892  cdlemg12c  41893  cdlemg12d  41894  cdlemg12f  41896  cdlemg12g  41897  cdlemg12  41898  cdlemg13a  41899  cdlemg16  41905  cdlemg17e  41913  cdlemg17f  41914  cdlemg17g  41915  cdlemg17ir  41918  cdlemg17  41925  cdlemg18b  41927  cdlemg18c  41928  cdlemg33e  41958  trlcoabs2N  41970  trlcocnvat  41972  trlcolem  41974  trlco  41975  cdlemg44  41981  cdlemg47  41984  ltrncom  41986  tendococl  42020  tendoplcl  42029  tendoplcom  42030  tendoplass  42031  tendodi1  42032  tendodi2  42033  tendo0pl  42039  tendoipl  42045  cdlemh1  42063  cdlemi2  42067  tendo0mul  42074  tendo0mulr  42075  cdlemk2  42080  cdlemk3  42081  cdlemk4  42082  cdlemk6  42085  cdlemk8  42086  cdlemk12  42098  cdlemkole  42101  cdlemk14  42102  cdlemk15  42103  cdlemk5u  42109  cdlemk6u  42110  cdlemk12u  42120  cdlemkfid1N  42169  cdlemk19x  42191  cdlemk48  42198  cdlemk53a  42203  cdlemk56  42219  cdleml2N  42225  cdleml3N  42226  cdleml6  42229  cdleml7  42230  dva1dim  42233  dia2dimlem4  42315  dvhlveclem  42356  doca2N  42374  djajN  42385  cdlemn2a  42444  cdlemn3  42445  dihordlem6  42461  dihord5apre  42510  dihglbcpreN  42548  dihmeetcN  42550  dihmeetbN  42551  dihmeetlem10N  42564  dihmeetlem12N  42566  dihmeetlem15N  42569  dihmeetALTN  42575  dih1dimatlem0  42576  dihjatcclem3  42668  dihjatcclem4  42669  mapdpglem22  42941  hdmap14lem1a  43114  eldioph2b  43965  jm2.19lem4  44190  jm2.19  44191  jm2.26a  44198  jm2.26  44200  hbtlem2  44316  fnchoice  46249  stoweidlem42  47255  stoweidlem59  47272  fourierdlem42  47362  zplusmodne  48622  minusmod5ne  48628