Theorem syl131anc 1410

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

This proof depends on syntax axioms:   → wi 4   ∧ 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:  syl132anc  1415  syl231anc  1417  syl133anc  1420  initoeu2lem1  18169  estrres  18293  mulgdir  19296  omndadd2d  20324  omndadd2rd  20325  submomnd  20326  omndmul2  20327  omndmul3  20328  ogrpinv0le  20330  ogrpsub  20331  ogrpaddltbi  20333  ogrpaddltrd  20334  ogrpinv0lt  20337  orngsqr  21103  ornglmulle  21104  orngrmulle  21105  ofldchr  21862  umgr2edg  29772  2pthfrgr  30867  isarchi3  33730  archirngz  33732  archiabllem1a  33734  archiabllem1b  33735  archiabllem2a  33737  archiabllem2c  33738  lineext  36811  brsegle2  36844  cvrcmp  40308  cvrcmp2  40309  atcvreq0  40339  cvlatexch3  40363  cvlcvr1  40364  cvlsupr2  40368  cvlsupr7  40373  atnlej1  40404  atnlej2  40405  cvrval3  40438  ltltncvr  40448  atcvrneN  40455  atcvrj2b  40457  atbtwnex  40473  3noncolr2  40474  3noncolr1N  40475  4noncolr3  40478  3dimlem2  40484  3dimlem3a  40485  3dimlem3  40486  3dimlem3OLDN  40487  3dimlem4a  40488  3dimlem4  40489  3dimlem4OLDN  40490  ps-1  40502  hlatexch4  40506  3atlem1  40508  3atlem2  40509  3atlem3  40510  3atlem4  40511  3atlem5  40512  3atlem6  40513  3atlem7  40514  2llnmat  40549  ps-2c  40553  lplnri3N  40580  lplnexllnN  40589  2llnmeqat  40596  4atlem0a  40618  4atlem0ae  40619  4atlem0be  40620  4atlem9  40628  4atlem10a  40629  4atlem10b  40630  4atlem10  40631  4atlem11a  40632  4atlem11  40634  4atlem12a  40635  dalemcnes  40675  dalempnes  40676  dalemqnet  40677  dalem1  40684  dalemdea  40687  dalem3  40689  dalem5  40692  dalem-cly  40696  dalem27  40724  dalem28  40725  dalem41  40738  dalem45  40742  dalem48  40745  lneq2at  40803  2lnat  40809  2llnma1  40812  2llnma3r  40813  2llnma2  40814  cdlemblem  40818  paddasslem2  40846  pmodl42N  40876  hlmod1i  40881  atmod1i1m  40883  atmod2i1  40886  atmod2i2  40887  atmod3i1  40889  llnexchb2lem  40893  dalawlem2  40897  dalawlem3  40898  dalawlem6  40901  dalawlem7  40902  dalawlem11  40906  dalawlem12  40907  pexmidlem3N  40997  lhpexle3lem  41036  lhpmcvr3  41050  lhp2at0  41057  lhpelim  41062  lhpmod2i2  41063  lhpmod6i1  41064  4atexlempns  41087  4atexlemunv  41091  4atexlemc  41094  4atexlemnclw  41095  4atexlemex2  41096  4atexlemex6  41099  4atex  41101  4atex3  41106  trljat1  41191  trljat2  41192  ltrnatlw  41208  trlval4  41213  cdlemc1  41216  cdlemc3  41218  cdlemc6  41221  cdlemd3  41225  cdlemd4  41226  cdlemd5  41227  cdlemd6  41228  cdlemd7  41229  cdleme00a  41234  cdleme0cp  41239  cdleme0cq  41240  cdleme0e  41242  cdleme02N  41247  cdleme0ex2N  41249  cdleme0moN  41250  cdleme1  41252  cdleme2  41253  cdleme3e  41257  cdleme3g  41259  cdleme3h  41260  cdleme4  41263  cdleme5  41265  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme8  41275  cdleme9  41278  cdleme10  41279  cdleme16aN  41284  cdleme11a  41285  cdleme11c  41286  cdleme11dN  41287  cdleme11e  41288  cdleme11g  41290  cdleme11h  41291  cdleme11j  41292  cdleme11k  41293  cdleme12  41296  cdleme15a  41299  cdleme15b  41300  cdleme16b  41304  cdleme17c  41313  cdleme0nex  41315  cdleme18d  41320  cdlemednpq  41324  cdleme20zN  41326  cdleme20y  41327  cdleme19a  41328  cdleme19d  41331  cdleme20aN  41334  cdleme20c  41336  cdleme20i  41342  cdleme20j  41343  cdleme21a  41350  cdleme21b  41351  cdleme21c  41352  cdleme21ct  41354  cdleme22cN  41367  cdleme22d  41368  cdleme22e  41369  cdleme22eALTN  41370  cdleme22f  41371  cdleme22f2  41372  cdleme22g  41373  cdleme23c  41376  cdleme41sn3a  41458  cdleme32le  41472  cdleme35b  41475  cdleme35c  41476  cdleme35d  41477  cdleme35e  41478  cdleme36a  41485  cdleme37m  41487  cdleme39a  41490  cdleme42a  41496  cdleme17d2  41520  cdlemeg46frv  41550  cdlemeg46rgv  41553  cdlemf1  41586  cdlemg2fv2  41625  cdlemg2l  41628  cdlemg2m  41629  cdlemg4d  41638  cdlemg4e  41639  cdlemg4f  41640  cdlemg4  41642  cdlemg6c  41645  cdlemg9a  41657  cdlemg10bALTN  41661  cdlemg12a  41668  cdlemg13  41677  cdlemg14f  41678  cdlemg14g  41679  cdlemg17i  41694  cdlemg17pq  41697  cdlemg19  41709  cdlemg21  41711  cdlemg27b  41721  cdlemg33c  41733  cdlemg33d  41734  trlcoabs2N  41747  cdlemg43  41755  cdlemg44b  41757  cdlemg44  41758  cdlemh1  41840  cdlemh2  41841  cdlemi1  41843  tendo0mul  41851  tendo0mulr  41852  cdlemk4  41859  cdlemk9  41864  cdlemk9bN  41865  cdlemk14  41879  cdlemkfid1N  41946  cdlemkid1  41947  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk55a  41984  cdlemk55u  41991  cdlemk39u  41993  cdlemk19u  41995  cdlemk56  41996  cdleml8  42008  dia2dimlem1  42089  dia2dimlem2  42090  dia2dimlem3  42091  cdlemn10  42231  dihjust  42242  dihord1  42243  dihlsscpre  42259  dihvalcqpre  42260  dihglbcpreN  42325  dihmeetlem5  42333  dihmeetlem7N  42335  dihjatc1  42336  modmknepk  48382  modm2nep1  48386  modp2nep1  48387  modm1nep2  48388  modm1nem2  48389  lincreslvec3  49538  isldepslvec2  49541