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  18228  eengtrkg  29059  eengtrkge  29060  mgcmnt1  33074  mgcmnt2  33075  mgcmntco  33076  dfmgc2lem  33077  gsumtp  33147  linds2eq  33462  evl1deg1  33657  evl1deg3  33659  qqhval2lem  34138  qqhghm  34145  qqhrhm  34146  btwncomim  36207  btwnswapid  36211  btwnintr  36213  btwnexch3  36214  btwnxfr  36250  linecgrand  36276  btwnconn1lem13  36293  seglecgr12im  36304  segletr  36308  linethru  36347  lshpkrlem5  39370  omlmod1i2N  39516  omlspjN  39517  atcmp  39567  atexchcvrN  39696  atbtwn  39702  1cvratlt  39730  2atjlej  39735  hlatexch3N  39736  hlatexch4  39737  atcvrlln2  39775  atcvrlln  39776  llncmp  39778  llncvrlpln  39814  lplncmp  39818  lplnexllnN  39820  2llnjaN  39822  4atlem11  39865  lplncvrlvol  39872  lvolcmp  39873  dalem1  39915  dalem2  39917  dalem24  39953  dalem25  39954  dalem42  39970  lncvrat  40038  2llnma3r  40044  lhp2lt  40257  4atexlemswapqr  40319  4atexlemtlw  40323  4atexlemntlpq  40324  4atexlemc  40325  4atexlemnclw  40326  4atexlemcnd  40328  4atex2  40333  cdlemd1  40454  cdlemd7  40460  cdleme0e  40473  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme16aN  40515  cdleme11c  40517  cdleme11e  40519  cdleme11l  40525  cdleme11  40526  cdleme14  40529  cdleme15a  40530  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme16e  40538  cdleme16f  40539  cdleme18b  40548  cdleme19d  40562  cdleme20d  40568  cdleme20f  40570  cdleme20h  40572  cdleme20l1  40576  cdleme20l2  40577  cdleme20l  40578  cdleme21a  40581  cdleme21b  40582  cdleme21c  40583  cdleme21ct  40585  cdleme22f2  40603  cdleme22g  40604  cdlemefr32sn2aw  40660  cdleme43fsv1snlem  40676  cdleme32b  40698  cdleme35a  40704  cdleme35f  40710  cdleme36m  40717  cdleme37m  40718  cdleme42k  40740  cdleme43bN  40746  cdleme17d2  40751  cdlemeg46req  40785  cdlemeg46gfv  40786  cdlemeg46gfre  40788  cdleme50trn2a  40806  cdleme50trn2  40807  cdlemg8b  40884  cdlemg10a  40896  cdlemg12d  40902  cdlemg13a  40907  cdlemg15  40912  cdlemg16z  40915  cdlemg18b  40935  cdlemg18c  40936  cdlemg18  40938  cdlemg27b  40952  cdlemg33  40967  cdlemg42  40985  trljco  40996  cdlemj3  41079  tendoid0  41081  cdlemk3  41089  cdlemk22  41149  cdlemk36  41169  cdlemkfid3N  41181  cdlemk47  41205  cdlemk48  41206  cdlemk49  41207  cdlemk50  41208  cdlemk51  41209  cdlemk52  41210  cdlemk53a  41211  cdlemk53b  41212  cdlemk53  41213  cdlemk54  41214  cdlemk55  41217  cdlemk35u  41220  cdlemk39u1  41223  cdleml3N  41234  m1modnep2mod  47594  ssccatid  49313