Theorem syl132anc 1384

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  drsdirfi  17551  eengtrkg  26775  eengtrkge  26776  linds2eq  30945  qqhval2lem  31226  qqhghm  31233  qqhrhm  31234  btwncomim  33478  btwnswapid  33482  btwnintr  33484  btwnexch3  33485  btwnxfr  33521  linecgrand  33547  btwnconn1lem13  33564  seglecgr12im  33575  segletr  33579  linethru  33618  lshpkrlem5  36254  omlmod1i2N  36400  omlspjN  36401  atcmp  36451  atexchcvrN  36580  atbtwn  36586  1cvratlt  36614  2atjlej  36619  hlatexch3N  36620  hlatexch4  36621  atcvrlln2  36659  atcvrlln  36660  llncmp  36662  llncvrlpln  36698  lplncmp  36702  lplnexllnN  36704  2llnjaN  36706  4atlem11  36749  lplncvrlvol  36756  lvolcmp  36757  dalem1  36799  dalem2  36801  dalem24  36837  dalem25  36838  dalem42  36854  lncvrat  36922  2llnma3r  36928  lhp2lt  37141  4atexlemswapqr  37203  4atexlemtlw  37207  4atexlemntlpq  37208  4atexlemc  37209  4atexlemnclw  37210  4atexlemcnd  37212  4atex2  37217  cdlemd1  37338  cdlemd7  37344  cdleme0e  37357  cdleme7c  37385  cdleme7d  37386  cdleme7e  37387  cdleme7ga  37388  cdleme7  37389  cdleme16aN  37399  cdleme11c  37401  cdleme11e  37403  cdleme11l  37409  cdleme11  37410  cdleme14  37413  cdleme15a  37414  cdleme16b  37419  cdleme16c  37420  cdleme16d  37421  cdleme16e  37422  cdleme16f  37423  cdleme18b  37432  cdleme19d  37446  cdleme20d  37452  cdleme20f  37454  cdleme20h  37456  cdleme20l1  37460  cdleme20l2  37461  cdleme20l  37462  cdleme21a  37465  cdleme21b  37466  cdleme21c  37467  cdleme21ct  37469  cdleme22f2  37487  cdleme22g  37488  cdlemefr32sn2aw  37544  cdleme43fsv1snlem  37560  cdleme32b  37582  cdleme35a  37588  cdleme35f  37594  cdleme36m  37601  cdleme37m  37602  cdleme42k  37624  cdleme43bN  37630  cdleme17d2  37635  cdlemeg46req  37669  cdlemeg46gfv  37670  cdlemeg46gfre  37672  cdleme50trn2a  37690  cdleme50trn2  37691  cdlemg8b  37768  cdlemg10a  37780  cdlemg12d  37786  cdlemg13a  37791  cdlemg15  37796  cdlemg16z  37799  cdlemg18b  37819  cdlemg18c  37820  cdlemg18  37822  cdlemg27b  37836  cdlemg33  37851  cdlemg42  37869  trljco  37880  cdlemj3  37963  tendoid0  37965  cdlemk3  37973  cdlemk22  38033  cdlemk36  38053  cdlemkfid3N  38065  cdlemk47  38089  cdlemk48  38090  cdlemk49  38091  cdlemk50  38092  cdlemk51  38093  cdlemk52  38094  cdlemk53a  38095  cdlemk53b  38096  cdlemk53  38097  cdlemk54  38098  cdlemk55  38101  cdlemk35u  38104  cdlemk39u1  38107  cdleml3N  38118