Theorem simpl33 1338

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  ax5seglem3a  26020  ax5seg  26028  elwwlks2ons3OLD  27092  numclwwlk1lem2foa  27529  br8d  29743  br8  31963  nosupres  32169  cgrextend  32431  segconeq  32433  trisegint  32451  ifscgr  32467  cgrsub  32468  btwnxfr  32479  seglecgr12im  32533  segletr  32537  atbtwn  35221  4atlem10b  35380  4atlem11  35384  4atlem12  35387  2lplnj  35395  paddasslem4  35598  paddasslem7  35601  pmodlem1  35621  4atex2  35852  trlval3  35962  arglem1N  35965  cdleme0moN  36000  cdleme20  36099  cdleme21j  36111  cdleme28c  36147  cdleme38n  36239  cdlemg6c  36395  cdlemg6  36398  cdlemg7N  36401  cdlemg16  36432  cdlemg16ALTN  36433  cdlemg16zz  36435  cdlemg20  36460  cdlemg22  36462  cdlemg37  36464  cdlemg31d  36475  cdlemg29  36480  cdlemg33b  36482  cdlemg33  36486  cdlemg46  36510  cdlemk25-3  36679