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

This theorem is referenced by:  drsdirfi  18263  eengtrkg  28512  eengtrkge  28513  mgcmnt1  32430  mgcmnt2  32431  mgcmntco  32432  dfmgc2lem  32433  linds2eq  32772  qqhval2lem  33260  qqhghm  33267  qqhrhm  33268  btwncomim  35290  btwnswapid  35294  btwnintr  35296  btwnexch3  35297  btwnxfr  35333  linecgrand  35359  btwnconn1lem13  35376  seglecgr12im  35387  segletr  35391  linethru  35430  lshpkrlem5  38288  omlmod1i2N  38434  omlspjN  38435  atcmp  38485  atexchcvrN  38615  atbtwn  38621  1cvratlt  38649  2atjlej  38654  hlatexch3N  38655  hlatexch4  38656  atcvrlln2  38694  atcvrlln  38695  llncmp  38697  llncvrlpln  38733  lplncmp  38737  lplnexllnN  38739  2llnjaN  38741  4atlem11  38784  lplncvrlvol  38791  lvolcmp  38792  dalem1  38834  dalem2  38836  dalem24  38872  dalem25  38873  dalem42  38889  lncvrat  38957  2llnma3r  38963  lhp2lt  39176  4atexlemswapqr  39238  4atexlemtlw  39242  4atexlemntlpq  39243  4atexlemc  39244  4atexlemnclw  39245  4atexlemcnd  39247  4atex2  39252  cdlemd1  39373  cdlemd7  39379  cdleme0e  39392  cdleme7c  39420  cdleme7d  39421  cdleme7e  39422  cdleme7ga  39423  cdleme7  39424  cdleme16aN  39434  cdleme11c  39436  cdleme11e  39438  cdleme11l  39444  cdleme11  39445  cdleme14  39448  cdleme15a  39449  cdleme16b  39454  cdleme16c  39455  cdleme16d  39456  cdleme16e  39457  cdleme16f  39458  cdleme18b  39467  cdleme19d  39481  cdleme20d  39487  cdleme20f  39489  cdleme20h  39491  cdleme20l1  39495  cdleme20l2  39496  cdleme20l  39497  cdleme21a  39500  cdleme21b  39501  cdleme21c  39502  cdleme21ct  39504  cdleme22f2  39522  cdleme22g  39523  cdlemefr32sn2aw  39579  cdleme43fsv1snlem  39595  cdleme32b  39617  cdleme35a  39623  cdleme35f  39629  cdleme36m  39636  cdleme37m  39637  cdleme42k  39659  cdleme43bN  39665  cdleme17d2  39670  cdlemeg46req  39704  cdlemeg46gfv  39705  cdlemeg46gfre  39707  cdleme50trn2a  39725  cdleme50trn2  39726  cdlemg8b  39803  cdlemg10a  39815  cdlemg12d  39821  cdlemg13a  39826  cdlemg15  39831  cdlemg16z  39834  cdlemg18b  39854  cdlemg18c  39855  cdlemg18  39857  cdlemg27b  39871  cdlemg33  39886  cdlemg42  39904  trljco  39915  cdlemj3  39998  tendoid0  40000  cdlemk3  40008  cdlemk22  40068  cdlemk36  40088  cdlemkfid3N  40100  cdlemk47  40124  cdlemk48  40125  cdlemk49  40126  cdlemk50  40127  cdlemk51  40128  cdlemk52  40129  cdlemk53a  40130  cdlemk53b  40131  cdlemk53  40132  cdlemk54  40133  cdlemk55  40136  cdlemk35u  40139  cdlemk39u1  40142  cdleml3N  40153