Theorem syl132anc 1409

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 400  df-3an 1101

This theorem is referenced by:  drsdirfi  18339  eengtrkg  29189  eengtrkge  29190  mgcmnt1  33172  mgcmnt2  33173  mgcmntco  33174  dfmgc2lem  33175  gsumtp  33246  linds2eq  33569  evl1deg1  33774  evl1deg3  33776  qqhval2lem  34280  qqhghm  34287  qqhrhm  34288  btwncomim  36368  btwnswapid  36372  btwnintr  36374  btwnexch3  36375  btwnxfr  36411  linecgrand  36437  btwnconn1lem13  36454  seglecgr12im  36465  segletr  36469  linethru  36508  lshpkrlem5  39743  omlmod1i2N  39889  omlspjN  39890  atcmp  39940  atexchcvrN  40069  atbtwn  40075  1cvratlt  40103  2atjlej  40108  hlatexch3N  40109  hlatexch4  40110  atcvrlln2  40148  atcvrlln  40149  llncmp  40151  llncvrlpln  40187  lplncmp  40191  lplnexllnN  40193  2llnjaN  40195  4atlem11  40238  lplncvrlvol  40245  lvolcmp  40246  dalem1  40288  dalem2  40290  dalem24  40326  dalem25  40327  dalem42  40343  lncvrat  40411  2llnma3r  40417  lhp2lt  40630  4atexlemswapqr  40692  4atexlemtlw  40696  4atexlemntlpq  40697  4atexlemc  40698  4atexlemnclw  40699  4atexlemcnd  40701  4atex2  40706  cdlemd1  40827  cdlemd7  40833  cdleme0e  40846  cdleme7c  40874  cdleme7d  40875  cdleme7e  40876  cdleme7ga  40877  cdleme7  40878  cdleme16aN  40888  cdleme11c  40890  cdleme11e  40892  cdleme11l  40898  cdleme11  40899  cdleme14  40902  cdleme15a  40903  cdleme16b  40908  cdleme16c  40909  cdleme16d  40910  cdleme16e  40911  cdleme16f  40912  cdleme18b  40921  cdleme19d  40935  cdleme20d  40941  cdleme20f  40943  cdleme20h  40945  cdleme20l1  40949  cdleme20l2  40950  cdleme20l  40951  cdleme21a  40954  cdleme21b  40955  cdleme21c  40956  cdleme21ct  40958  cdleme22f2  40976  cdleme22g  40977  cdlemefr32sn2aw  41033  cdleme43fsv1snlem  41049  cdleme32b  41071  cdleme35a  41077  cdleme35f  41083  cdleme36m  41090  cdleme37m  41091  cdleme42k  41113  cdleme43bN  41119  cdleme17d2  41124  cdlemeg46req  41158  cdlemeg46gfv  41159  cdlemeg46gfre  41161  cdleme50trn2a  41179  cdleme50trn2  41180  cdlemg8b  41257  cdlemg10a  41269  cdlemg12d  41275  cdlemg13a  41280  cdlemg15  41285  cdlemg16z  41288  cdlemg18b  41308  cdlemg18c  41309  cdlemg18  41311  cdlemg27b  41325  cdlemg33  41340  cdlemg42  41358  trljco  41369  cdlemj3  41452  tendoid0  41454  cdlemk3  41462  cdlemk22  41522  cdlemk36  41542  cdlemkfid3N  41554  cdlemk47  41578  cdlemk48  41579  cdlemk49  41580  cdlemk50  41581  cdlemk51  41582  cdlemk52  41583  cdlemk53a  41584  cdlemk53b  41585  cdlemk53  41586  cdlemk54  41587  cdlemk55  41590  cdlemk35u  41593  cdlemk39u1  41596  cdleml3N  41607  m1modnep2mod  47957  ssccatid  49698