Theorem syl132anc 1415

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  drsdirfi  18426  eengtrkg  29483  eengtrkge  29484  mgcmnt1  33472  mgcmnt2  33473  mgcmntco  33474  dfmgc2lem  33475  gsumtp  33544  linds2eq  33855  evl1deg1  34027  evl1deg3  34029  qqhval2lem  34532  qqhghm  34539  qqhrhm  34540  btwncomim  36694  btwnswapid  36698  btwnintr  36700  btwnexch3  36701  btwnxfr  36737  linecgrand  36763  btwnconn1lem13  36780  seglecgr12im  36791  segletr  36795  linethru  36834  lshpkrlem5  40085  omlmod1i2N  40231  omlspjN  40232  atcmp  40282  atexchcvrN  40411  atbtwn  40417  1cvratlt  40445  2atjlej  40450  hlatexch3N  40451  hlatexch4  40452  atcvrlln2  40490  atcvrlln  40491  llncmp  40493  llncvrlpln  40529  lplncmp  40533  lplnexllnN  40535  2llnjaN  40537  4atlem11  40580  lplncvrlvol  40587  lvolcmp  40588  dalem1  40630  dalem2  40632  dalem24  40668  dalem25  40669  dalem42  40685  lncvrat  40753  2llnma3r  40759  lhp2lt  40972  4atexlemswapqr  41034  4atexlemtlw  41038  4atexlemntlpq  41039  4atexlemc  41040  4atexlemnclw  41041  4atexlemcnd  41043  4atex2  41048  cdlemd1  41169  cdlemd7  41175  cdleme0e  41188  cdleme7c  41216  cdleme7d  41217  cdleme7e  41218  cdleme7ga  41219  cdleme7  41220  cdleme16aN  41230  cdleme11c  41232  cdleme11e  41234  cdleme11l  41240  cdleme11  41241  cdleme14  41244  cdleme15a  41245  cdleme16b  41250  cdleme16c  41251  cdleme16d  41252  cdleme16e  41253  cdleme16f  41254  cdleme18b  41263  cdleme19d  41277  cdleme20d  41283  cdleme20f  41285  cdleme20h  41287  cdleme20l1  41291  cdleme20l2  41292  cdleme20l  41293  cdleme21a  41296  cdleme21b  41297  cdleme21c  41298  cdleme21ct  41300  cdleme22f2  41318  cdleme22g  41319  cdlemefr32sn2aw  41375  cdleme43fsv1snlem  41391  cdleme32b  41413  cdleme35a  41419  cdleme35f  41425  cdleme36m  41432  cdleme37m  41433  cdleme42k  41455  cdleme43bN  41461  cdleme17d2  41466  cdlemeg46req  41500  cdlemeg46gfv  41501  cdlemeg46gfre  41503  cdleme50trn2a  41521  cdleme50trn2  41522  cdlemg8b  41599  cdlemg10a  41611  cdlemg12d  41617  cdlemg13a  41622  cdlemg15  41627  cdlemg16z  41630  cdlemg18b  41650  cdlemg18c  41651  cdlemg18  41653  cdlemg27b  41667  cdlemg33  41682  cdlemg42  41700  trljco  41711  cdlemj3  41794  tendoid0  41796  cdlemk3  41804  cdlemk22  41864  cdlemk36  41884  cdlemkfid3N  41896  cdlemk47  41920  cdlemk48  41921  cdlemk49  41922  cdlemk50  41923  cdlemk51  41924  cdlemk52  41925  cdlemk53a  41926  cdlemk53b  41927  cdlemk53  41928  cdlemk54  41929  cdlemk55  41932  cdlemk35u  41935  cdlemk39u1  41938  cdleml3N  41949  m1modnep2mod  48344  ssccatid  50096