Theorem simpl32 1274

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl32	⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl32

Step	Hyp	Ref	Expression
1		simpl2 1211	. 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:  initoeu2lem2  18097  mulmarep1gsum2  22768  tsmsxp  24349  noinfres  27923  ax5seg  29325  br8d  32990  br8  36269  cgrextend  36521  segconeq  36523  trisegint  36541  ifscgr  36557  cgrsub  36558  btwnxfr  36569  seglecgr12im  36623  segletr  36627  exatleN  40219  atbtwn  40261  3dim1  40282  3dim2  40283  2llnjaN  40381  4atlem10b  40420  4atlem11  40424  4atlem12  40427  2lplnj  40435  cdlemb  40609  paddasslem4  40638  pmodlem1  40661  4atex2  40892  trlval3  41002  arglem1N  41005  cdleme0moN  41040  cdleme17b  41102  cdleme20  41139  cdleme21j  41151  cdleme28c  41187  cdleme35h2  41272  cdleme38n  41279  cdlemg6c  41435  cdlemg6  41438  cdlemg7N  41441  cdlemg11a  41452  cdlemg12e  41462  cdlemg16  41472  cdlemg16ALTN  41473  cdlemg16zz  41475  cdlemg20  41500  cdlemg22  41502  cdlemg37  41504  cdlemg31d  41515  cdlemg29  41520  cdlemg33b  41522  cdlemg33  41526  cdlemg39  41531  cdlemg42  41544  cdlemk25-3  41719