Theorem simpl32 1254

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  initoeu2lem2  17730  mulmarep1gsum2  21723  tsmsxp  23306  ax5seg  27306  br8d  30950  br8  33723  noinfres  33925  cgrextend  34310  segconeq  34312  trisegint  34330  ifscgr  34346  cgrsub  34347  btwnxfr  34358  seglecgr12im  34412  segletr  34416  exatleN  37418  atbtwn  37460  3dim1  37481  3dim2  37482  2llnjaN  37580  4atlem10b  37619  4atlem11  37623  4atlem12  37626  2lplnj  37634  cdlemb  37808  paddasslem4  37837  pmodlem1  37860  4atex2  38091  trlval3  38201  arglem1N  38204  cdleme0moN  38239  cdleme17b  38301  cdleme20  38338  cdleme21j  38350  cdleme28c  38386  cdleme35h2  38471  cdleme38n  38478  cdlemg6c  38634  cdlemg6  38637  cdlemg7N  38640  cdlemg11a  38651  cdlemg12e  38661  cdlemg16  38671  cdlemg16ALTN  38672  cdlemg16zz  38674  cdlemg20  38699  cdlemg22  38701  cdlemg37  38703  cdlemg31d  38714  cdlemg29  38719  cdlemg33b  38721  cdlemg33  38725  cdlemg39  38730  cdlemg42  38743  cdlemk25-3  38918