Theorem syl132anc 1391

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 1386	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  drsdirfi  18271  eengtrkg  29055  eengtrkge  29056  mgcmnt1  33052  mgcmnt2  33053  mgcmntco  33054  dfmgc2lem  33055  gsumtp  33125  linds2eq  33441  evl1deg1  33636  evl1deg3  33638  qqhval2lem  34125  qqhghm  34132  qqhrhm  34133  btwncomim  36195  btwnswapid  36199  btwnintr  36201  btwnexch3  36202  btwnxfr  36238  linecgrand  36264  btwnconn1lem13  36281  seglecgr12im  36292  segletr  36296  linethru  36335  lshpkrlem5  39560  omlmod1i2N  39706  omlspjN  39707  atcmp  39757  atexchcvrN  39886  atbtwn  39892  1cvratlt  39920  2atjlej  39925  hlatexch3N  39926  hlatexch4  39927  atcvrlln2  39965  atcvrlln  39966  llncmp  39968  llncvrlpln  40004  lplncmp  40008  lplnexllnN  40010  2llnjaN  40012  4atlem11  40055  lplncvrlvol  40062  lvolcmp  40063  dalem1  40105  dalem2  40107  dalem24  40143  dalem25  40144  dalem42  40160  lncvrat  40228  2llnma3r  40234  lhp2lt  40447  4atexlemswapqr  40509  4atexlemtlw  40513  4atexlemntlpq  40514  4atexlemc  40515  4atexlemnclw  40516  4atexlemcnd  40518  4atex2  40523  cdlemd1  40644  cdlemd7  40650  cdleme0e  40663  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme16aN  40705  cdleme11c  40707  cdleme11e  40709  cdleme11l  40715  cdleme11  40716  cdleme14  40719  cdleme15a  40720  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme18b  40738  cdleme19d  40752  cdleme20d  40758  cdleme20f  40760  cdleme20h  40762  cdleme20l1  40766  cdleme20l2  40767  cdleme20l  40768  cdleme21a  40771  cdleme21b  40772  cdleme21c  40773  cdleme21ct  40775  cdleme22f2  40793  cdleme22g  40794  cdlemefr32sn2aw  40850  cdleme43fsv1snlem  40866  cdleme32b  40888  cdleme35a  40894  cdleme35f  40900  cdleme36m  40907  cdleme37m  40908  cdleme42k  40930  cdleme43bN  40936  cdleme17d2  40941  cdlemeg46req  40975  cdlemeg46gfv  40976  cdlemeg46gfre  40978  cdleme50trn2a  40996  cdleme50trn2  40997  cdlemg8b  41074  cdlemg10a  41086  cdlemg12d  41092  cdlemg13a  41097  cdlemg15  41102  cdlemg16z  41105  cdlemg18b  41125  cdlemg18c  41126  cdlemg18  41128  cdlemg27b  41142  cdlemg33  41157  cdlemg42  41175  trljco  41186  cdlemj3  41269  tendoid0  41271  cdlemk3  41279  cdlemk22  41339  cdlemk36  41359  cdlemkfid3N  41371  cdlemk47  41395  cdlemk48  41396  cdlemk49  41397  cdlemk50  41398  cdlemk51  41399  cdlemk52  41400  cdlemk53a  41401  cdlemk53b  41402  cdlemk53  41403  cdlemk54  41404  cdlemk55  41407  cdlemk35u  41410  cdlemk39u1  41413  cdleml3N  41424  m1modnep2mod  47806  ssccatid  49547