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  18222  mulmarep1gsum2  22922  tsmsxp  24507  noinfres  28112  ax5seg  29549  br8d  33277  br8  36712  cgrextend  36964  segconeq  36966  trisegint  36984  ifscgr  37000  cgrsub  37001  btwnxfr  37012  seglecgr12im  37066  segletr  37070  exatleN  40664  atbtwn  40706  3dim1  40727  3dim2  40728  2llnjaN  40826  4atlem10b  40865  4atlem11  40869  4atlem12  40872  2lplnj  40880  cdlemb  41054  paddasslem4  41083  pmodlem1  41106  4atex2  41337  trlval3  41447  arglem1N  41450  cdleme0moN  41485  cdleme17b  41547  cdleme20  41584  cdleme21j  41596  cdleme28c  41632  cdleme35h2  41717  cdleme38n  41724  cdlemg6c  41880  cdlemg6  41883  cdlemg7N  41886  cdlemg11a  41897  cdlemg12e  41907  cdlemg16  41917  cdlemg16ALTN  41918  cdlemg16zz  41920  cdlemg20  41945  cdlemg22  41947  cdlemg37  41949  cdlemg31d  41960  cdlemg29  41965  cdlemg33b  41967  cdlemg33  41971  cdlemg39  41976  cdlemg42  41989  cdlemk25-3  42164