Theorem syl132anc 1387

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 1382	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  18362  eengtrkg  29015  eengtrkge  29016  mgcmnt1  32966  mgcmnt2  32967  mgcmntco  32968  dfmgc2lem  32969  gsumtp  33043  linds2eq  33388  evl1deg1  33580  evl1deg3  33582  qqhval2lem  33943  qqhghm  33950  qqhrhm  33951  btwncomim  35994  btwnswapid  35998  btwnintr  36000  btwnexch3  36001  btwnxfr  36037  linecgrand  36063  btwnconn1lem13  36080  seglecgr12im  36091  segletr  36095  linethru  36134  lshpkrlem5  39095  omlmod1i2N  39241  omlspjN  39242  atcmp  39292  atexchcvrN  39422  atbtwn  39428  1cvratlt  39456  2atjlej  39461  hlatexch3N  39462  hlatexch4  39463  atcvrlln2  39501  atcvrlln  39502  llncmp  39504  llncvrlpln  39540  lplncmp  39544  lplnexllnN  39546  2llnjaN  39548  4atlem11  39591  lplncvrlvol  39598  lvolcmp  39599  dalem1  39641  dalem2  39643  dalem24  39679  dalem25  39680  dalem42  39696  lncvrat  39764  2llnma3r  39770  lhp2lt  39983  4atexlemswapqr  40045  4atexlemtlw  40049  4atexlemntlpq  40050  4atexlemc  40051  4atexlemnclw  40052  4atexlemcnd  40054  4atex2  40059  cdlemd1  40180  cdlemd7  40186  cdleme0e  40199  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme16aN  40241  cdleme11c  40243  cdleme11e  40245  cdleme11l  40251  cdleme11  40252  cdleme14  40255  cdleme15a  40256  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme18b  40274  cdleme19d  40288  cdleme20d  40294  cdleme20f  40296  cdleme20h  40298  cdleme20l1  40302  cdleme20l2  40303  cdleme20l  40304  cdleme21a  40307  cdleme21b  40308  cdleme21c  40309  cdleme21ct  40311  cdleme22f2  40329  cdleme22g  40330  cdlemefr32sn2aw  40386  cdleme43fsv1snlem  40402  cdleme32b  40424  cdleme35a  40430  cdleme35f  40436  cdleme36m  40443  cdleme37m  40444  cdleme42k  40466  cdleme43bN  40472  cdleme17d2  40477  cdlemeg46req  40511  cdlemeg46gfv  40512  cdlemeg46gfre  40514  cdleme50trn2a  40532  cdleme50trn2  40533  cdlemg8b  40610  cdlemg10a  40622  cdlemg12d  40628  cdlemg13a  40633  cdlemg15  40638  cdlemg16z  40641  cdlemg18b  40661  cdlemg18c  40662  cdlemg18  40664  cdlemg27b  40678  cdlemg33  40693  cdlemg42  40711  trljco  40722  cdlemj3  40805  tendoid0  40807  cdlemk3  40815  cdlemk22  40875  cdlemk36  40895  cdlemkfid3N  40907  cdlemk47  40931  cdlemk48  40932  cdlemk49  40933  cdlemk50  40934  cdlemk51  40935  cdlemk52  40936  cdlemk53a  40937  cdlemk53b  40938  cdlemk53  40939  cdlemk54  40940  cdlemk55  40943  cdlemk35u  40946  cdlemk39u1  40949  cdleml3N  40960  m1modnep2mod  47291