Theorem syl132anc 1390

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

This theorem is referenced by:  drsdirfi  18315  eengtrkg  28911  eengtrkge  28912  mgcmnt1  32918  mgcmnt2  32919  mgcmntco  32920  dfmgc2lem  32921  gsumtp  32998  linds2eq  33342  evl1deg1  33535  evl1deg3  33537  qqhval2lem  33958  qqhghm  33965  qqhrhm  33966  btwncomim  35977  btwnswapid  35981  btwnintr  35983  btwnexch3  35984  btwnxfr  36020  linecgrand  36046  btwnconn1lem13  36063  seglecgr12im  36074  segletr  36078  linethru  36117  lshpkrlem5  39078  omlmod1i2N  39224  omlspjN  39225  atcmp  39275  atexchcvrN  39405  atbtwn  39411  1cvratlt  39439  2atjlej  39444  hlatexch3N  39445  hlatexch4  39446  atcvrlln2  39484  atcvrlln  39485  llncmp  39487  llncvrlpln  39523  lplncmp  39527  lplnexllnN  39529  2llnjaN  39531  4atlem11  39574  lplncvrlvol  39581  lvolcmp  39582  dalem1  39624  dalem2  39626  dalem24  39662  dalem25  39663  dalem42  39679  lncvrat  39747  2llnma3r  39753  lhp2lt  39966  4atexlemswapqr  40028  4atexlemtlw  40032  4atexlemntlpq  40033  4atexlemc  40034  4atexlemnclw  40035  4atexlemcnd  40037  4atex2  40042  cdlemd1  40163  cdlemd7  40169  cdleme0e  40182  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme16aN  40224  cdleme11c  40226  cdleme11e  40228  cdleme11l  40234  cdleme11  40235  cdleme14  40238  cdleme15a  40239  cdleme16b  40244  cdleme16c  40245  cdleme16d  40246  cdleme16e  40247  cdleme16f  40248  cdleme18b  40257  cdleme19d  40271  cdleme20d  40277  cdleme20f  40279  cdleme20h  40281  cdleme20l1  40285  cdleme20l2  40286  cdleme20l  40287  cdleme21a  40290  cdleme21b  40291  cdleme21c  40292  cdleme21ct  40294  cdleme22f2  40312  cdleme22g  40313  cdlemefr32sn2aw  40369  cdleme43fsv1snlem  40385  cdleme32b  40407  cdleme35a  40413  cdleme35f  40419  cdleme36m  40426  cdleme37m  40427  cdleme42k  40449  cdleme43bN  40455  cdleme17d2  40460  cdlemeg46req  40494  cdlemeg46gfv  40495  cdlemeg46gfre  40497  cdleme50trn2a  40515  cdleme50trn2  40516  cdlemg8b  40593  cdlemg10a  40605  cdlemg12d  40611  cdlemg13a  40616  cdlemg15  40621  cdlemg16z  40624  cdlemg18b  40644  cdlemg18c  40645  cdlemg18  40647  cdlemg27b  40661  cdlemg33  40676  cdlemg42  40694  trljco  40705  cdlemj3  40788  tendoid0  40790  cdlemk3  40798  cdlemk22  40858  cdlemk36  40878  cdlemkfid3N  40890  cdlemk47  40914  cdlemk48  40915  cdlemk49  40916  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  cdlemk53a  40920  cdlemk53b  40921  cdlemk53  40922  cdlemk54  40923  cdlemk55  40926  cdlemk35u  40929  cdlemk39u1  40932  cdleml3N  40943  m1modnep2mod  47329  ssccatid  48987