Theorem syl131anc 1383

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl131anc.6	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)

Assertion

Ref	Expression
syl131anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl131anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	2, 3, 4	3jca 1128	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1371	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ 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:  syl132anc  1388  syl231anc  1390  syl133anc  1393  initoeu2lem1  18081  estrres  18208  mulgdir  19146  umgr2edg  29244  2pthfrgr  30316  omndadd2d  33058  omndadd2rd  33059  submomnd  33060  omndmul2  33062  omndmul3  33063  ogrpinv0le  33065  ogrpsub  33066  ogrpaddltbi  33068  ogrpaddltrd  33069  ogrpinv0lt  33072  isarchi3  33167  archirngz  33169  archiabllem1a  33171  archiabllem1b  33172  archiabllem2a  33174  archiabllem2c  33175  orngsqr  33299  ornglmulle  33300  orngrmulle  33301  ofldchr  33309  lineext  36040  brsegle2  36073  cvrcmp  39239  cvrcmp2  39240  atcvreq0  39270  cvlatexch3  39294  cvlcvr1  39295  cvlsupr2  39299  cvlsupr7  39304  atnlej1  39336  atnlej2  39337  cvrval3  39370  ltltncvr  39380  atcvrneN  39387  atcvrj2b  39389  atbtwnex  39405  3noncolr2  39406  3noncolr1N  39407  4noncolr3  39410  3dimlem2  39416  3dimlem3a  39417  3dimlem3  39418  3dimlem3OLDN  39419  3dimlem4a  39420  3dimlem4  39421  3dimlem4OLDN  39422  ps-1  39434  hlatexch4  39438  3atlem1  39440  3atlem2  39441  3atlem3  39442  3atlem4  39443  3atlem5  39444  3atlem6  39445  3atlem7  39446  2llnmat  39481  ps-2c  39485  lplnri3N  39512  lplnexllnN  39521  2llnmeqat  39528  4atlem0a  39550  4atlem0ae  39551  4atlem0be  39552  4atlem9  39560  4atlem10a  39561  4atlem10b  39562  4atlem10  39563  4atlem11a  39564  4atlem11  39566  4atlem12a  39567  dalemcnes  39607  dalempnes  39608  dalemqnet  39609  dalem1  39616  dalemdea  39619  dalem3  39621  dalem5  39624  dalem-cly  39628  dalem27  39656  dalem28  39657  dalem41  39670  dalem45  39674  dalem48  39677  lneq2at  39735  2lnat  39741  2llnma1  39744  2llnma3r  39745  2llnma2  39746  cdlemblem  39750  paddasslem2  39778  pmodl42N  39808  hlmod1i  39813  atmod1i1m  39815  atmod2i1  39818  atmod2i2  39819  atmod3i1  39821  llnexchb2lem  39825  dalawlem2  39829  dalawlem3  39830  dalawlem6  39833  dalawlem7  39834  dalawlem11  39838  dalawlem12  39839  pexmidlem3N  39929  lhpexle3lem  39968  lhpmcvr3  39982  lhp2at0  39989  lhpelim  39994  lhpmod2i2  39995  lhpmod6i1  39996  4atexlempns  40019  4atexlemunv  40023  4atexlemc  40026  4atexlemnclw  40027  4atexlemex2  40028  4atexlemex6  40031  4atex  40033  4atex3  40038  trljat1  40123  trljat2  40124  ltrnatlw  40140  trlval4  40145  cdlemc1  40148  cdlemc3  40150  cdlemc6  40153  cdlemd3  40157  cdlemd4  40158  cdlemd5  40159  cdlemd6  40160  cdlemd7  40161  cdleme00a  40166  cdleme0cp  40171  cdleme0cq  40172  cdleme0e  40174  cdleme02N  40179  cdleme0ex2N  40181  cdleme0moN  40182  cdleme1  40184  cdleme2  40185  cdleme3e  40189  cdleme3g  40191  cdleme3h  40192  cdleme4  40195  cdleme5  40197  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme8  40207  cdleme9  40210  cdleme10  40211  cdleme16aN  40216  cdleme11a  40217  cdleme11c  40218  cdleme11dN  40219  cdleme11e  40220  cdleme11g  40222  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme12  40228  cdleme15a  40231  cdleme15b  40232  cdleme16b  40236  cdleme17c  40245  cdleme0nex  40247  cdleme18d  40252  cdlemednpq  40256  cdleme20zN  40258  cdleme20y  40259  cdleme19a  40260  cdleme19d  40263  cdleme20aN  40266  cdleme20c  40268  cdleme20i  40274  cdleme20j  40275  cdleme21a  40282  cdleme21b  40283  cdleme21c  40284  cdleme21ct  40286  cdleme22cN  40299  cdleme22d  40300  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f  40303  cdleme22f2  40304  cdleme22g  40305  cdleme23c  40308  cdleme41sn3a  40390  cdleme32le  40404  cdleme35b  40407  cdleme35c  40408  cdleme35d  40409  cdleme35e  40410  cdleme36a  40417  cdleme37m  40419  cdleme39a  40422  cdleme42a  40428  cdleme17d2  40452  cdlemeg46frv  40482  cdlemeg46rgv  40485  cdlemf1  40518  cdlemg2fv2  40557  cdlemg2l  40560  cdlemg2m  40561  cdlemg4d  40570  cdlemg4e  40571  cdlemg4f  40572  cdlemg4  40574  cdlemg6c  40577  cdlemg9a  40589  cdlemg10bALTN  40593  cdlemg12a  40600  cdlemg13  40609  cdlemg14f  40610  cdlemg14g  40611  cdlemg17i  40626  cdlemg17pq  40629  cdlemg19  40641  cdlemg21  40643  cdlemg27b  40653  cdlemg33c  40665  cdlemg33d  40666  trlcoabs2N  40679  cdlemg43  40687  cdlemg44b  40689  cdlemg44  40690  cdlemh1  40772  cdlemh2  40773  cdlemi1  40775  tendo0mul  40783  tendo0mulr  40784  cdlemk4  40791  cdlemk9  40796  cdlemk9bN  40797  cdlemk14  40811  cdlemkfid1N  40878  cdlemkid1  40879  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk55a  40916  cdlemk55u  40923  cdlemk39u  40925  cdlemk19u  40927  cdlemk56  40928  cdleml8  40940  dia2dimlem1  41021  dia2dimlem2  41022  dia2dimlem3  41023  cdlemn10  41163  dihjust  41174  dihord1  41175  dihlsscpre  41191  dihvalcqpre  41192  dihglbcpreN  41257  dihmeetlem5  41265  dihmeetlem7N  41267  dihjatc1  41268  lincreslvec3  48211  isldepslvec2  48214