Theorem syl132anc 1391

Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl132anc.7	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl132anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl132anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7	5, 6	jca 511	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl132anc.7	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl131anc 1386	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  drsdirfi  18262  eengtrkg  29069  eengtrkge  29070  mgcmnt1  33067  mgcmnt2  33068  mgcmntco  33069  dfmgc2lem  33070  gsumtp  33140  linds2eq  33456  evl1deg1  33651  evl1deg3  33653  qqhval2lem  34141  qqhghm  34148  qqhrhm  34149  btwncomim  36211  btwnswapid  36215  btwnintr  36217  btwnexch3  36218  btwnxfr  36254  linecgrand  36280  btwnconn1lem13  36297  seglecgr12im  36308  segletr  36312  linethru  36351  lshpkrlem5  39574  omlmod1i2N  39720  omlspjN  39721  atcmp  39771  atexchcvrN  39900  atbtwn  39906  1cvratlt  39934  2atjlej  39939  hlatexch3N  39940  hlatexch4  39941  atcvrlln2  39979  atcvrlln  39980  llncmp  39982  llncvrlpln  40018  lplncmp  40022  lplnexllnN  40024  2llnjaN  40026  4atlem11  40069  lplncvrlvol  40076  lvolcmp  40077  dalem1  40119  dalem2  40121  dalem24  40157  dalem25  40158  dalem42  40174  lncvrat  40242  2llnma3r  40248  lhp2lt  40461  4atexlemswapqr  40523  4atexlemtlw  40527  4atexlemntlpq  40528  4atexlemc  40529  4atexlemnclw  40530  4atexlemcnd  40532  4atex2  40537  cdlemd1  40658  cdlemd7  40664  cdleme0e  40677  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme16aN  40719  cdleme11c  40721  cdleme11e  40723  cdleme11l  40729  cdleme11  40730  cdleme14  40733  cdleme15a  40734  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme18b  40752  cdleme19d  40766  cdleme20d  40772  cdleme20f  40774  cdleme20h  40776  cdleme20l1  40780  cdleme20l2  40781  cdleme20l  40782  cdleme21a  40785  cdleme21b  40786  cdleme21c  40787  cdleme21ct  40789  cdleme22f2  40807  cdleme22g  40808  cdlemefr32sn2aw  40864  cdleme43fsv1snlem  40880  cdleme32b  40902  cdleme35a  40908  cdleme35f  40914  cdleme36m  40921  cdleme37m  40922  cdleme42k  40944  cdleme43bN  40950  cdleme17d2  40955  cdlemeg46req  40989  cdlemeg46gfv  40990  cdlemeg46gfre  40992  cdleme50trn2a  41010  cdleme50trn2  41011  cdlemg8b  41088  cdlemg10a  41100  cdlemg12d  41106  cdlemg13a  41111  cdlemg15  41116  cdlemg16z  41119  cdlemg18b  41139  cdlemg18c  41140  cdlemg18  41142  cdlemg27b  41156  cdlemg33  41171  cdlemg42  41189  trljco  41200  cdlemj3  41283  tendoid0  41285  cdlemk3  41293  cdlemk22  41353  cdlemk36  41373  cdlemkfid3N  41385  cdlemk47  41409  cdlemk48  41410  cdlemk49  41411  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  cdlemk53a  41415  cdlemk53b  41416  cdlemk53  41417  cdlemk54  41418  cdlemk55  41421  cdlemk35u  41424  cdlemk39u1  41427  cdleml3N  41438  m1modnep2mod  47818  ssccatid  49559