Theorem simpl33 1252

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem3a  26719  ax5seg  26727  numclwwlk1lem2foa  28136  br8d  30364  br8  32996  nosupres  33211  cgrextend  33473  segconeq  33475  trisegint  33493  ifscgr  33509  cgrsub  33510  btwnxfr  33521  seglecgr12im  33575  segletr  33579  atbtwn  36586  4atlem10b  36745  4atlem11  36749  4atlem12  36752  2lplnj  36760  paddasslem4  36963  paddasslem7  36966  pmodlem1  36986  4atex2  37217  trlval3  37327  arglem1N  37330  cdleme0moN  37365  cdleme20  37464  cdleme21j  37476  cdleme28c  37512  cdleme38n  37604  cdlemg6c  37760  cdlemg6  37763  cdlemg7N  37766  cdlemg16  37797  cdlemg16ALTN  37798  cdlemg16zz  37800  cdlemg20  37825  cdlemg22  37827  cdlemg37  37829  cdlemg31d  37840  cdlemg29  37845  cdlemg33b  37847  cdlemg33  37851  cdlemg46  37875  cdlemk25-3  38044