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 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  18351  eengtrkg  29001  eengtrkge  29002  mgcmnt1  32982  mgcmnt2  32983  mgcmntco  32984  dfmgc2lem  32985  gsumtp  33061  linds2eq  33409  evl1deg1  33601  evl1deg3  33603  qqhval2lem  33982  qqhghm  33989  qqhrhm  33990  btwncomim  36014  btwnswapid  36018  btwnintr  36020  btwnexch3  36021  btwnxfr  36057  linecgrand  36083  btwnconn1lem13  36100  seglecgr12im  36111  segletr  36115  linethru  36154  lshpkrlem5  39115  omlmod1i2N  39261  omlspjN  39262  atcmp  39312  atexchcvrN  39442  atbtwn  39448  1cvratlt  39476  2atjlej  39481  hlatexch3N  39482  hlatexch4  39483  atcvrlln2  39521  atcvrlln  39522  llncmp  39524  llncvrlpln  39560  lplncmp  39564  lplnexllnN  39566  2llnjaN  39568  4atlem11  39611  lplncvrlvol  39618  lvolcmp  39619  dalem1  39661  dalem2  39663  dalem24  39699  dalem25  39700  dalem42  39716  lncvrat  39784  2llnma3r  39790  lhp2lt  40003  4atexlemswapqr  40065  4atexlemtlw  40069  4atexlemntlpq  40070  4atexlemc  40071  4atexlemnclw  40072  4atexlemcnd  40074  4atex2  40079  cdlemd1  40200  cdlemd7  40206  cdleme0e  40219  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme16aN  40261  cdleme11c  40263  cdleme11e  40265  cdleme11l  40271  cdleme11  40272  cdleme14  40275  cdleme15a  40276  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme18b  40294  cdleme19d  40308  cdleme20d  40314  cdleme20f  40316  cdleme20h  40318  cdleme20l1  40322  cdleme20l2  40323  cdleme20l  40324  cdleme21a  40327  cdleme21b  40328  cdleme21c  40329  cdleme21ct  40331  cdleme22f2  40349  cdleme22g  40350  cdlemefr32sn2aw  40406  cdleme43fsv1snlem  40422  cdleme32b  40444  cdleme35a  40450  cdleme35f  40456  cdleme36m  40463  cdleme37m  40464  cdleme42k  40486  cdleme43bN  40492  cdleme17d2  40497  cdlemeg46req  40531  cdlemeg46gfv  40532  cdlemeg46gfre  40534  cdleme50trn2a  40552  cdleme50trn2  40553  cdlemg8b  40630  cdlemg10a  40642  cdlemg12d  40648  cdlemg13a  40653  cdlemg15  40658  cdlemg16z  40661  cdlemg18b  40681  cdlemg18c  40682  cdlemg18  40684  cdlemg27b  40698  cdlemg33  40713  cdlemg42  40731  trljco  40742  cdlemj3  40825  tendoid0  40827  cdlemk3  40835  cdlemk22  40895  cdlemk36  40915  cdlemkfid3N  40927  cdlemk47  40951  cdlemk48  40952  cdlemk49  40953  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  cdlemk53a  40957  cdlemk53b  40958  cdlemk53  40959  cdlemk54  40960  cdlemk55  40963  cdlemk35u  40966  cdlemk39u1  40969  cdleml3N  40980  m1modnep2mod  47354