Theorem syl132anc 1386

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  drsdirfi  18262  eengtrkg  28511  eengtrkge  28512  mgcmnt1  32429  mgcmnt2  32430  mgcmntco  32431  dfmgc2lem  32432  linds2eq  32771  qqhval2lem  33259  qqhghm  33266  qqhrhm  33267  btwncomim  35289  btwnswapid  35293  btwnintr  35295  btwnexch3  35296  btwnxfr  35332  linecgrand  35358  btwnconn1lem13  35375  seglecgr12im  35386  segletr  35390  linethru  35429  lshpkrlem5  38287  omlmod1i2N  38433  omlspjN  38434  atcmp  38484  atexchcvrN  38614  atbtwn  38620  1cvratlt  38648  2atjlej  38653  hlatexch3N  38654  hlatexch4  38655  atcvrlln2  38693  atcvrlln  38694  llncmp  38696  llncvrlpln  38732  lplncmp  38736  lplnexllnN  38738  2llnjaN  38740  4atlem11  38783  lplncvrlvol  38790  lvolcmp  38791  dalem1  38833  dalem2  38835  dalem24  38871  dalem25  38872  dalem42  38888  lncvrat  38956  2llnma3r  38962  lhp2lt  39175  4atexlemswapqr  39237  4atexlemtlw  39241  4atexlemntlpq  39242  4atexlemc  39243  4atexlemnclw  39244  4atexlemcnd  39246  4atex2  39251  cdlemd1  39372  cdlemd7  39378  cdleme0e  39391  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme7ga  39422  cdleme7  39423  cdleme16aN  39433  cdleme11c  39435  cdleme11e  39437  cdleme11l  39443  cdleme11  39444  cdleme14  39447  cdleme15a  39448  cdleme16b  39453  cdleme16c  39454  cdleme16d  39455  cdleme16e  39456  cdleme16f  39457  cdleme18b  39466  cdleme19d  39480  cdleme20d  39486  cdleme20f  39488  cdleme20h  39490  cdleme20l1  39494  cdleme20l2  39495  cdleme20l  39496  cdleme21a  39499  cdleme21b  39500  cdleme21c  39501  cdleme21ct  39503  cdleme22f2  39521  cdleme22g  39522  cdlemefr32sn2aw  39578  cdleme43fsv1snlem  39594  cdleme32b  39616  cdleme35a  39622  cdleme35f  39628  cdleme36m  39635  cdleme37m  39636  cdleme42k  39658  cdleme43bN  39664  cdleme17d2  39669  cdlemeg46req  39703  cdlemeg46gfv  39704  cdlemeg46gfre  39706  cdleme50trn2a  39724  cdleme50trn2  39725  cdlemg8b  39802  cdlemg10a  39814  cdlemg12d  39820  cdlemg13a  39825  cdlemg15  39830  cdlemg16z  39833  cdlemg18b  39853  cdlemg18c  39854  cdlemg18  39856  cdlemg27b  39870  cdlemg33  39885  cdlemg42  39903  trljco  39914  cdlemj3  39997  tendoid0  39999  cdlemk3  40007  cdlemk22  40067  cdlemk36  40087  cdlemkfid3N  40099  cdlemk47  40123  cdlemk48  40124  cdlemk49  40125  cdlemk50  40126  cdlemk51  40127  cdlemk52  40128  cdlemk53a  40129  cdlemk53b  40130  cdlemk53  40131  cdlemk54  40132  cdlemk55  40135  cdlemk35u  40138  cdlemk39u1  40141  cdleml3N  40152