Theorem syl132anc 1385

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 515	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl132anc.7	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl131anc 1380	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  drsdirfi  17540  eengtrkg  26780  eengtrkge  26781  mcgmnt1  30700  mcgmnt2  30701  mgcmntco  30702  dfmgc2lem  30703  linds2eq  30995  qqhval2lem  31332  qqhghm  31339  qqhrhm  31340  btwncomim  33587  btwnswapid  33591  btwnintr  33593  btwnexch3  33594  btwnxfr  33630  linecgrand  33656  btwnconn1lem13  33673  seglecgr12im  33684  segletr  33688  linethru  33727  lshpkrlem5  36410  omlmod1i2N  36556  omlspjN  36557  atcmp  36607  atexchcvrN  36736  atbtwn  36742  1cvratlt  36770  2atjlej  36775  hlatexch3N  36776  hlatexch4  36777  atcvrlln2  36815  atcvrlln  36816  llncmp  36818  llncvrlpln  36854  lplncmp  36858  lplnexllnN  36860  2llnjaN  36862  4atlem11  36905  lplncvrlvol  36912  lvolcmp  36913  dalem1  36955  dalem2  36957  dalem24  36993  dalem25  36994  dalem42  37010  lncvrat  37078  2llnma3r  37084  lhp2lt  37297  4atexlemswapqr  37359  4atexlemtlw  37363  4atexlemntlpq  37364  4atexlemc  37365  4atexlemnclw  37366  4atexlemcnd  37368  4atex2  37373  cdlemd1  37494  cdlemd7  37500  cdleme0e  37513  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme7  37545  cdleme16aN  37555  cdleme11c  37557  cdleme11e  37559  cdleme11l  37565  cdleme11  37566  cdleme14  37569  cdleme15a  37570  cdleme16b  37575  cdleme16c  37576  cdleme16d  37577  cdleme16e  37578  cdleme16f  37579  cdleme18b  37588  cdleme19d  37602  cdleme20d  37608  cdleme20f  37610  cdleme20h  37612  cdleme20l1  37616  cdleme20l2  37617  cdleme20l  37618  cdleme21a  37621  cdleme21b  37622  cdleme21c  37623  cdleme21ct  37625  cdleme22f2  37643  cdleme22g  37644  cdlemefr32sn2aw  37700  cdleme43fsv1snlem  37716  cdleme32b  37738  cdleme35a  37744  cdleme35f  37750  cdleme36m  37757  cdleme37m  37758  cdleme42k  37780  cdleme43bN  37786  cdleme17d2  37791  cdlemeg46req  37825  cdlemeg46gfv  37826  cdlemeg46gfre  37828  cdleme50trn2a  37846  cdleme50trn2  37847  cdlemg8b  37924  cdlemg10a  37936  cdlemg12d  37942  cdlemg13a  37947  cdlemg15  37952  cdlemg16z  37955  cdlemg18b  37975  cdlemg18c  37976  cdlemg18  37978  cdlemg27b  37992  cdlemg33  38007  cdlemg42  38025  trljco  38036  cdlemj3  38119  tendoid0  38121  cdlemk3  38129  cdlemk22  38189  cdlemk36  38209  cdlemkfid3N  38221  cdlemk47  38245  cdlemk48  38246  cdlemk49  38247  cdlemk50  38248  cdlemk51  38249  cdlemk52  38250  cdlemk53a  38251  cdlemk53b  38252  cdlemk53  38253  cdlemk54  38254  cdlemk55  38257  cdlemk35u  38260  cdlemk39u1  38263  cdleml3N  38274