Theorem syl132anc 1397

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  drsdirfi  18266  eengtrkg  29075  eengtrkge  29076  mgcmnt1  33073  mgcmnt2  33074  mgcmntco  33075  dfmgc2lem  33076  gsumtp  33147  linds2eq  33466  evl1deg1  33669  evl1deg3  33671  qqhval2lem  34175  qqhghm  34182  qqhrhm  34183  btwncomim  36254  btwnswapid  36258  btwnintr  36260  btwnexch3  36261  btwnxfr  36297  linecgrand  36323  btwnconn1lem13  36340  seglecgr12im  36351  segletr  36355  linethru  36394  lshpkrlem5  39619  omlmod1i2N  39765  omlspjN  39766  atcmp  39816  atexchcvrN  39945  atbtwn  39951  1cvratlt  39979  2atjlej  39984  hlatexch3N  39985  hlatexch4  39986  atcvrlln2  40024  atcvrlln  40025  llncmp  40027  llncvrlpln  40063  lplncmp  40067  lplnexllnN  40069  2llnjaN  40071  4atlem11  40114  lplncvrlvol  40121  lvolcmp  40122  dalem1  40164  dalem2  40166  dalem24  40202  dalem25  40203  dalem42  40219  lncvrat  40287  2llnma3r  40293  lhp2lt  40506  4atexlemswapqr  40568  4atexlemtlw  40572  4atexlemntlpq  40573  4atexlemc  40574  4atexlemnclw  40575  4atexlemcnd  40577  4atex2  40582  cdlemd1  40703  cdlemd7  40709  cdleme0e  40722  cdleme7c  40750  cdleme7d  40751  cdleme7e  40752  cdleme7ga  40753  cdleme7  40754  cdleme16aN  40764  cdleme11c  40766  cdleme11e  40768  cdleme11l  40774  cdleme11  40775  cdleme14  40778  cdleme15a  40779  cdleme16b  40784  cdleme16c  40785  cdleme16d  40786  cdleme16e  40787  cdleme16f  40788  cdleme18b  40797  cdleme19d  40811  cdleme20d  40817  cdleme20f  40819  cdleme20h  40821  cdleme20l1  40825  cdleme20l2  40826  cdleme20l  40827  cdleme21a  40830  cdleme21b  40831  cdleme21c  40832  cdleme21ct  40834  cdleme22f2  40852  cdleme22g  40853  cdlemefr32sn2aw  40909  cdleme43fsv1snlem  40925  cdleme32b  40947  cdleme35a  40953  cdleme35f  40959  cdleme36m  40966  cdleme37m  40967  cdleme42k  40989  cdleme43bN  40995  cdleme17d2  41000  cdlemeg46req  41034  cdlemeg46gfv  41035  cdlemeg46gfre  41037  cdleme50trn2a  41055  cdleme50trn2  41056  cdlemg8b  41133  cdlemg10a  41145  cdlemg12d  41151  cdlemg13a  41156  cdlemg15  41161  cdlemg16z  41164  cdlemg18b  41184  cdlemg18c  41185  cdlemg18  41187  cdlemg27b  41201  cdlemg33  41216  cdlemg42  41234  trljco  41245  cdlemj3  41328  tendoid0  41330  cdlemk3  41338  cdlemk22  41398  cdlemk36  41418  cdlemkfid3N  41430  cdlemk47  41454  cdlemk48  41455  cdlemk49  41456  cdlemk50  41457  cdlemk51  41458  cdlemk52  41459  cdlemk53a  41460  cdlemk53b  41461  cdlemk53  41462  cdlemk54  41463  cdlemk55  41466  cdlemk35u  41469  cdlemk39u1  41472  cdleml3N  41483  m1modnep2mod  47833  ssccatid  49574