Theorem syl132anc 1389

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  drsdirfi  18258  eengtrkg  28244  eengtrkge  28245  mgcmnt1  32162  mgcmnt2  32163  mgcmntco  32164  dfmgc2lem  32165  linds2eq  32497  qqhval2lem  32961  qqhghm  32968  qqhrhm  32969  btwncomim  34985  btwnswapid  34989  btwnintr  34991  btwnexch3  34992  btwnxfr  35028  linecgrand  35054  btwnconn1lem13  35071  seglecgr12im  35082  segletr  35086  linethru  35125  lshpkrlem5  37984  omlmod1i2N  38130  omlspjN  38131  atcmp  38181  atexchcvrN  38311  atbtwn  38317  1cvratlt  38345  2atjlej  38350  hlatexch3N  38351  hlatexch4  38352  atcvrlln2  38390  atcvrlln  38391  llncmp  38393  llncvrlpln  38429  lplncmp  38433  lplnexllnN  38435  2llnjaN  38437  4atlem11  38480  lplncvrlvol  38487  lvolcmp  38488  dalem1  38530  dalem2  38532  dalem24  38568  dalem25  38569  dalem42  38585  lncvrat  38653  2llnma3r  38659  lhp2lt  38872  4atexlemswapqr  38934  4atexlemtlw  38938  4atexlemntlpq  38939  4atexlemc  38940  4atexlemnclw  38941  4atexlemcnd  38943  4atex2  38948  cdlemd1  39069  cdlemd7  39075  cdleme0e  39088  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme7  39120  cdleme16aN  39130  cdleme11c  39132  cdleme11e  39134  cdleme11l  39140  cdleme11  39141  cdleme14  39144  cdleme15a  39145  cdleme16b  39150  cdleme16c  39151  cdleme16d  39152  cdleme16e  39153  cdleme16f  39154  cdleme18b  39163  cdleme19d  39177  cdleme20d  39183  cdleme20f  39185  cdleme20h  39187  cdleme20l1  39191  cdleme20l2  39192  cdleme20l  39193  cdleme21a  39196  cdleme21b  39197  cdleme21c  39198  cdleme21ct  39200  cdleme22f2  39218  cdleme22g  39219  cdlemefr32sn2aw  39275  cdleme43fsv1snlem  39291  cdleme32b  39313  cdleme35a  39319  cdleme35f  39325  cdleme36m  39332  cdleme37m  39333  cdleme42k  39355  cdleme43bN  39361  cdleme17d2  39366  cdlemeg46req  39400  cdlemeg46gfv  39401  cdlemeg46gfre  39403  cdleme50trn2a  39421  cdleme50trn2  39422  cdlemg8b  39499  cdlemg10a  39511  cdlemg12d  39517  cdlemg13a  39522  cdlemg15  39527  cdlemg16z  39530  cdlemg18b  39550  cdlemg18c  39551  cdlemg18  39553  cdlemg27b  39567  cdlemg33  39582  cdlemg42  39600  trljco  39611  cdlemj3  39694  tendoid0  39696  cdlemk3  39704  cdlemk22  39764  cdlemk36  39784  cdlemkfid3N  39796  cdlemk47  39820  cdlemk48  39821  cdlemk49  39822  cdlemk50  39823  cdlemk51  39824  cdlemk52  39825  cdlemk53a  39826  cdlemk53b  39827  cdlemk53  39828  cdlemk54  39829  cdlemk55  39832  cdlemk35u  39835  cdlemk39u1  39838  cdleml3N  39849