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  18211  eengtrkg  28965  eengtrkge  28966  mgcmnt1  32971  mgcmnt2  32972  mgcmntco  32973  dfmgc2lem  32974  gsumtp  33036  linds2eq  33344  evl1deg1  33537  evl1deg3  33539  qqhval2lem  33992  qqhghm  33999  qqhrhm  34000  btwncomim  36053  btwnswapid  36057  btwnintr  36059  btwnexch3  36060  btwnxfr  36096  linecgrand  36122  btwnconn1lem13  36139  seglecgr12im  36150  segletr  36154  linethru  36193  lshpkrlem5  39159  omlmod1i2N  39305  omlspjN  39306  atcmp  39356  atexchcvrN  39485  atbtwn  39491  1cvratlt  39519  2atjlej  39524  hlatexch3N  39525  hlatexch4  39526  atcvrlln2  39564  atcvrlln  39565  llncmp  39567  llncvrlpln  39603  lplncmp  39607  lplnexllnN  39609  2llnjaN  39611  4atlem11  39654  lplncvrlvol  39661  lvolcmp  39662  dalem1  39704  dalem2  39706  dalem24  39742  dalem25  39743  dalem42  39759  lncvrat  39827  2llnma3r  39833  lhp2lt  40046  4atexlemswapqr  40108  4atexlemtlw  40112  4atexlemntlpq  40113  4atexlemc  40114  4atexlemnclw  40115  4atexlemcnd  40117  4atex2  40122  cdlemd1  40243  cdlemd7  40249  cdleme0e  40262  cdleme7c  40290  cdleme7d  40291  cdleme7e  40292  cdleme7ga  40293  cdleme7  40294  cdleme16aN  40304  cdleme11c  40306  cdleme11e  40308  cdleme11l  40314  cdleme11  40315  cdleme14  40318  cdleme15a  40319  cdleme16b  40324  cdleme16c  40325  cdleme16d  40326  cdleme16e  40327  cdleme16f  40328  cdleme18b  40337  cdleme19d  40351  cdleme20d  40357  cdleme20f  40359  cdleme20h  40361  cdleme20l1  40365  cdleme20l2  40366  cdleme20l  40367  cdleme21a  40370  cdleme21b  40371  cdleme21c  40372  cdleme21ct  40374  cdleme22f2  40392  cdleme22g  40393  cdlemefr32sn2aw  40449  cdleme43fsv1snlem  40465  cdleme32b  40487  cdleme35a  40493  cdleme35f  40499  cdleme36m  40506  cdleme37m  40507  cdleme42k  40529  cdleme43bN  40535  cdleme17d2  40540  cdlemeg46req  40574  cdlemeg46gfv  40575  cdlemeg46gfre  40577  cdleme50trn2a  40595  cdleme50trn2  40596  cdlemg8b  40673  cdlemg10a  40685  cdlemg12d  40691  cdlemg13a  40696  cdlemg15  40701  cdlemg16z  40704  cdlemg18b  40724  cdlemg18c  40725  cdlemg18  40727  cdlemg27b  40741  cdlemg33  40756  cdlemg42  40774  trljco  40785  cdlemj3  40868  tendoid0  40870  cdlemk3  40878  cdlemk22  40938  cdlemk36  40958  cdlemkfid3N  40970  cdlemk47  40994  cdlemk48  40995  cdlemk49  40996  cdlemk50  40997  cdlemk51  40998  cdlemk52  40999  cdlemk53a  41000  cdlemk53b  41001  cdlemk53  41002  cdlemk54  41003  cdlemk55  41006  cdlemk35u  41009  cdlemk39u1  41012  cdleml3N  41023  m1modnep2mod  47389  ssccatid  49110