Theorem simpl33 1255

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 1192	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl3 1186	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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:  ax5seglem3a  27298  ax5seg  27306  numclwwlk1lem2foa  28718  br8d  30950  br8  33723  nosupres  33910  noinfres  33925  cgrextend  34310  segconeq  34312  trisegint  34330  ifscgr  34346  cgrsub  34347  btwnxfr  34358  seglecgr12im  34412  segletr  34416  atbtwn  37460  4atlem10b  37619  4atlem11  37623  4atlem12  37626  2lplnj  37634  paddasslem4  37837  paddasslem7  37840  pmodlem1  37860  4atex2  38091  trlval3  38201  arglem1N  38204  cdleme0moN  38239  cdleme20  38338  cdleme21j  38350  cdleme28c  38386  cdleme38n  38478  cdlemg6c  38634  cdlemg6  38637  cdlemg7N  38640  cdlemg16  38671  cdlemg16ALTN  38672  cdlemg16zz  38674  cdlemg20  38699  cdlemg22  38701  cdlemg37  38703  cdlemg31d  38714  cdlemg29  38719  cdlemg33b  38721  cdlemg33  38725  cdlemg46  38749  cdlemk25-3  38918