Theorem simpl33 1258

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  nosupres  27687  noinfres  27702  ax5seglem3a  29015  ax5seg  29023  numclwwlk1lem2foa  30441  br8d  32697  br8  35969  cgrextend  36221  segconeq  36223  trisegint  36241  ifscgr  36257  cgrsub  36258  btwnxfr  36269  seglecgr12im  36323  segletr  36327  atbtwn  39819  4atlem10b  39978  4atlem11  39982  4atlem12  39985  2lplnj  39993  paddasslem4  40196  paddasslem7  40199  pmodlem1  40219  4atex2  40450  trlval3  40560  arglem1N  40563  cdleme0moN  40598  cdleme20  40697  cdleme21j  40709  cdleme28c  40745  cdleme38n  40837  cdlemg6c  40993  cdlemg6  40996  cdlemg7N  40999  cdlemg16  41030  cdlemg16ALTN  41031  cdlemg16zz  41033  cdlemg20  41058  cdlemg22  41060  cdlemg37  41062  cdlemg31d  41073  cdlemg29  41078  cdlemg33b  41080  cdlemg33  41084  cdlemg46  41108  cdlemk25-3  41277