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  18096  estrres  18220  mulgdir  19203  omndadd2d  20231  omndadd2rd  20232  submomnd  20233  omndmul2  20234  omndmul3  20235  ogrpinv0le  20237  ogrpsub  20238  ogrpaddltbi  20240  ogrpaddltrd  20241  ogrpinv0lt  20244  orngsqr  21006  ornglmulle  21007  orngrmulle  21008  ofldchr  21763  umgr2edg  29596  2pthfrgr  30672  isarchi3  33538  archirngz  33540  archiabllem1a  33542  archiabllem1b  33543  archiabllem2a  33545  archiabllem2c  33546  lineext  36589  brsegle2  36622  cvrcmp  40098  cvrcmp2  40099  atcvreq0  40129  cvlatexch3  40153  cvlcvr1  40154  cvlsupr2  40158  cvlsupr7  40163  atnlej1  40194  atnlej2  40195  cvrval3  40228  ltltncvr  40238  atcvrneN  40245  atcvrj2b  40247  atbtwnex  40263  3noncolr2  40264  3noncolr1N  40265  4noncolr3  40268  3dimlem2  40274  3dimlem3a  40275  3dimlem3  40276  3dimlem3OLDN  40277  3dimlem4a  40278  3dimlem4  40279  3dimlem4OLDN  40280  ps-1  40292  hlatexch4  40296  3atlem1  40298  3atlem2  40299  3atlem3  40300  3atlem4  40301  3atlem5  40302  3atlem6  40303  3atlem7  40304  2llnmat  40339  ps-2c  40343  lplnri3N  40370  lplnexllnN  40379  2llnmeqat  40386  4atlem0a  40408  4atlem0ae  40409  4atlem0be  40410  4atlem9  40418  4atlem10a  40419  4atlem10b  40420  4atlem10  40421  4atlem11a  40422  4atlem11  40424  4atlem12a  40425  dalemcnes  40465  dalempnes  40466  dalemqnet  40467  dalem1  40474  dalemdea  40477  dalem3  40479  dalem5  40482  dalem-cly  40486  dalem27  40514  dalem28  40515  dalem41  40528  dalem45  40532  dalem48  40535  lneq2at  40593  2lnat  40599  2llnma1  40602  2llnma3r  40603  2llnma2  40604  cdlemblem  40608  paddasslem2  40636  pmodl42N  40666  hlmod1i  40671  atmod1i1m  40673  atmod2i1  40676  atmod2i2  40677  atmod3i1  40679  llnexchb2lem  40683  dalawlem2  40687  dalawlem3  40688  dalawlem6  40691  dalawlem7  40692  dalawlem11  40696  dalawlem12  40697  pexmidlem3N  40787  lhpexle3lem  40826  lhpmcvr3  40840  lhp2at0  40847  lhpelim  40852  lhpmod2i2  40853  lhpmod6i1  40854  4atexlempns  40877  4atexlemunv  40881  4atexlemc  40884  4atexlemnclw  40885  4atexlemex2  40886  4atexlemex6  40889  4atex  40891  4atex3  40896  trljat1  40981  trljat2  40982  ltrnatlw  40998  trlval4  41003  cdlemc1  41006  cdlemc3  41008  cdlemc6  41011  cdlemd3  41015  cdlemd4  41016  cdlemd5  41017  cdlemd6  41018  cdlemd7  41019  cdleme00a  41024  cdleme0cp  41029  cdleme0cq  41030  cdleme0e  41032  cdleme02N  41037  cdleme0ex2N  41039  cdleme0moN  41040  cdleme1  41042  cdleme2  41043  cdleme3e  41047  cdleme3g  41049  cdleme3h  41050  cdleme4  41053  cdleme5  41055  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme8  41065  cdleme9  41068  cdleme10  41069  cdleme16aN  41074  cdleme11a  41075  cdleme11c  41076  cdleme11dN  41077  cdleme11e  41078  cdleme11g  41080  cdleme11h  41081  cdleme11j  41082  cdleme11k  41083  cdleme12  41086  cdleme15a  41089  cdleme15b  41090  cdleme16b  41094  cdleme17c  41103  cdleme0nex  41105  cdleme18d  41110  cdlemednpq  41114  cdleme20zN  41116  cdleme20y  41117  cdleme19a  41118  cdleme19d  41121  cdleme20aN  41124  cdleme20c  41126  cdleme20i  41132  cdleme20j  41133  cdleme21a  41140  cdleme21b  41141  cdleme21c  41142  cdleme21ct  41144  cdleme22cN  41157  cdleme22d  41158  cdleme22e  41159  cdleme22eALTN  41160  cdleme22f  41161  cdleme22f2  41162  cdleme22g  41163  cdleme23c  41166  cdleme41sn3a  41248  cdleme32le  41262  cdleme35b  41265  cdleme35c  41266  cdleme35d  41267  cdleme35e  41268  cdleme36a  41275  cdleme37m  41277  cdleme39a  41280  cdleme42a  41286  cdleme17d2  41310  cdlemeg46frv  41340  cdlemeg46rgv  41343  cdlemf1  41376  cdlemg2fv2  41415  cdlemg2l  41418  cdlemg2m  41419  cdlemg4d  41428  cdlemg4e  41429  cdlemg4f  41430  cdlemg4  41432  cdlemg6c  41435  cdlemg9a  41447  cdlemg10bALTN  41451  cdlemg12a  41458  cdlemg13  41467  cdlemg14f  41468  cdlemg14g  41469  cdlemg17i  41484  cdlemg17pq  41487  cdlemg19  41499  cdlemg21  41501  cdlemg27b  41511  cdlemg33c  41523  cdlemg33d  41524  trlcoabs2N  41537  cdlemg43  41545  cdlemg44b  41547  cdlemg44  41548  cdlemh1  41630  cdlemh2  41631  cdlemi1  41633  tendo0mul  41641  tendo0mulr  41642  cdlemk4  41649  cdlemk9  41654  cdlemk9bN  41655  cdlemk14  41669  cdlemkfid1N  41736  cdlemkid1  41737  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk55a  41774  cdlemk55u  41781  cdlemk39u  41783  cdlemk19u  41785  cdlemk56  41786  cdleml8  41798  dia2dimlem1  41879  dia2dimlem2  41880  dia2dimlem3  41881  cdlemn10  42021  dihjust  42032  dihord1  42033  dihlsscpre  42049  dihvalcqpre  42050  dihglbcpreN  42115  dihmeetlem5  42123  dihmeetlem7N  42125  dihjatc1  42126  modmknepk  48146  modm2nep1  48150  modp2nep1  48151  modm1nep2  48152  modm1nem2  48153  lincreslvec3  49303  isldepslvec2  49306