Theorem syl132anc 1414

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 520	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl132anc.7	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl131anc 1409	1 ⊢ (𝜑 → 𝜎)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  drsdirfi  18367  eengtrkg  29347  eengtrkge  29348  mgcmnt1  33321  mgcmnt2  33322  mgcmntco  33323  dfmgc2lem  33324  gsumtp  33393  linds2eq  33703  evl1deg1  33875  evl1deg3  33877  qqhval2lem  34380  qqhghm  34387  qqhrhm  34388  btwncomim  36513  btwnswapid  36517  btwnintr  36519  btwnexch3  36520  btwnxfr  36556  linecgrand  36582  btwnconn1lem13  36599  seglecgr12im  36610  segletr  36614  linethru  36653  lshpkrlem5  39916  omlmod1i2N  40062  omlspjN  40063  atcmp  40113  atexchcvrN  40242  atbtwn  40248  1cvratlt  40276  2atjlej  40281  hlatexch3N  40282  hlatexch4  40283  atcvrlln2  40321  atcvrlln  40322  llncmp  40324  llncvrlpln  40360  lplncmp  40364  lplnexllnN  40366  2llnjaN  40368  4atlem11  40411  lplncvrlvol  40418  lvolcmp  40419  dalem1  40461  dalem2  40463  dalem24  40499  dalem25  40500  dalem42  40516  lncvrat  40584  2llnma3r  40590  lhp2lt  40803  4atexlemswapqr  40865  4atexlemtlw  40869  4atexlemntlpq  40870  4atexlemc  40871  4atexlemnclw  40872  4atexlemcnd  40874  4atex2  40879  cdlemd1  41000  cdlemd7  41006  cdleme0e  41019  cdleme7c  41047  cdleme7d  41048  cdleme7e  41049  cdleme7ga  41050  cdleme7  41051  cdleme16aN  41061  cdleme11c  41063  cdleme11e  41065  cdleme11l  41071  cdleme11  41072  cdleme14  41075  cdleme15a  41076  cdleme16b  41081  cdleme16c  41082  cdleme16d  41083  cdleme16e  41084  cdleme16f  41085  cdleme18b  41094  cdleme19d  41108  cdleme20d  41114  cdleme20f  41116  cdleme20h  41118  cdleme20l1  41122  cdleme20l2  41123  cdleme20l  41124  cdleme21a  41127  cdleme21b  41128  cdleme21c  41129  cdleme21ct  41131  cdleme22f2  41149  cdleme22g  41150  cdlemefr32sn2aw  41206  cdleme43fsv1snlem  41222  cdleme32b  41244  cdleme35a  41250  cdleme35f  41256  cdleme36m  41263  cdleme37m  41264  cdleme42k  41286  cdleme43bN  41292  cdleme17d2  41297  cdlemeg46req  41331  cdlemeg46gfv  41332  cdlemeg46gfre  41334  cdleme50trn2a  41352  cdleme50trn2  41353  cdlemg8b  41430  cdlemg10a  41442  cdlemg12d  41448  cdlemg13a  41453  cdlemg15  41458  cdlemg16z  41461  cdlemg18b  41481  cdlemg18c  41482  cdlemg18  41484  cdlemg27b  41498  cdlemg33  41513  cdlemg42  41531  trljco  41542  cdlemj3  41625  tendoid0  41627  cdlemk3  41635  cdlemk22  41695  cdlemk36  41715  cdlemkfid3N  41727  cdlemk47  41751  cdlemk48  41752  cdlemk49  41753  cdlemk50  41754  cdlemk51  41755  cdlemk52  41756  cdlemk53a  41757  cdlemk53b  41758  cdlemk53  41759  cdlemk54  41760  cdlemk55  41763  cdlemk35u  41766  cdlemk39u1  41769  cdleml3N  41780  m1modnep2mod  48123  ssccatid  49878