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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 206  df-an 396  df-3an 1086

This theorem is referenced by:  drsdirfi  18259  eengtrkg  28679  eengtrkge  28680  mgcmnt1  32595  mgcmnt2  32596  mgcmntco  32597  dfmgc2lem  32598  linds2eq  32932  qqhval2lem  33416  qqhghm  33423  qqhrhm  33424  btwncomim  35446  btwnswapid  35450  btwnintr  35452  btwnexch3  35453  btwnxfr  35489  linecgrand  35515  btwnconn1lem13  35532  seglecgr12im  35543  segletr  35547  linethru  35586  lshpkrlem5  38440  omlmod1i2N  38586  omlspjN  38587  atcmp  38637  atexchcvrN  38767  atbtwn  38773  1cvratlt  38801  2atjlej  38806  hlatexch3N  38807  hlatexch4  38808  atcvrlln2  38846  atcvrlln  38847  llncmp  38849  llncvrlpln  38885  lplncmp  38889  lplnexllnN  38891  2llnjaN  38893  4atlem11  38936  lplncvrlvol  38943  lvolcmp  38944  dalem1  38986  dalem2  38988  dalem24  39024  dalem25  39025  dalem42  39041  lncvrat  39109  2llnma3r  39115  lhp2lt  39328  4atexlemswapqr  39390  4atexlemtlw  39394  4atexlemntlpq  39395  4atexlemc  39396  4atexlemnclw  39397  4atexlemcnd  39399  4atex2  39404  cdlemd1  39525  cdlemd7  39531  cdleme0e  39544  cdleme7c  39572  cdleme7d  39573  cdleme7e  39574  cdleme7ga  39575  cdleme7  39576  cdleme16aN  39586  cdleme11c  39588  cdleme11e  39590  cdleme11l  39596  cdleme11  39597  cdleme14  39600  cdleme15a  39601  cdleme16b  39606  cdleme16c  39607  cdleme16d  39608  cdleme16e  39609  cdleme16f  39610  cdleme18b  39619  cdleme19d  39633  cdleme20d  39639  cdleme20f  39641  cdleme20h  39643  cdleme20l1  39647  cdleme20l2  39648  cdleme20l  39649  cdleme21a  39652  cdleme21b  39653  cdleme21c  39654  cdleme21ct  39656  cdleme22f2  39674  cdleme22g  39675  cdlemefr32sn2aw  39731  cdleme43fsv1snlem  39747  cdleme32b  39769  cdleme35a  39775  cdleme35f  39781  cdleme36m  39788  cdleme37m  39789  cdleme42k  39811  cdleme43bN  39817  cdleme17d2  39822  cdlemeg46req  39856  cdlemeg46gfv  39857  cdlemeg46gfre  39859  cdleme50trn2a  39877  cdleme50trn2  39878  cdlemg8b  39955  cdlemg10a  39967  cdlemg12d  39973  cdlemg13a  39978  cdlemg15  39983  cdlemg16z  39986  cdlemg18b  40006  cdlemg18c  40007  cdlemg18  40009  cdlemg27b  40023  cdlemg33  40038  cdlemg42  40056  trljco  40067  cdlemj3  40150  tendoid0  40152  cdlemk3  40160  cdlemk22  40220  cdlemk36  40240  cdlemkfid3N  40252  cdlemk47  40276  cdlemk48  40277  cdlemk49  40278  cdlemk50  40279  cdlemk51  40280  cdlemk52  40281  cdlemk53a  40282  cdlemk53b  40283  cdlemk53  40284  cdlemk54  40285  cdlemk55  40288  cdlemk35u  40291  cdlemk39u1  40294  cdleml3N  40305