Theorem syl131anc 1382

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  syl132anc  1387  syl231anc  1389  syl133anc  1392  initoeu2lem1  18067  estrres  18194  mulgdir  19136  umgr2edg  29240  2pthfrgr  30312  omndadd2d  33067  omndadd2rd  33068  submomnd  33069  omndmul2  33071  omndmul3  33072  ogrpinv0le  33074  ogrpsub  33075  ogrpaddltbi  33077  ogrpaddltrd  33078  ogrpinv0lt  33081  isarchi3  33176  archirngz  33178  archiabllem1a  33180  archiabllem1b  33181  archiabllem2a  33183  archiabllem2c  33184  orngsqr  33313  ornglmulle  33314  orngrmulle  33315  ofldchr  33323  lineext  36057  brsegle2  36090  cvrcmp  39264  cvrcmp2  39265  atcvreq0  39295  cvlatexch3  39319  cvlcvr1  39320  cvlsupr2  39324  cvlsupr7  39329  atnlej1  39361  atnlej2  39362  cvrval3  39395  ltltncvr  39405  atcvrneN  39412  atcvrj2b  39414  atbtwnex  39430  3noncolr2  39431  3noncolr1N  39432  4noncolr3  39435  3dimlem2  39441  3dimlem3a  39442  3dimlem3  39443  3dimlem3OLDN  39444  3dimlem4a  39445  3dimlem4  39446  3dimlem4OLDN  39447  ps-1  39459  hlatexch4  39463  3atlem1  39465  3atlem2  39466  3atlem3  39467  3atlem4  39468  3atlem5  39469  3atlem6  39470  3atlem7  39471  2llnmat  39506  ps-2c  39510  lplnri3N  39537  lplnexllnN  39546  2llnmeqat  39553  4atlem0a  39575  4atlem0ae  39576  4atlem0be  39577  4atlem9  39585  4atlem10a  39586  4atlem10b  39587  4atlem10  39588  4atlem11a  39589  4atlem11  39591  4atlem12a  39592  dalemcnes  39632  dalempnes  39633  dalemqnet  39634  dalem1  39641  dalemdea  39644  dalem3  39646  dalem5  39649  dalem-cly  39653  dalem27  39681  dalem28  39682  dalem41  39695  dalem45  39699  dalem48  39702  lneq2at  39760  2lnat  39766  2llnma1  39769  2llnma3r  39770  2llnma2  39771  cdlemblem  39775  paddasslem2  39803  pmodl42N  39833  hlmod1i  39838  atmod1i1m  39840  atmod2i1  39843  atmod2i2  39844  atmod3i1  39846  llnexchb2lem  39850  dalawlem2  39854  dalawlem3  39855  dalawlem6  39858  dalawlem7  39859  dalawlem11  39863  dalawlem12  39864  pexmidlem3N  39954  lhpexle3lem  39993  lhpmcvr3  40007  lhp2at0  40014  lhpelim  40019  lhpmod2i2  40020  lhpmod6i1  40021  4atexlempns  40044  4atexlemunv  40048  4atexlemc  40051  4atexlemnclw  40052  4atexlemex2  40053  4atexlemex6  40056  4atex  40058  4atex3  40063  trljat1  40148  trljat2  40149  ltrnatlw  40165  trlval4  40170  cdlemc1  40173  cdlemc3  40175  cdlemc6  40178  cdlemd3  40182  cdlemd4  40183  cdlemd5  40184  cdlemd6  40185  cdlemd7  40186  cdleme00a  40191  cdleme0cp  40196  cdleme0cq  40197  cdleme0e  40199  cdleme02N  40204  cdleme0ex2N  40206  cdleme0moN  40207  cdleme1  40209  cdleme2  40210  cdleme3e  40214  cdleme3g  40216  cdleme3h  40217  cdleme4  40220  cdleme5  40222  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme8  40232  cdleme9  40235  cdleme10  40236  cdleme16aN  40241  cdleme11a  40242  cdleme11c  40243  cdleme11dN  40244  cdleme11e  40245  cdleme11g  40247  cdleme11h  40248  cdleme11j  40249  cdleme11k  40250  cdleme12  40253  cdleme15a  40256  cdleme15b  40257  cdleme16b  40261  cdleme17c  40270  cdleme0nex  40272  cdleme18d  40277  cdlemednpq  40281  cdleme20zN  40283  cdleme20y  40284  cdleme19a  40285  cdleme19d  40288  cdleme20aN  40291  cdleme20c  40293  cdleme20i  40299  cdleme20j  40300  cdleme21a  40307  cdleme21b  40308  cdleme21c  40309  cdleme21ct  40311  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme22f2  40329  cdleme22g  40330  cdleme23c  40333  cdleme41sn3a  40415  cdleme32le  40429  cdleme35b  40432  cdleme35c  40433  cdleme35d  40434  cdleme35e  40435  cdleme36a  40442  cdleme37m  40444  cdleme39a  40447  cdleme42a  40453  cdleme17d2  40477  cdlemeg46frv  40507  cdlemeg46rgv  40510  cdlemf1  40543  cdlemg2fv2  40582  cdlemg2l  40585  cdlemg2m  40586  cdlemg4d  40595  cdlemg4e  40596  cdlemg4f  40597  cdlemg4  40599  cdlemg6c  40602  cdlemg9a  40614  cdlemg10bALTN  40618  cdlemg12a  40625  cdlemg13  40634  cdlemg14f  40635  cdlemg14g  40636  cdlemg17i  40651  cdlemg17pq  40654  cdlemg19  40666  cdlemg21  40668  cdlemg27b  40678  cdlemg33c  40690  cdlemg33d  40691  trlcoabs2N  40704  cdlemg43  40712  cdlemg44b  40714  cdlemg44  40715  cdlemh1  40797  cdlemh2  40798  cdlemi1  40800  tendo0mul  40808  tendo0mulr  40809  cdlemk4  40816  cdlemk9  40821  cdlemk9bN  40822  cdlemk14  40836  cdlemkfid1N  40903  cdlemkid1  40904  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk55a  40941  cdlemk55u  40948  cdlemk39u  40950  cdlemk19u  40952  cdlemk56  40953  cdleml8  40965  dia2dimlem1  41046  dia2dimlem2  41047  dia2dimlem3  41048  cdlemn10  41188  dihjust  41199  dihord1  41200  dihlsscpre  41216  dihvalcqpre  41217  dihglbcpreN  41282  dihmeetlem5  41290  dihmeetlem7N  41292  dihjatc1  41293  gpg3nbgrvtxlem  47957  lincreslvec3  48327  isldepslvec2  48330