Theorem syl113anc 1381

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl113anc.6	⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl113anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl113anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	3, 4, 5	3jca 1127	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂))
7		syl113anc.6	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 6, 7	syl3anc 1370	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl123anc  1386  syl213anc  1388  pythagtriplem18  16542  initoeu2  17740  psgnunilem1  19110  mulmarep1gsum1  21731  mulmarep1gsum2  21732  smadiadetlem4  21827  cramerimplem2  21842  cramerlem2  21846  cramer  21849  cnhaus  22514  dishaus  22542  ordthauslem  22543  pthaus  22798  txhaus  22807  xkohaus  22813  regr1lem  22899  methaus  23685  metnrmlem3  24033  iscgrad  27181  f1otrge  27242  axpaschlem  27317  wwlksnwwlksnon  28289  n4cyclfrgr  28664  br8d  30959  lt2addrd  31083  xlt2addrd  31090  br8  33732  br4  33734  nosupres  33919  nosupbnd1lem1  33920  nosupbnd2  33928  noinfres  33934  noinfbnd1lem1  33935  btwnxfr  34367  lineext  34387  brsegle  34419  brsegle2  34420  lfl0  37086  lfladd  37087  lflsub  37088  lflmul  37089  lflnegcl  37096  lflvscl  37098  lkrlss  37116  3dimlem3  37482  3dimlem4  37485  3dim3  37490  2llnm3N  37590  2lplnja  37640  4atex  38097  4atex3  38102  trlval4  38209  cdleme7c  38266  cdleme7d  38267  cdleme7ga  38269  cdleme21h  38355  cdleme21i  38356  cdleme21j  38357  cdleme21  38358  cdleme32d  38465  cdleme32f  38467  cdleme35h2  38478  cdleme38m  38484  cdleme40m  38488  cdlemg8  38652  cdlemg11a  38658  cdlemg10a  38661  cdlemg12b  38665  cdlemg12d  38667  cdlemg12f  38669  cdlemg12g  38670  cdlemg15a  38676  cdlemg16  38678  cdlemg16z  38680  cdlemg18a  38699  cdlemg24  38709  cdlemg29  38726  cdlemg33b  38728  cdlemg38  38736  cdlemg39  38737  cdlemg40  38738  cdlemg44b  38753  cdlemj2  38843  cdlemk7  38869  cdlemk12  38871  cdlemk12u  38893  cdlemk32  38918  cdlemk25-3  38925  cdlemk34  38931  cdlemkid3N  38954  cdlemkid4  38955  cdlemk11t  38967  cdlemk53  38978  cdlemk55b  38981  cdleml3N  38999  hdmapln1  39927  sepfsepc  46232