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  18479  eengtrkg  29564  eengtrkge  29565  mgcmnt1  33553  mgcmnt2  33554  mgcmntco  33555  dfmgc2lem  33556  gsumtp  33625  linds2eq  33936  evl1deg1  34108  evl1deg3  34110  qqhval2lem  34613  qqhghm  34620  qqhrhm  34621  btwncomim  36778  btwnswapid  36782  btwnintr  36784  btwnexch3  36785  btwnxfr  36821  linecgrand  36847  btwnconn1lem13  36864  seglecgr12im  36875  segletr  36879  linethru  36918  lshpkrlem5  40172  omlmod1i2N  40318  omlspjN  40319  atcmp  40369  atexchcvrN  40498  atbtwn  40504  1cvratlt  40532  2atjlej  40537  hlatexch3N  40538  hlatexch4  40539  atcvrlln2  40577  atcvrlln  40578  llncmp  40580  llncvrlpln  40616  lplncmp  40620  lplnexllnN  40622  2llnjaN  40624  4atlem11  40667  lplncvrlvol  40674  lvolcmp  40675  dalem1  40717  dalem2  40719  dalem24  40755  dalem25  40756  dalem42  40772  lncvrat  40840  2llnma3r  40846  lhp2lt  41059  4atexlemswapqr  41121  4atexlemtlw  41125  4atexlemntlpq  41126  4atexlemc  41127  4atexlemnclw  41128  4atexlemcnd  41130  4atex2  41135  cdlemd1  41256  cdlemd7  41262  cdleme0e  41275  cdleme7c  41303  cdleme7d  41304  cdleme7e  41305  cdleme7ga  41306  cdleme7  41307  cdleme16aN  41317  cdleme11c  41319  cdleme11e  41321  cdleme11l  41327  cdleme11  41328  cdleme14  41331  cdleme15a  41332  cdleme16b  41337  cdleme16c  41338  cdleme16d  41339  cdleme16e  41340  cdleme16f  41341  cdleme18b  41350  cdleme19d  41364  cdleme20d  41370  cdleme20f  41372  cdleme20h  41374  cdleme20l1  41378  cdleme20l2  41379  cdleme20l  41380  cdleme21a  41383  cdleme21b  41384  cdleme21c  41385  cdleme21ct  41387  cdleme22f2  41405  cdleme22g  41406  cdlemefr32sn2aw  41462  cdleme43fsv1snlem  41478  cdleme32b  41500  cdleme35a  41506  cdleme35f  41512  cdleme36m  41519  cdleme37m  41520  cdleme42k  41542  cdleme43bN  41548  cdleme17d2  41553  cdlemeg46req  41587  cdlemeg46gfv  41588  cdlemeg46gfre  41590  cdleme50trn2a  41608  cdleme50trn2  41609  cdlemg8b  41686  cdlemg10a  41698  cdlemg12d  41704  cdlemg13a  41709  cdlemg15  41714  cdlemg16z  41717  cdlemg18b  41737  cdlemg18c  41738  cdlemg18  41740  cdlemg27b  41754  cdlemg33  41769  cdlemg42  41787  trljco  41798  cdlemj3  41881  tendoid0  41883  cdlemk3  41891  cdlemk22  41951  cdlemk36  41971  cdlemkfid3N  41983  cdlemk47  42007  cdlemk48  42008  cdlemk49  42009  cdlemk50  42010  cdlemk51  42011  cdlemk52  42012  cdlemk53a  42013  cdlemk53b  42014  cdlemk53  42015  cdlemk54  42016  cdlemk55  42019  cdlemk35u  42022  cdlemk39u1  42025  cdleml3N  42036  m1modnep2mod  48428  ssccatid  50180