Theorem simpl33 1257

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

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

Proof of Theorem simpl33

Step	Hyp	Ref	Expression
1		simpl3 1194	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl3 1188	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  nosupres  27210  noinfres  27225  ax5seglem3a  28219  ax5seg  28227  numclwwlk1lem2foa  29638  br8d  31870  br8  34757  cgrextend  35011  segconeq  35013  trisegint  35031  ifscgr  35047  cgrsub  35048  btwnxfr  35059  seglecgr12im  35113  segletr  35117  atbtwn  38365  4atlem10b  38524  4atlem11  38528  4atlem12  38531  2lplnj  38539  paddasslem4  38742  paddasslem7  38745  pmodlem1  38765  4atex2  38996  trlval3  39106  arglem1N  39109  cdleme0moN  39144  cdleme20  39243  cdleme21j  39255  cdleme28c  39291  cdleme38n  39383  cdlemg6c  39539  cdlemg6  39542  cdlemg7N  39545  cdlemg16  39576  cdlemg16ALTN  39577  cdlemg16zz  39579  cdlemg20  39604  cdlemg22  39606  cdlemg37  39608  cdlemg31d  39619  cdlemg29  39624  cdlemg33b  39626  cdlemg33  39630  cdlemg46  39654  cdlemk25-3  39823