Theorem syl132anc 1391

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  drsdirfi  18240  eengtrkg  29071  eengtrkge  29072  mgcmnt1  33084  mgcmnt2  33085  mgcmntco  33086  dfmgc2lem  33087  gsumtp  33157  linds2eq  33473  evl1deg1  33668  evl1deg3  33670  qqhval2lem  34158  qqhghm  34165  qqhrhm  34166  btwncomim  36226  btwnswapid  36230  btwnintr  36232  btwnexch3  36233  btwnxfr  36269  linecgrand  36295  btwnconn1lem13  36312  seglecgr12im  36323  segletr  36327  linethru  36366  lshpkrlem5  39484  omlmod1i2N  39630  omlspjN  39631  atcmp  39681  atexchcvrN  39810  atbtwn  39816  1cvratlt  39844  2atjlej  39849  hlatexch3N  39850  hlatexch4  39851  atcvrlln2  39889  atcvrlln  39890  llncmp  39892  llncvrlpln  39928  lplncmp  39932  lplnexllnN  39934  2llnjaN  39936  4atlem11  39979  lplncvrlvol  39986  lvolcmp  39987  dalem1  40029  dalem2  40031  dalem24  40067  dalem25  40068  dalem42  40084  lncvrat  40152  2llnma3r  40158  lhp2lt  40371  4atexlemswapqr  40433  4atexlemtlw  40437  4atexlemntlpq  40438  4atexlemc  40439  4atexlemnclw  40440  4atexlemcnd  40442  4atex2  40447  cdlemd1  40568  cdlemd7  40574  cdleme0e  40587  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme16aN  40629  cdleme11c  40631  cdleme11e  40633  cdleme11l  40639  cdleme11  40640  cdleme14  40643  cdleme15a  40644  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme16e  40652  cdleme16f  40653  cdleme18b  40662  cdleme19d  40676  cdleme20d  40682  cdleme20f  40684  cdleme20h  40686  cdleme20l1  40690  cdleme20l2  40691  cdleme20l  40692  cdleme21a  40695  cdleme21b  40696  cdleme21c  40697  cdleme21ct  40699  cdleme22f2  40717  cdleme22g  40718  cdlemefr32sn2aw  40774  cdleme43fsv1snlem  40790  cdleme32b  40812  cdleme35a  40818  cdleme35f  40824  cdleme36m  40831  cdleme37m  40832  cdleme42k  40854  cdleme43bN  40860  cdleme17d2  40865  cdlemeg46req  40899  cdlemeg46gfv  40900  cdlemeg46gfre  40902  cdleme50trn2a  40920  cdleme50trn2  40921  cdlemg8b  40998  cdlemg10a  41010  cdlemg12d  41016  cdlemg13a  41021  cdlemg15  41026  cdlemg16z  41029  cdlemg18b  41049  cdlemg18c  41050  cdlemg18  41052  cdlemg27b  41066  cdlemg33  41081  cdlemg42  41099  trljco  41110  cdlemj3  41193  tendoid0  41195  cdlemk3  41203  cdlemk22  41263  cdlemk36  41283  cdlemkfid3N  41295  cdlemk47  41319  cdlemk48  41320  cdlemk49  41321  cdlemk50  41322  cdlemk51  41323  cdlemk52  41324  cdlemk53a  41325  cdlemk53b  41326  cdlemk53  41327  cdlemk54  41328  cdlemk55  41331  cdlemk35u  41334  cdlemk39u1  41337  cdleml3N  41348  m1modnep2mod  47706  ssccatid  49425