Theorem simpl33 1275

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  nosupres  27908  noinfres  27923  ax5seglem3a  29317  ax5seg  29325  numclwwlk1lem2foa  30742  br8d  32990  br8  36269  cgrextend  36521  segconeq  36523  trisegint  36541  ifscgr  36557  cgrsub  36558  btwnxfr  36569  seglecgr12im  36623  segletr  36627  atbtwn  40261  4atlem10b  40420  4atlem11  40424  4atlem12  40427  2lplnj  40435  paddasslem4  40638  paddasslem7  40641  pmodlem1  40661  4atex2  40892  trlval3  41002  arglem1N  41005  cdleme0moN  41040  cdleme20  41139  cdleme21j  41151  cdleme28c  41187  cdleme38n  41279  cdlemg6c  41435  cdlemg6  41438  cdlemg7N  41441  cdlemg16  41472  cdlemg16ALTN  41473  cdlemg16zz  41475  cdlemg20  41500  cdlemg22  41502  cdlemg37  41504  cdlemg31d  41515  cdlemg29  41520  cdlemg33b  41522  cdlemg33  41526  cdlemg46  41550  cdlemk25-3  41719