Theorem syl132anc 1390

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 1385	1 ⊢ (𝜑 → 𝜎)

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

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 1088

This theorem is referenced by:  drsdirfi  18213  eengtrkg  28966  eengtrkge  28967  mgcmnt1  32980  mgcmnt2  32981  mgcmntco  32982  dfmgc2lem  32983  gsumtp  33045  linds2eq  33353  evl1deg1  33546  evl1deg3  33548  qqhval2lem  34015  qqhghm  34022  qqhrhm  34023  btwncomim  36078  btwnswapid  36082  btwnintr  36084  btwnexch3  36085  btwnxfr  36121  linecgrand  36147  btwnconn1lem13  36164  seglecgr12im  36175  segletr  36179  linethru  36218  lshpkrlem5  39234  omlmod1i2N  39380  omlspjN  39381  atcmp  39431  atexchcvrN  39560  atbtwn  39566  1cvratlt  39594  2atjlej  39599  hlatexch3N  39600  hlatexch4  39601  atcvrlln2  39639  atcvrlln  39640  llncmp  39642  llncvrlpln  39678  lplncmp  39682  lplnexllnN  39684  2llnjaN  39686  4atlem11  39729  lplncvrlvol  39736  lvolcmp  39737  dalem1  39779  dalem2  39781  dalem24  39817  dalem25  39818  dalem42  39834  lncvrat  39902  2llnma3r  39908  lhp2lt  40121  4atexlemswapqr  40183  4atexlemtlw  40187  4atexlemntlpq  40188  4atexlemc  40189  4atexlemnclw  40190  4atexlemcnd  40192  4atex2  40197  cdlemd1  40318  cdlemd7  40324  cdleme0e  40337  cdleme7c  40365  cdleme7d  40366  cdleme7e  40367  cdleme7ga  40368  cdleme7  40369  cdleme16aN  40379  cdleme11c  40381  cdleme11e  40383  cdleme11l  40389  cdleme11  40390  cdleme14  40393  cdleme15a  40394  cdleme16b  40399  cdleme16c  40400  cdleme16d  40401  cdleme16e  40402  cdleme16f  40403  cdleme18b  40412  cdleme19d  40426  cdleme20d  40432  cdleme20f  40434  cdleme20h  40436  cdleme20l1  40440  cdleme20l2  40441  cdleme20l  40442  cdleme21a  40445  cdleme21b  40446  cdleme21c  40447  cdleme21ct  40449  cdleme22f2  40467  cdleme22g  40468  cdlemefr32sn2aw  40524  cdleme43fsv1snlem  40540  cdleme32b  40562  cdleme35a  40568  cdleme35f  40574  cdleme36m  40581  cdleme37m  40582  cdleme42k  40604  cdleme43bN  40610  cdleme17d2  40615  cdlemeg46req  40649  cdlemeg46gfv  40650  cdlemeg46gfre  40652  cdleme50trn2a  40670  cdleme50trn2  40671  cdlemg8b  40748  cdlemg10a  40760  cdlemg12d  40766  cdlemg13a  40771  cdlemg15  40776  cdlemg16z  40779  cdlemg18b  40799  cdlemg18c  40800  cdlemg18  40802  cdlemg27b  40816  cdlemg33  40831  cdlemg42  40849  trljco  40860  cdlemj3  40943  tendoid0  40945  cdlemk3  40953  cdlemk22  41013  cdlemk36  41033  cdlemkfid3N  41045  cdlemk47  41069  cdlemk48  41070  cdlemk49  41071  cdlemk50  41072  cdlemk51  41073  cdlemk52  41074  cdlemk53a  41075  cdlemk53b  41076  cdlemk53  41077  cdlemk54  41078  cdlemk55  41081  cdlemk35u  41084  cdlemk39u1  41087  cdleml3N  41098  m1modnep2mod  47477  ssccatid  49198