Theorem syl131anc 1411

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 1399	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  1416  syl231anc  1418  syl133anc  1421  initoeu2lem1  18218  estrres  18342  mulgdir  19345  omndadd2d  20374  omndadd2rd  20375  submomnd  20376  omndmul2  20377  omndmul3  20378  ogrpinv0le  20380  ogrpsub  20381  ogrpaddltbi  20383  ogrpaddltrd  20384  ogrpinv0lt  20387  orngsqr  21153  ornglmulle  21154  orngrmulle  21155  ofldchr  21912  umgr2edg  29820  2pthfrgr  30915  isarchi3  33818  archirngz  33820  archiabllem1a  33822  archiabllem1b  33823  archiabllem2a  33825  archiabllem2c  33826  lineext  37019  brsegle2  37052  cvrcmp  40532  cvrcmp2  40533  atcvreq0  40563  cvlatexch3  40587  cvlcvr1  40588  cvlsupr2  40592  cvlsupr7  40597  atnlej1  40628  atnlej2  40629  cvrval3  40662  ltltncvr  40672  atcvrneN  40679  atcvrj2b  40681  atbtwnex  40697  3noncolr2  40698  3noncolr1N  40699  4noncolr3  40702  3dimlem2  40708  3dimlem3a  40709  3dimlem3  40710  3dimlem3OLDN  40711  3dimlem4a  40712  3dimlem4  40713  3dimlem4OLDN  40714  ps-1  40726  hlatexch4  40730  3atlem1  40732  3atlem2  40733  3atlem3  40734  3atlem4  40735  3atlem5  40736  3atlem6  40737  3atlem7  40738  2llnmat  40773  ps-2c  40777  lplnri3N  40804  lplnexllnN  40813  2llnmeqat  40820  4atlem0a  40842  4atlem0ae  40843  4atlem0be  40844  4atlem9  40852  4atlem10a  40853  4atlem10b  40854  4atlem10  40855  4atlem11a  40856  4atlem11  40858  4atlem12a  40859  dalemcnes  40899  dalempnes  40900  dalemqnet  40901  dalem1  40908  dalemdea  40911  dalem3  40913  dalem5  40916  dalem-cly  40920  dalem27  40948  dalem28  40949  dalem41  40962  dalem45  40966  dalem48  40969  lneq2at  41027  2lnat  41033  2llnma1  41036  2llnma3r  41037  2llnma2  41038  cdlemblem  41042  paddasslem2  41070  pmodl42N  41100  hlmod1i  41105  atmod1i1m  41107  atmod2i1  41110  atmod2i2  41111  atmod3i1  41113  llnexchb2lem  41117  dalawlem2  41121  dalawlem3  41122  dalawlem6  41125  dalawlem7  41126  dalawlem11  41130  dalawlem12  41131  pexmidlem3N  41221  lhpexle3lem  41260  lhpmcvr3  41274  lhp2at0  41281  lhpelim  41286  lhpmod2i2  41287  lhpmod6i1  41288  4atexlempns  41311  4atexlemunv  41315  4atexlemc  41318  4atexlemnclw  41319  4atexlemex2  41320  4atexlemex6  41323  4atex  41325  4atex3  41330  trljat1  41415  trljat2  41416  ltrnatlw  41432  trlval4  41437  cdlemc1  41440  cdlemc3  41442  cdlemc6  41445  cdlemd3  41449  cdlemd4  41450  cdlemd5  41451  cdlemd6  41452  cdlemd7  41453  cdleme00a  41458  cdleme0cp  41463  cdleme0cq  41464  cdleme0e  41466  cdleme02N  41471  cdleme0ex2N  41473  cdleme0moN  41474  cdleme1  41476  cdleme2  41477  cdleme3e  41481  cdleme3g  41483  cdleme3h  41484  cdleme4  41487  cdleme5  41489  cdleme7aa  41491  cdleme7c  41494  cdleme7d  41495  cdleme7e  41496  cdleme8  41499  cdleme9  41502  cdleme10  41503  cdleme16aN  41508  cdleme11a  41509  cdleme11c  41510  cdleme11dN  41511  cdleme11e  41512  cdleme11g  41514  cdleme11h  41515  cdleme11j  41516  cdleme11k  41517  cdleme12  41520  cdleme15a  41523  cdleme15b  41524  cdleme16b  41528  cdleme17c  41537  cdleme0nex  41539  cdleme18d  41544  cdlemednpq  41548  cdleme20zN  41550  cdleme20y  41551  cdleme19a  41552  cdleme19d  41555  cdleme20aN  41558  cdleme20c  41560  cdleme20i  41566  cdleme20j  41567  cdleme21a  41574  cdleme21b  41575  cdleme21c  41576  cdleme21ct  41578  cdleme22cN  41591  cdleme22d  41592  cdleme22e  41593  cdleme22eALTN  41594  cdleme22f  41595  cdleme22f2  41596  cdleme22g  41597  cdleme23c  41600  cdleme41sn3a  41682  cdleme32le  41696  cdleme35b  41699  cdleme35c  41700  cdleme35d  41701  cdleme35e  41702  cdleme36a  41709  cdleme37m  41711  cdleme39a  41714  cdleme42a  41720  cdleme17d2  41744  cdlemeg46frv  41774  cdlemeg46rgv  41777  cdlemf1  41810  cdlemg2fv2  41849  cdlemg2l  41852  cdlemg2m  41853  cdlemg4d  41862  cdlemg4e  41863  cdlemg4f  41864  cdlemg4  41866  cdlemg6c  41869  cdlemg9a  41881  cdlemg10bALTN  41885  cdlemg12a  41892  cdlemg13  41901  cdlemg14f  41902  cdlemg14g  41903  cdlemg17i  41918  cdlemg17pq  41921  cdlemg19  41933  cdlemg21  41935  cdlemg27b  41945  cdlemg33c  41957  cdlemg33d  41958  trlcoabs2N  41971  cdlemg43  41979  cdlemg44b  41981  cdlemg44  41982  cdlemh1  42064  cdlemh2  42065  cdlemi1  42067  tendo0mul  42075  tendo0mulr  42076  cdlemk4  42083  cdlemk9  42088  cdlemk9bN  42089  cdlemk14  42103  cdlemkfid1N  42170  cdlemkid1  42171  cdlemk35s-id  42187  cdlemk39s-id  42189  cdlemk55a  42208  cdlemk55u  42215  cdlemk39u  42217  cdlemk19u  42219  cdlemk56  42220  cdleml8  42232  dia2dimlem1  42313  dia2dimlem2  42314  dia2dimlem3  42315  cdlemn10  42455  dihjust  42466  dihord1  42467  dihlsscpre  42483  dihvalcqpre  42484  dihglbcpreN  42549  dihmeetlem5  42557  dihmeetlem7N  42559  dihjatc1  42560  modmknepk  48643  modm2nep1  48647  modp2nep1  48648  modm1nep2  48649  modm1nem2  48650  lincreslvec3  49799  isldepslvec2  49802