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  18273  eengtrkg  28920  eengtrkge  28921  mgcmnt1  32925  mgcmnt2  32926  mgcmntco  32927  dfmgc2lem  32928  gsumtp  33005  linds2eq  33359  evl1deg1  33552  evl1deg3  33554  qqhval2lem  33978  qqhghm  33985  qqhrhm  33986  btwncomim  36008  btwnswapid  36012  btwnintr  36014  btwnexch3  36015  btwnxfr  36051  linecgrand  36077  btwnconn1lem13  36094  seglecgr12im  36105  segletr  36109  linethru  36148  lshpkrlem5  39114  omlmod1i2N  39260  omlspjN  39261  atcmp  39311  atexchcvrN  39441  atbtwn  39447  1cvratlt  39475  2atjlej  39480  hlatexch3N  39481  hlatexch4  39482  atcvrlln2  39520  atcvrlln  39521  llncmp  39523  llncvrlpln  39559  lplncmp  39563  lplnexllnN  39565  2llnjaN  39567  4atlem11  39610  lplncvrlvol  39617  lvolcmp  39618  dalem1  39660  dalem2  39662  dalem24  39698  dalem25  39699  dalem42  39715  lncvrat  39783  2llnma3r  39789  lhp2lt  40002  4atexlemswapqr  40064  4atexlemtlw  40068  4atexlemntlpq  40069  4atexlemc  40070  4atexlemnclw  40071  4atexlemcnd  40073  4atex2  40078  cdlemd1  40199  cdlemd7  40205  cdleme0e  40218  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme16aN  40260  cdleme11c  40262  cdleme11e  40264  cdleme11l  40270  cdleme11  40271  cdleme14  40274  cdleme15a  40275  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme18b  40293  cdleme19d  40307  cdleme20d  40313  cdleme20f  40315  cdleme20h  40317  cdleme20l1  40321  cdleme20l2  40322  cdleme20l  40323  cdleme21a  40326  cdleme21b  40327  cdleme21c  40328  cdleme21ct  40330  cdleme22f2  40348  cdleme22g  40349  cdlemefr32sn2aw  40405  cdleme43fsv1snlem  40421  cdleme32b  40443  cdleme35a  40449  cdleme35f  40455  cdleme36m  40462  cdleme37m  40463  cdleme42k  40485  cdleme43bN  40491  cdleme17d2  40496  cdlemeg46req  40530  cdlemeg46gfv  40531  cdlemeg46gfre  40533  cdleme50trn2a  40551  cdleme50trn2  40552  cdlemg8b  40629  cdlemg10a  40641  cdlemg12d  40647  cdlemg13a  40652  cdlemg15  40657  cdlemg16z  40660  cdlemg18b  40680  cdlemg18c  40681  cdlemg18  40683  cdlemg27b  40697  cdlemg33  40712  cdlemg42  40730  trljco  40741  cdlemj3  40824  tendoid0  40826  cdlemk3  40834  cdlemk22  40894  cdlemk36  40914  cdlemkfid3N  40926  cdlemk47  40950  cdlemk48  40951  cdlemk49  40952  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  cdlemk53a  40956  cdlemk53b  40957  cdlemk53  40958  cdlemk54  40959  cdlemk55  40962  cdlemk35u  40965  cdlemk39u1  40968  cdleml3N  40979  m1modnep2mod  47357  ssccatid  49065