Theorem simpl32 1336

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  initoeu2lem2  16869  mulmarep1gsum2  20591  tsmsxp  22171  ax5seg  26032  elwwlks2ons3OLD  27096  br8d  29747  br8  31968  cgrextend  32436  segconeq  32438  trisegint  32456  ifscgr  32472  cgrsub  32473  btwnxfr  32484  seglecgr12im  32538  segletr  32542  exatleN  35184  atbtwn  35226  3dim1  35247  3dim2  35248  2llnjaN  35346  4atlem10b  35385  4atlem11  35389  4atlem12  35392  2lplnj  35400  cdlemb  35574  paddasslem4  35603  pmodlem1  35626  4atex2  35857  trlval3  35968  arglem1N  35971  cdleme0moN  36006  cdleme17b  36068  cdleme20  36105  cdleme21j  36117  cdleme28c  36153  cdleme35h2  36238  cdleme38n  36245  cdlemg6c  36401  cdlemg6  36404  cdlemg7N  36407  cdlemg11a  36418  cdlemg12e  36428  cdlemg16  36438  cdlemg16ALTN  36439  cdlemg16zz  36441  cdlemg20  36466  cdlemg22  36468  cdlemg37  36470  cdlemg31d  36481  cdlemg29  36486  cdlemg33b  36488  cdlemg33  36492  cdlemg39  36497  cdlemg42  36510  cdlemk25-3  36685