Theorem syl131anc 1381

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 1126	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1369	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  syl132anc  1386  syl231anc  1388  syl133anc  1391  initoeu2lem1  17710  estrres  17837  mulgdir  18716  umgr2edg  27557  2pthfrgr  28627  omndadd2d  31313  omndadd2rd  31314  submomnd  31315  omndmul2  31317  omndmul3  31318  ogrpinv0le  31320  ogrpsub  31321  ogrpaddltbi  31323  ogrpaddltrd  31324  ogrpinv0lt  31327  isarchi3  31420  archirngz  31422  archiabllem1a  31424  archiabllem1b  31425  archiabllem2a  31427  archiabllem2c  31428  orngsqr  31482  ornglmulle  31483  orngrmulle  31484  ofldchr  31492  lineext  34357  brsegle2  34390  cvrcmp  37276  cvrcmp2  37277  atcvreq0  37307  cvlatexch3  37331  cvlcvr1  37332  cvlsupr2  37336  cvlsupr7  37341  atnlej1  37372  atnlej2  37373  cvrval3  37406  ltltncvr  37416  atcvrneN  37423  atcvrj2b  37425  atbtwnex  37441  3noncolr2  37442  3noncolr1N  37443  4noncolr3  37446  3dimlem2  37452  3dimlem3a  37453  3dimlem3  37454  3dimlem3OLDN  37455  3dimlem4a  37456  3dimlem4  37457  3dimlem4OLDN  37458  ps-1  37470  hlatexch4  37474  3atlem1  37476  3atlem2  37477  3atlem3  37478  3atlem4  37479  3atlem5  37480  3atlem6  37481  3atlem7  37482  2llnmat  37517  ps-2c  37521  lplnri3N  37548  lplnexllnN  37557  2llnmeqat  37564  4atlem0a  37586  4atlem0ae  37587  4atlem0be  37588  4atlem9  37596  4atlem10a  37597  4atlem10b  37598  4atlem10  37599  4atlem11a  37600  4atlem11  37602  4atlem12a  37603  dalemcnes  37643  dalempnes  37644  dalemqnet  37645  dalem1  37652  dalemdea  37655  dalem3  37657  dalem5  37660  dalem-cly  37664  dalem27  37692  dalem28  37693  dalem41  37706  dalem45  37710  dalem48  37713  lneq2at  37771  2lnat  37777  2llnma1  37780  2llnma3r  37781  2llnma2  37782  cdlemblem  37786  paddasslem2  37814  pmodl42N  37844  hlmod1i  37849  atmod1i1m  37851  atmod2i1  37854  atmod2i2  37855  atmod3i1  37857  llnexchb2lem  37861  dalawlem2  37865  dalawlem3  37866  dalawlem6  37869  dalawlem7  37870  dalawlem11  37874  dalawlem12  37875  pexmidlem3N  37965  lhpexle3lem  38004  lhpmcvr3  38018  lhp2at0  38025  lhpelim  38030  lhpmod2i2  38031  lhpmod6i1  38032  4atexlempns  38055  4atexlemunv  38059  4atexlemc  38062  4atexlemnclw  38063  4atexlemex2  38064  4atexlemex6  38067  4atex  38069  4atex3  38074  trljat1  38159  trljat2  38160  ltrnatlw  38176  trlval4  38181  cdlemc1  38184  cdlemc3  38186  cdlemc6  38189  cdlemd3  38193  cdlemd4  38194  cdlemd5  38195  cdlemd6  38196  cdlemd7  38197  cdleme00a  38202  cdleme0cp  38207  cdleme0cq  38208  cdleme0e  38210  cdleme02N  38215  cdleme0ex2N  38217  cdleme0moN  38218  cdleme1  38220  cdleme2  38221  cdleme3e  38225  cdleme3g  38227  cdleme3h  38228  cdleme4  38231  cdleme5  38233  cdleme7aa  38235  cdleme7c  38238  cdleme7d  38239  cdleme7e  38240  cdleme8  38243  cdleme9  38246  cdleme10  38247  cdleme16aN  38252  cdleme11a  38253  cdleme11c  38254  cdleme11dN  38255  cdleme11e  38256  cdleme11g  38258  cdleme11h  38259  cdleme11j  38260  cdleme11k  38261  cdleme12  38264  cdleme15a  38267  cdleme15b  38268  cdleme16b  38272  cdleme17c  38281  cdleme0nex  38283  cdleme18d  38288  cdlemednpq  38292  cdleme20zN  38294  cdleme20y  38295  cdleme19a  38296  cdleme19d  38299  cdleme20aN  38302  cdleme20c  38304  cdleme20i  38310  cdleme20j  38311  cdleme21a  38318  cdleme21b  38319  cdleme21c  38320  cdleme21ct  38322  cdleme22cN  38335  cdleme22d  38336  cdleme22e  38337  cdleme22eALTN  38338  cdleme22f  38339  cdleme22f2  38340  cdleme22g  38341  cdleme23c  38344  cdleme41sn3a  38426  cdleme32le  38440  cdleme35b  38443  cdleme35c  38444  cdleme35d  38445  cdleme35e  38446  cdleme36a  38453  cdleme37m  38455  cdleme39a  38458  cdleme42a  38464  cdleme17d2  38488  cdlemeg46frv  38518  cdlemeg46rgv  38521  cdlemf1  38554  cdlemg2fv2  38593  cdlemg2l  38596  cdlemg2m  38597  cdlemg4d  38606  cdlemg4e  38607  cdlemg4f  38608  cdlemg4  38610  cdlemg6c  38613  cdlemg9a  38625  cdlemg10bALTN  38629  cdlemg12a  38636  cdlemg13  38645  cdlemg14f  38646  cdlemg14g  38647  cdlemg17i  38662  cdlemg17pq  38665  cdlemg19  38677  cdlemg21  38679  cdlemg27b  38689  cdlemg33c  38701  cdlemg33d  38702  trlcoabs2N  38715  cdlemg43  38723  cdlemg44b  38725  cdlemg44  38726  cdlemh1  38808  cdlemh2  38809  cdlemi1  38811  tendo0mul  38819  tendo0mulr  38820  cdlemk4  38827  cdlemk9  38832  cdlemk9bN  38833  cdlemk14  38847  cdlemkfid1N  38914  cdlemkid1  38915  cdlemk35s-id  38931  cdlemk39s-id  38933  cdlemk55a  38952  cdlemk55u  38959  cdlemk39u  38961  cdlemk19u  38963  cdlemk56  38964  cdleml8  38976  dia2dimlem1  39057  dia2dimlem2  39058  dia2dimlem3  39059  cdlemn10  39199  dihjust  39210  dihord1  39211  dihlsscpre  39227  dihvalcqpre  39228  dihglbcpreN  39293  dihmeetlem5  39301  dihmeetlem7N  39303  dihjatc1  39304  lincreslvec3  45775  isldepslvec2  45778