Theorem simpl33 1330

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  ax5seglem3a  26031  ax5seg  26039  elwwlks2ons3OLD  27103  numclwwlk1lem2foa  27540  br8d  29760  br8  31984  nosupres  32190  cgrextend  32452  segconeq  32454  trisegint  32472  ifscgr  32488  cgrsub  32489  btwnxfr  32500  seglecgr12im  32554  segletr  32558  atbtwn  35254  4atlem10b  35413  4atlem11  35417  4atlem12  35420  2lplnj  35428  paddasslem4  35631  paddasslem7  35634  pmodlem1  35654  4atex2  35885  trlval3  35996  arglem1N  35999  cdleme0moN  36034  cdleme20  36133  cdleme21j  36145  cdleme28c  36181  cdleme38n  36273  cdlemg6c  36429  cdlemg6  36432  cdlemg7N  36435  cdlemg16  36466  cdlemg16ALTN  36467  cdlemg16zz  36469  cdlemg20  36494  cdlemg22  36496  cdlemg37  36498  cdlemg31d  36509  cdlemg29  36514  cdlemg33b  36516  cdlemg33  36520  cdlemg46  36544  cdlemk25-3  36713