Theorem simpl33 1249

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  ax5seglem3a  26399  ax5seg  26407  numclwwlk1lem2foa  27825  br8d  30051  br8  32600  nosupres  32816  cgrextend  33078  segconeq  33080  trisegint  33098  ifscgr  33114  cgrsub  33115  btwnxfr  33126  seglecgr12im  33180  segletr  33184  atbtwn  36113  4atlem10b  36272  4atlem11  36276  4atlem12  36279  2lplnj  36287  paddasslem4  36490  paddasslem7  36493  pmodlem1  36513  4atex2  36744  trlval3  36854  arglem1N  36857  cdleme0moN  36892  cdleme20  36991  cdleme21j  37003  cdleme28c  37039  cdleme38n  37131  cdlemg6c  37287  cdlemg6  37290  cdlemg7N  37293  cdlemg16  37324  cdlemg16ALTN  37325  cdlemg16zz  37327  cdlemg20  37352  cdlemg22  37354  cdlemg37  37356  cdlemg31d  37367  cdlemg29  37372  cdlemg33b  37374  cdlemg33  37378  cdlemg46  37402  cdlemk25-3  37571