Theorem syl132anc 1336

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

Hypotheses

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

Assertion

Ref	Expression
syl132anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl132anc

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  drsdirfi  16761  eengtrkg  25665  eengtrkge  25666  qqhval2lem  29353  qqhghm  29360  qqhrhm  29361  btwncomim  31290  btwnswapid  31294  btwnintr  31296  btwnexch3  31297  btwnxfr  31333  linecgrand  31359  btwnconn1lem13  31376  seglecgr12im  31387  segletr  31391  linethru  31430  lshpkrlem5  33419  omlmod1i2N  33565  omlspjN  33566  atcmp  33616  atexchcvrN  33744  atbtwn  33750  1cvratlt  33778  2atjlej  33783  hlatexch3N  33784  hlatexch4  33785  atcvrlln2  33823  atcvrlln  33824  llncmp  33826  llncvrlpln  33862  lplncmp  33866  lplnexllnN  33868  2llnjaN  33870  4atlem11  33913  lplncvrlvol  33920  lvolcmp  33921  dalem1  33963  dalem2  33965  dalem24  34001  dalem25  34002  dalem42  34018  lncvrat  34086  2llnma3r  34092  lhp2lt  34305  4atexlemswapqr  34367  4atexlemtlw  34371  4atexlemntlpq  34372  4atexlemc  34373  4atexlemnclw  34374  4atexlemcnd  34376  4atex2  34381  cdlemd1  34503  cdlemd7  34509  cdleme0e  34522  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme16aN  34564  cdleme11c  34566  cdleme11e  34568  cdleme11l  34574  cdleme11  34575  cdleme14  34578  cdleme15a  34579  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme18b  34597  cdleme19d  34612  cdleme20d  34618  cdleme20f  34620  cdleme20h  34622  cdleme20l1  34626  cdleme20l2  34627  cdleme20l  34628  cdleme21a  34631  cdleme21b  34632  cdleme21c  34633  cdleme21ct  34635  cdleme22f2  34653  cdleme22g  34654  cdlemefr32sn2aw  34710  cdleme43fsv1snlem  34726  cdleme32b  34748  cdleme35a  34754  cdleme35f  34760  cdleme36m  34767  cdleme37m  34768  cdleme42k  34790  cdleme43bN  34796  cdleme17d2  34801  cdlemeg46req  34835  cdlemeg46gfv  34836  cdlemeg46gfre  34838  cdleme50trn2a  34856  cdleme50trn2  34857  cdlemg8b  34934  cdlemg10a  34946  cdlemg12d  34952  cdlemg13a  34957  cdlemg15  34962  cdlemg16z  34965  cdlemg18b  34985  cdlemg18c  34986  cdlemg18  34988  cdlemg27b  35002  cdlemg33  35017  cdlemg42  35035  trljco  35046  cdlemj3  35129  tendoid0  35131  cdlemk3  35139  cdlemk22  35199  cdlemk36  35219  cdlemkfid3N  35231  cdlemk47  35255  cdlemk48  35256  cdlemk49  35257  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  cdlemk53a  35261  cdlemk53b  35262  cdlemk53  35263  cdlemk54  35264  cdlemk55  35267  cdlemk35u  35270  cdlemk39u1  35273  cdleml3N  35284