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  18110  mulmarep1gsum2  22802  tsmsxp  24387  noinfres  27966  ax5seg  29403  br8d  33089  br8  36343  cgrextend  36596  segconeq  36598  trisegint  36616  ifscgr  36632  cgrsub  36633  btwnxfr  36644  seglecgr12im  36698  segletr  36702  exatleN  40285  atbtwn  40327  3dim1  40348  3dim2  40349  2llnjaN  40447  4atlem10b  40486  4atlem11  40490  4atlem12  40493  2lplnj  40501  cdlemb  40675  paddasslem4  40704  pmodlem1  40727  4atex2  40958  trlval3  41068  arglem1N  41071  cdleme0moN  41106  cdleme17b  41168  cdleme20  41205  cdleme21j  41217  cdleme28c  41253  cdleme35h2  41338  cdleme38n  41345  cdlemg6c  41501  cdlemg6  41504  cdlemg7N  41507  cdlemg11a  41518  cdlemg12e  41528  cdlemg16  41538  cdlemg16ALTN  41539  cdlemg16zz  41541  cdlemg20  41566  cdlemg22  41568  cdlemg37  41570  cdlemg31d  41581  cdlemg29  41586  cdlemg33b  41588  cdlemg33  41592  cdlemg39  41597  cdlemg42  41610  cdlemk25-3  41785