Theorem syl132anc 1413

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  drsdirfi  18360  eengtrkg  29302  eengtrkge  29303  mgcmnt1  33278  mgcmnt2  33279  mgcmntco  33280  dfmgc2lem  33281  gsumtp  33350  linds2eq  33660  evl1deg1  33832  evl1deg3  33834  qqhval2lem  34337  qqhghm  34344  qqhrhm  34345  btwncomim  36459  btwnswapid  36463  btwnintr  36465  btwnexch3  36466  btwnxfr  36502  linecgrand  36528  btwnconn1lem13  36545  seglecgr12im  36556  segletr  36560  linethru  36599  lshpkrlem5  39834  omlmod1i2N  39980  omlspjN  39981  atcmp  40031  atexchcvrN  40160  atbtwn  40166  1cvratlt  40194  2atjlej  40199  hlatexch3N  40200  hlatexch4  40201  atcvrlln2  40239  atcvrlln  40240  llncmp  40242  llncvrlpln  40278  lplncmp  40282  lplnexllnN  40284  2llnjaN  40286  4atlem11  40329  lplncvrlvol  40336  lvolcmp  40337  dalem1  40379  dalem2  40381  dalem24  40417  dalem25  40418  dalem42  40434  lncvrat  40502  2llnma3r  40508  lhp2lt  40721  4atexlemswapqr  40783  4atexlemtlw  40787  4atexlemntlpq  40788  4atexlemc  40789  4atexlemnclw  40790  4atexlemcnd  40792  4atex2  40797  cdlemd1  40918  cdlemd7  40924  cdleme0e  40937  cdleme7c  40965  cdleme7d  40966  cdleme7e  40967  cdleme7ga  40968  cdleme7  40969  cdleme16aN  40979  cdleme11c  40981  cdleme11e  40983  cdleme11l  40989  cdleme11  40990  cdleme14  40993  cdleme15a  40994  cdleme16b  40999  cdleme16c  41000  cdleme16d  41001  cdleme16e  41002  cdleme16f  41003  cdleme18b  41012  cdleme19d  41026  cdleme20d  41032  cdleme20f  41034  cdleme20h  41036  cdleme20l1  41040  cdleme20l2  41041  cdleme20l  41042  cdleme21a  41045  cdleme21b  41046  cdleme21c  41047  cdleme21ct  41049  cdleme22f2  41067  cdleme22g  41068  cdlemefr32sn2aw  41124  cdleme43fsv1snlem  41140  cdleme32b  41162  cdleme35a  41168  cdleme35f  41174  cdleme36m  41181  cdleme37m  41182  cdleme42k  41204  cdleme43bN  41210  cdleme17d2  41215  cdlemeg46req  41249  cdlemeg46gfv  41250  cdlemeg46gfre  41252  cdleme50trn2a  41270  cdleme50trn2  41271  cdlemg8b  41348  cdlemg10a  41360  cdlemg12d  41366  cdlemg13a  41371  cdlemg15  41376  cdlemg16z  41379  cdlemg18b  41399  cdlemg18c  41400  cdlemg18  41402  cdlemg27b  41416  cdlemg33  41431  cdlemg42  41449  trljco  41460  cdlemj3  41543  tendoid0  41545  cdlemk3  41553  cdlemk22  41613  cdlemk36  41633  cdlemkfid3N  41645  cdlemk47  41669  cdlemk48  41670  cdlemk49  41671  cdlemk50  41672  cdlemk51  41673  cdlemk52  41674  cdlemk53a  41675  cdlemk53b  41676  cdlemk53  41677  cdlemk54  41678  cdlemk55  41681  cdlemk35u  41684  cdlemk39u1  41687  cdleml3N  41698  m1modnep2mod  48040  ssccatid  49795