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  18228  eengtrkg  29059  eengtrkge  29060  mgcmnt1  33074  mgcmnt2  33075  mgcmntco  33076  dfmgc2lem  33077  gsumtp  33147  linds2eq  33462  evl1deg1  33657  evl1deg3  33659  qqhval2lem  34138  qqhghm  34145  qqhrhm  34146  btwncomim  36207  btwnswapid  36211  btwnintr  36213  btwnexch3  36214  btwnxfr  36250  linecgrand  36276  btwnconn1lem13  36293  seglecgr12im  36304  segletr  36308  linethru  36347  lshpkrlem5  39374  omlmod1i2N  39520  omlspjN  39521  atcmp  39571  atexchcvrN  39700  atbtwn  39706  1cvratlt  39734  2atjlej  39739  hlatexch3N  39740  hlatexch4  39741  atcvrlln2  39779  atcvrlln  39780  llncmp  39782  llncvrlpln  39818  lplncmp  39822  lplnexllnN  39824  2llnjaN  39826  4atlem11  39869  lplncvrlvol  39876  lvolcmp  39877  dalem1  39919  dalem2  39921  dalem24  39957  dalem25  39958  dalem42  39974  lncvrat  40042  2llnma3r  40048  lhp2lt  40261  4atexlemswapqr  40323  4atexlemtlw  40327  4atexlemntlpq  40328  4atexlemc  40329  4atexlemnclw  40330  4atexlemcnd  40332  4atex2  40337  cdlemd1  40458  cdlemd7  40464  cdleme0e  40477  cdleme7c  40505  cdleme7d  40506  cdleme7e  40507  cdleme7ga  40508  cdleme7  40509  cdleme16aN  40519  cdleme11c  40521  cdleme11e  40523  cdleme11l  40529  cdleme11  40530  cdleme14  40533  cdleme15a  40534  cdleme16b  40539  cdleme16c  40540  cdleme16d  40541  cdleme16e  40542  cdleme16f  40543  cdleme18b  40552  cdleme19d  40566  cdleme20d  40572  cdleme20f  40574  cdleme20h  40576  cdleme20l1  40580  cdleme20l2  40581  cdleme20l  40582  cdleme21a  40585  cdleme21b  40586  cdleme21c  40587  cdleme21ct  40589  cdleme22f2  40607  cdleme22g  40608  cdlemefr32sn2aw  40664  cdleme43fsv1snlem  40680  cdleme32b  40702  cdleme35a  40708  cdleme35f  40714  cdleme36m  40721  cdleme37m  40722  cdleme42k  40744  cdleme43bN  40750  cdleme17d2  40755  cdlemeg46req  40789  cdlemeg46gfv  40790  cdlemeg46gfre  40792  cdleme50trn2a  40810  cdleme50trn2  40811  cdlemg8b  40888  cdlemg10a  40900  cdlemg12d  40906  cdlemg13a  40911  cdlemg15  40916  cdlemg16z  40919  cdlemg18b  40939  cdlemg18c  40940  cdlemg18  40942  cdlemg27b  40956  cdlemg33  40971  cdlemg42  40989  trljco  41000  cdlemj3  41083  tendoid0  41085  cdlemk3  41093  cdlemk22  41153  cdlemk36  41173  cdlemkfid3N  41185  cdlemk47  41209  cdlemk48  41210  cdlemk49  41211  cdlemk50  41212  cdlemk51  41213  cdlemk52  41214  cdlemk53a  41215  cdlemk53b  41216  cdlemk53  41217  cdlemk54  41218  cdlemk55  41221  cdlemk35u  41224  cdlemk39u1  41227  cdleml3N  41238  m1modnep2mod  47598  ssccatid  49317