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  27647  noinfres  27662  ax5seglem3a  28909  ax5seg  28917  numclwwlk1lem2foa  30332  br8d  32589  br8  35798  cgrextend  36048  segconeq  36050  trisegint  36068  ifscgr  36084  cgrsub  36085  btwnxfr  36096  seglecgr12im  36150  segletr  36154  atbtwn  39491  4atlem10b  39650  4atlem11  39654  4atlem12  39657  2lplnj  39665  paddasslem4  39868  paddasslem7  39871  pmodlem1  39891  4atex2  40122  trlval3  40232  arglem1N  40235  cdleme0moN  40270  cdleme20  40369  cdleme21j  40381  cdleme28c  40417  cdleme38n  40509  cdlemg6c  40665  cdlemg6  40668  cdlemg7N  40671  cdlemg16  40702  cdlemg16ALTN  40703  cdlemg16zz  40705  cdlemg20  40730  cdlemg22  40732  cdlemg37  40734  cdlemg31d  40745  cdlemg29  40750  cdlemg33b  40752  cdlemg33  40756  cdlemg46  40780  cdlemk25-3  40949