Theorem syl132anc 1388

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 1383	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  18375  eengtrkg  29019  eengtrkge  29020  mgcmnt1  32965  mgcmnt2  32966  mgcmntco  32967  dfmgc2lem  32968  gsumtp  33039  linds2eq  33374  evl1deg1  33566  evl1deg3  33568  qqhval2lem  33927  qqhghm  33934  qqhrhm  33935  btwncomim  35977  btwnswapid  35981  btwnintr  35983  btwnexch3  35984  btwnxfr  36020  linecgrand  36046  btwnconn1lem13  36063  seglecgr12im  36074  segletr  36078  linethru  36117  lshpkrlem5  39070  omlmod1i2N  39216  omlspjN  39217  atcmp  39267  atexchcvrN  39397  atbtwn  39403  1cvratlt  39431  2atjlej  39436  hlatexch3N  39437  hlatexch4  39438  atcvrlln2  39476  atcvrlln  39477  llncmp  39479  llncvrlpln  39515  lplncmp  39519  lplnexllnN  39521  2llnjaN  39523  4atlem11  39566  lplncvrlvol  39573  lvolcmp  39574  dalem1  39616  dalem2  39618  dalem24  39654  dalem25  39655  dalem42  39671  lncvrat  39739  2llnma3r  39745  lhp2lt  39958  4atexlemswapqr  40020  4atexlemtlw  40024  4atexlemntlpq  40025  4atexlemc  40026  4atexlemnclw  40027  4atexlemcnd  40029  4atex2  40034  cdlemd1  40155  cdlemd7  40161  cdleme0e  40174  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme16aN  40216  cdleme11c  40218  cdleme11e  40220  cdleme11l  40226  cdleme11  40227  cdleme14  40230  cdleme15a  40231  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme16f  40240  cdleme18b  40249  cdleme19d  40263  cdleme20d  40269  cdleme20f  40271  cdleme20h  40273  cdleme20l1  40277  cdleme20l2  40278  cdleme20l  40279  cdleme21a  40282  cdleme21b  40283  cdleme21c  40284  cdleme21ct  40286  cdleme22f2  40304  cdleme22g  40305  cdlemefr32sn2aw  40361  cdleme43fsv1snlem  40377  cdleme32b  40399  cdleme35a  40405  cdleme35f  40411  cdleme36m  40418  cdleme37m  40419  cdleme42k  40441  cdleme43bN  40447  cdleme17d2  40452  cdlemeg46req  40486  cdlemeg46gfv  40487  cdlemeg46gfre  40489  cdleme50trn2a  40507  cdleme50trn2  40508  cdlemg8b  40585  cdlemg10a  40597  cdlemg12d  40603  cdlemg13a  40608  cdlemg15  40613  cdlemg16z  40616  cdlemg18b  40636  cdlemg18c  40637  cdlemg18  40639  cdlemg27b  40653  cdlemg33  40668  cdlemg42  40686  trljco  40697  cdlemj3  40780  tendoid0  40782  cdlemk3  40790  cdlemk22  40850  cdlemk36  40870  cdlemkfid3N  40882  cdlemk47  40906  cdlemk48  40907  cdlemk49  40908  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  cdlemk53a  40912  cdlemk53b  40913  cdlemk53  40914  cdlemk54  40915  cdlemk55  40918  cdlemk35u  40921  cdlemk39u1  40924  cdleml3N  40935