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  18229  eengtrkg  28949  eengtrkge  28950  mgcmnt1  32947  mgcmnt2  32948  mgcmntco  32949  dfmgc2lem  32950  gsumtp  33024  linds2eq  33328  evl1deg1  33521  evl1deg3  33523  qqhval2lem  33947  qqhghm  33954  qqhrhm  33955  btwncomim  35986  btwnswapid  35990  btwnintr  35992  btwnexch3  35993  btwnxfr  36029  linecgrand  36055  btwnconn1lem13  36072  seglecgr12im  36083  segletr  36087  linethru  36126  lshpkrlem5  39092  omlmod1i2N  39238  omlspjN  39239  atcmp  39289  atexchcvrN  39419  atbtwn  39425  1cvratlt  39453  2atjlej  39458  hlatexch3N  39459  hlatexch4  39460  atcvrlln2  39498  atcvrlln  39499  llncmp  39501  llncvrlpln  39537  lplncmp  39541  lplnexllnN  39543  2llnjaN  39545  4atlem11  39588  lplncvrlvol  39595  lvolcmp  39596  dalem1  39638  dalem2  39640  dalem24  39676  dalem25  39677  dalem42  39693  lncvrat  39761  2llnma3r  39767  lhp2lt  39980  4atexlemswapqr  40042  4atexlemtlw  40046  4atexlemntlpq  40047  4atexlemc  40048  4atexlemnclw  40049  4atexlemcnd  40051  4atex2  40056  cdlemd1  40177  cdlemd7  40183  cdleme0e  40196  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme16aN  40238  cdleme11c  40240  cdleme11e  40242  cdleme11l  40248  cdleme11  40249  cdleme14  40252  cdleme15a  40253  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme16e  40261  cdleme16f  40262  cdleme18b  40271  cdleme19d  40285  cdleme20d  40291  cdleme20f  40293  cdleme20h  40295  cdleme20l1  40299  cdleme20l2  40300  cdleme20l  40301  cdleme21a  40304  cdleme21b  40305  cdleme21c  40306  cdleme21ct  40308  cdleme22f2  40326  cdleme22g  40327  cdlemefr32sn2aw  40383  cdleme43fsv1snlem  40399  cdleme32b  40421  cdleme35a  40427  cdleme35f  40433  cdleme36m  40440  cdleme37m  40441  cdleme42k  40463  cdleme43bN  40469  cdleme17d2  40474  cdlemeg46req  40508  cdlemeg46gfv  40509  cdlemeg46gfre  40511  cdleme50trn2a  40529  cdleme50trn2  40530  cdlemg8b  40607  cdlemg10a  40619  cdlemg12d  40625  cdlemg13a  40630  cdlemg15  40635  cdlemg16z  40638  cdlemg18b  40658  cdlemg18c  40659  cdlemg18  40661  cdlemg27b  40675  cdlemg33  40690  cdlemg42  40708  trljco  40719  cdlemj3  40802  tendoid0  40804  cdlemk3  40812  cdlemk22  40872  cdlemk36  40892  cdlemkfid3N  40904  cdlemk47  40928  cdlemk48  40929  cdlemk49  40930  cdlemk50  40931  cdlemk51  40932  cdlemk52  40933  cdlemk53a  40934  cdlemk53b  40935  cdlemk53  40936  cdlemk54  40937  cdlemk55  40940  cdlemk35u  40943  cdlemk39u1  40946  cdleml3N  40957  m1modnep2mod  47337  ssccatid  49058