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  18266  eengtrkg  28913  eengtrkge  28914  mgcmnt1  32918  mgcmnt2  32919  mgcmntco  32920  dfmgc2lem  32921  gsumtp  32998  linds2eq  33352  evl1deg1  33545  evl1deg3  33547  qqhval2lem  33971  qqhghm  33978  qqhrhm  33979  btwncomim  36001  btwnswapid  36005  btwnintr  36007  btwnexch3  36008  btwnxfr  36044  linecgrand  36070  btwnconn1lem13  36087  seglecgr12im  36098  segletr  36102  linethru  36141  lshpkrlem5  39107  omlmod1i2N  39253  omlspjN  39254  atcmp  39304  atexchcvrN  39434  atbtwn  39440  1cvratlt  39468  2atjlej  39473  hlatexch3N  39474  hlatexch4  39475  atcvrlln2  39513  atcvrlln  39514  llncmp  39516  llncvrlpln  39552  lplncmp  39556  lplnexllnN  39558  2llnjaN  39560  4atlem11  39603  lplncvrlvol  39610  lvolcmp  39611  dalem1  39653  dalem2  39655  dalem24  39691  dalem25  39692  dalem42  39708  lncvrat  39776  2llnma3r  39782  lhp2lt  39995  4atexlemswapqr  40057  4atexlemtlw  40061  4atexlemntlpq  40062  4atexlemc  40063  4atexlemnclw  40064  4atexlemcnd  40066  4atex2  40071  cdlemd1  40192  cdlemd7  40198  cdleme0e  40211  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme16aN  40253  cdleme11c  40255  cdleme11e  40257  cdleme11l  40263  cdleme11  40264  cdleme14  40267  cdleme15a  40268  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme18b  40286  cdleme19d  40300  cdleme20d  40306  cdleme20f  40308  cdleme20h  40310  cdleme20l1  40314  cdleme20l2  40315  cdleme20l  40316  cdleme21a  40319  cdleme21b  40320  cdleme21c  40321  cdleme21ct  40323  cdleme22f2  40341  cdleme22g  40342  cdlemefr32sn2aw  40398  cdleme43fsv1snlem  40414  cdleme32b  40436  cdleme35a  40442  cdleme35f  40448  cdleme36m  40455  cdleme37m  40456  cdleme42k  40478  cdleme43bN  40484  cdleme17d2  40489  cdlemeg46req  40523  cdlemeg46gfv  40524  cdlemeg46gfre  40526  cdleme50trn2a  40544  cdleme50trn2  40545  cdlemg8b  40622  cdlemg10a  40634  cdlemg12d  40640  cdlemg13a  40645  cdlemg15  40650  cdlemg16z  40653  cdlemg18b  40673  cdlemg18c  40674  cdlemg18  40676  cdlemg27b  40690  cdlemg33  40705  cdlemg42  40723  trljco  40734  cdlemj3  40817  tendoid0  40819  cdlemk3  40827  cdlemk22  40887  cdlemk36  40907  cdlemkfid3N  40919  cdlemk47  40943  cdlemk48  40944  cdlemk49  40945  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  cdlemk53a  40949  cdlemk53b  40950  cdlemk53  40951  cdlemk54  40952  cdlemk55  40955  cdlemk35u  40958  cdlemk39u1  40961  cdleml3N  40972  m1modnep2mod  47353  ssccatid  49061