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  17614  eengtrkg  26879  eengtrkge  26880  mgcmnt1  30796  mgcmnt2  30797  mgcmntco  30798  dfmgc2lem  30799  linds2eq  31096  qqhval2lem  31450  qqhghm  31457  qqhrhm  31458  btwncomim  33864  btwnswapid  33868  btwnintr  33870  btwnexch3  33871  btwnxfr  33907  linecgrand  33933  btwnconn1lem13  33950  seglecgr12im  33961  segletr  33965  linethru  34004  lshpkrlem5  36690  omlmod1i2N  36836  omlspjN  36837  atcmp  36887  atexchcvrN  37016  atbtwn  37022  1cvratlt  37050  2atjlej  37055  hlatexch3N  37056  hlatexch4  37057  atcvrlln2  37095  atcvrlln  37096  llncmp  37098  llncvrlpln  37134  lplncmp  37138  lplnexllnN  37140  2llnjaN  37142  4atlem11  37185  lplncvrlvol  37192  lvolcmp  37193  dalem1  37235  dalem2  37237  dalem24  37273  dalem25  37274  dalem42  37290  lncvrat  37358  2llnma3r  37364  lhp2lt  37577  4atexlemswapqr  37639  4atexlemtlw  37643  4atexlemntlpq  37644  4atexlemc  37645  4atexlemnclw  37646  4atexlemcnd  37648  4atex2  37653  cdlemd1  37774  cdlemd7  37780  cdleme0e  37793  cdleme7c  37821  cdleme7d  37822  cdleme7e  37823  cdleme7ga  37824  cdleme7  37825  cdleme16aN  37835  cdleme11c  37837  cdleme11e  37839  cdleme11l  37845  cdleme11  37846  cdleme14  37849  cdleme15a  37850  cdleme16b  37855  cdleme16c  37856  cdleme16d  37857  cdleme16e  37858  cdleme16f  37859  cdleme18b  37868  cdleme19d  37882  cdleme20d  37888  cdleme20f  37890  cdleme20h  37892  cdleme20l1  37896  cdleme20l2  37897  cdleme20l  37898  cdleme21a  37901  cdleme21b  37902  cdleme21c  37903  cdleme21ct  37905  cdleme22f2  37923  cdleme22g  37924  cdlemefr32sn2aw  37980  cdleme43fsv1snlem  37996  cdleme32b  38018  cdleme35a  38024  cdleme35f  38030  cdleme36m  38037  cdleme37m  38038  cdleme42k  38060  cdleme43bN  38066  cdleme17d2  38071  cdlemeg46req  38105  cdlemeg46gfv  38106  cdlemeg46gfre  38108  cdleme50trn2a  38126  cdleme50trn2  38127  cdlemg8b  38204  cdlemg10a  38216  cdlemg12d  38222  cdlemg13a  38227  cdlemg15  38232  cdlemg16z  38235  cdlemg18b  38255  cdlemg18c  38256  cdlemg18  38258  cdlemg27b  38272  cdlemg33  38287  cdlemg42  38305  trljco  38316  cdlemj3  38399  tendoid0  38401  cdlemk3  38409  cdlemk22  38469  cdlemk36  38489  cdlemkfid3N  38501  cdlemk47  38525  cdlemk48  38526  cdlemk49  38527  cdlemk50  38528  cdlemk51  38529  cdlemk52  38530  cdlemk53a  38531  cdlemk53b  38532  cdlemk53  38533  cdlemk54  38534  cdlemk55  38537  cdlemk35u  38540  cdlemk39u1  38543  cdleml3N  38554