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 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  nosupres  27635  noinfres  27650  ax5seglem3a  28893  ax5seg  28901  numclwwlk1lem2foa  30316  br8d  32571  br8  35731  cgrextend  35984  segconeq  35986  trisegint  36004  ifscgr  36020  cgrsub  36021  btwnxfr  36032  seglecgr12im  36086  segletr  36090  atbtwn  39428  4atlem10b  39587  4atlem11  39591  4atlem12  39594  2lplnj  39602  paddasslem4  39805  paddasslem7  39808  pmodlem1  39828  4atex2  40059  trlval3  40169  arglem1N  40172  cdleme0moN  40207  cdleme20  40306  cdleme21j  40318  cdleme28c  40354  cdleme38n  40446  cdlemg6c  40602  cdlemg6  40605  cdlemg7N  40608  cdlemg16  40639  cdlemg16ALTN  40640  cdlemg16zz  40642  cdlemg20  40667  cdlemg22  40669  cdlemg37  40671  cdlemg31d  40682  cdlemg29  40687  cdlemg33b  40689  cdlemg33  40693  cdlemg46  40717  cdlemk25-3  40886