Theorem simpl32 1143

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl32	⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl32

Step	Hyp	Ref	Expression
1		simp32 1098	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓)
2	1	adantr 481	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  initoeu2lem2  16665  mulmarep1gsum2  20380  tsmsxp  21958  ax5seg  25818  elwwlks2ons3  26848  br8d  29422  br8  31646  cgrextend  32115  segconeq  32117  trisegint  32135  ifscgr  32151  cgrsub  32152  btwnxfr  32163  seglecgr12im  32217  segletr  32221  exatleN  34690  atbtwn  34732  3dim1  34753  3dim2  34754  2llnjaN  34852  4atlem10b  34891  4atlem11  34895  4atlem12  34898  2lplnj  34906  cdlemb  35080  paddasslem4  35109  pmodlem1  35132  4atex2  35363  trlval3  35474  arglem1N  35477  cdleme0moN  35512  cdleme17b  35574  cdleme20  35612  cdleme21j  35624  cdleme28c  35660  cdleme35h2  35745  cdleme38n  35752  cdlemg6c  35908  cdlemg6  35911  cdlemg7N  35914  cdlemg11a  35925  cdlemg12e  35935  cdlemg16  35945  cdlemg16ALTN  35946  cdlemg16zz  35948  cdlemg20  35973  cdlemg22  35975  cdlemg37  35977  cdlemg31d  35988  cdlemg29  35993  cdlemg33b  35995  cdlemg33  35999  cdlemg39  36004  cdlemg42  36017  cdlemk25-3  36192