Theorem simpl32 1252

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  initoeu2lem2  17346  mulmarep1gsum2  21279  tsmsxp  22860  ax5seg  26836  br8d  30477  br8  33243  noinfres  33514  cgrextend  33885  segconeq  33887  trisegint  33905  ifscgr  33921  cgrsub  33922  btwnxfr  33933  seglecgr12im  33987  segletr  33991  exatleN  37006  atbtwn  37048  3dim1  37069  3dim2  37070  2llnjaN  37168  4atlem10b  37207  4atlem11  37211  4atlem12  37214  2lplnj  37222  cdlemb  37396  paddasslem4  37425  pmodlem1  37448  4atex2  37679  trlval3  37789  arglem1N  37792  cdleme0moN  37827  cdleme17b  37889  cdleme20  37926  cdleme21j  37938  cdleme28c  37974  cdleme35h2  38059  cdleme38n  38066  cdlemg6c  38222  cdlemg6  38225  cdlemg7N  38228  cdlemg11a  38239  cdlemg12e  38249  cdlemg16  38259  cdlemg16ALTN  38260  cdlemg16zz  38262  cdlemg20  38287  cdlemg22  38289  cdlemg37  38291  cdlemg31d  38302  cdlemg29  38307  cdlemg33b  38309  cdlemg33  38313  cdlemg39  38318  cdlemg42  38331  cdlemk25-3  38506