Theorem simpl33 1144

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

Assertion

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

Proof of Theorem simpl33

Step	Hyp	Ref	Expression
1		simp33 1099	. 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:  ax5seglem3a  25810  ax5seg  25818  elwwlks2ons3  26848  br8d  29422  br8  31646  nosupres  31853  cgrextend  32115  segconeq  32117  trisegint  32135  ifscgr  32151  cgrsub  32152  btwnxfr  32163  seglecgr12im  32217  segletr  32221  atbtwn  34732  4atlem10b  34891  4atlem11  34895  4atlem12  34898  2lplnj  34906  paddasslem4  35109  paddasslem7  35112  pmodlem1  35132  4atex2  35363  trlval3  35474  arglem1N  35477  cdleme0moN  35512  cdleme20  35612  cdleme21j  35624  cdleme28c  35660  cdleme38n  35752  cdlemg6c  35908  cdlemg6  35911  cdlemg7N  35914  cdlemg16  35945  cdlemg16ALTN  35946  cdlemg16zz  35948  cdlemg20  35973  cdlemg22  35975  cdlemg37  35977  cdlemg31d  35988  cdlemg29  35993  cdlemg33b  35995  cdlemg33  35999  cdlemg46  36023  cdlemk25-3  36192