Theorem syl132anc 1387

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  drsdirfi  18032  eengtrkg  27363  eengtrkge  27364  mgcmnt1  31279  mgcmnt2  31280  mgcmntco  31281  dfmgc2lem  31282  linds2eq  31584  qqhval2lem  31940  qqhghm  31947  qqhrhm  31948  btwncomim  34324  btwnswapid  34328  btwnintr  34330  btwnexch3  34331  btwnxfr  34367  linecgrand  34393  btwnconn1lem13  34410  seglecgr12im  34421  segletr  34425  linethru  34464  lshpkrlem5  37135  omlmod1i2N  37281  omlspjN  37282  atcmp  37332  atexchcvrN  37461  atbtwn  37467  1cvratlt  37495  2atjlej  37500  hlatexch3N  37501  hlatexch4  37502  atcvrlln2  37540  atcvrlln  37541  llncmp  37543  llncvrlpln  37579  lplncmp  37583  lplnexllnN  37585  2llnjaN  37587  4atlem11  37630  lplncvrlvol  37637  lvolcmp  37638  dalem1  37680  dalem2  37682  dalem24  37718  dalem25  37719  dalem42  37735  lncvrat  37803  2llnma3r  37809  lhp2lt  38022  4atexlemswapqr  38084  4atexlemtlw  38088  4atexlemntlpq  38089  4atexlemc  38090  4atexlemnclw  38091  4atexlemcnd  38093  4atex2  38098  cdlemd1  38219  cdlemd7  38225  cdleme0e  38238  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme16aN  38280  cdleme11c  38282  cdleme11e  38284  cdleme11l  38290  cdleme11  38291  cdleme14  38294  cdleme15a  38295  cdleme16b  38300  cdleme16c  38301  cdleme16d  38302  cdleme16e  38303  cdleme16f  38304  cdleme18b  38313  cdleme19d  38327  cdleme20d  38333  cdleme20f  38335  cdleme20h  38337  cdleme20l1  38341  cdleme20l2  38342  cdleme20l  38343  cdleme21a  38346  cdleme21b  38347  cdleme21c  38348  cdleme21ct  38350  cdleme22f2  38368  cdleme22g  38369  cdlemefr32sn2aw  38425  cdleme43fsv1snlem  38441  cdleme32b  38463  cdleme35a  38469  cdleme35f  38475  cdleme36m  38482  cdleme37m  38483  cdleme42k  38505  cdleme43bN  38511  cdleme17d2  38516  cdlemeg46req  38550  cdlemeg46gfv  38551  cdlemeg46gfre  38553  cdleme50trn2a  38571  cdleme50trn2  38572  cdlemg8b  38649  cdlemg10a  38661  cdlemg12d  38667  cdlemg13a  38672  cdlemg15  38677  cdlemg16z  38680  cdlemg18b  38700  cdlemg18c  38701  cdlemg18  38703  cdlemg27b  38717  cdlemg33  38732  cdlemg42  38750  trljco  38761  cdlemj3  38844  tendoid0  38846  cdlemk3  38854  cdlemk22  38914  cdlemk36  38934  cdlemkfid3N  38946  cdlemk47  38970  cdlemk48  38971  cdlemk49  38972  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  cdlemk53a  38976  cdlemk53b  38977  cdlemk53  38978  cdlemk54  38979  cdlemk55  38982  cdlemk35u  38985  cdlemk39u1  38988  cdleml3N  38999