Theorem simpl32 1272

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  initoeu2lem2  18068  mulmarep1gsum2  22696  tsmsxp  24277  noinfres  27848  ax5seg  29225  br8d  32890  br8  36143  cgrextend  36395  segconeq  36397  trisegint  36415  ifscgr  36431  cgrsub  36432  btwnxfr  36443  seglecgr12im  36497  segletr  36501  exatleN  40063  atbtwn  40105  3dim1  40126  3dim2  40127  2llnjaN  40225  4atlem10b  40264  4atlem11  40268  4atlem12  40271  2lplnj  40279  cdlemb  40453  paddasslem4  40482  pmodlem1  40505  4atex2  40736  trlval3  40846  arglem1N  40849  cdleme0moN  40884  cdleme17b  40946  cdleme20  40983  cdleme21j  40995  cdleme28c  41031  cdleme35h2  41116  cdleme38n  41123  cdlemg6c  41279  cdlemg6  41282  cdlemg7N  41285  cdlemg11a  41296  cdlemg12e  41306  cdlemg16  41316  cdlemg16ALTN  41317  cdlemg16zz  41319  cdlemg20  41344  cdlemg22  41346  cdlemg37  41348  cdlemg31d  41359  cdlemg29  41364  cdlemg33b  41366  cdlemg33  41370  cdlemg39  41375  cdlemg42  41388  cdlemk25-3  41563