Theorem simpl32 1256

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 1193	. 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:  initoeu2lem2  17924  mulmarep1gsum2  22490  tsmsxp  24071  noinfres  27662  ax5seg  28918  br8d  32593  br8  35821  cgrextend  36073  segconeq  36075  trisegint  36093  ifscgr  36109  cgrsub  36110  btwnxfr  36121  seglecgr12im  36175  segletr  36179  exatleN  39524  atbtwn  39566  3dim1  39587  3dim2  39588  2llnjaN  39686  4atlem10b  39725  4atlem11  39729  4atlem12  39732  2lplnj  39740  cdlemb  39914  paddasslem4  39943  pmodlem1  39966  4atex2  40197  trlval3  40307  arglem1N  40310  cdleme0moN  40345  cdleme17b  40407  cdleme20  40444  cdleme21j  40456  cdleme28c  40492  cdleme35h2  40577  cdleme38n  40584  cdlemg6c  40740  cdlemg6  40743  cdlemg7N  40746  cdlemg11a  40757  cdlemg12e  40767  cdlemg16  40777  cdlemg16ALTN  40778  cdlemg16zz  40780  cdlemg20  40805  cdlemg22  40807  cdlemg37  40809  cdlemg31d  40820  cdlemg29  40825  cdlemg33b  40827  cdlemg33  40831  cdlemg39  40836  cdlemg42  40849  cdlemk25-3  41024