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  18196  mulmarep1gsum2  22895  tsmsxp  24480  noinfres  28085  ax5seg  29522  br8d  33250  br8  36614  cgrextend  36866  segconeq  36868  trisegint  36886  ifscgr  36902  cgrsub  36903  btwnxfr  36914  seglecgr12im  36968  segletr  36972  exatleN  40555  atbtwn  40597  3dim1  40618  3dim2  40619  2llnjaN  40717  4atlem10b  40756  4atlem11  40760  4atlem12  40763  2lplnj  40771  cdlemb  40945  paddasslem4  40974  pmodlem1  40997  4atex2  41228  trlval3  41338  arglem1N  41341  cdleme0moN  41376  cdleme17b  41438  cdleme20  41475  cdleme21j  41487  cdleme28c  41523  cdleme35h2  41608  cdleme38n  41615  cdlemg6c  41771  cdlemg6  41774  cdlemg7N  41777  cdlemg11a  41788  cdlemg12e  41798  cdlemg16  41808  cdlemg16ALTN  41809  cdlemg16zz  41811  cdlemg20  41836  cdlemg22  41838  cdlemg37  41840  cdlemg31d  41851  cdlemg29  41856  cdlemg33b  41858  cdlemg33  41862  cdlemg39  41867  cdlemg42  41880  cdlemk25-3  42055