Theorem simpl32 1257

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  initoeu2lem2  17951  mulmarep1gsum2  22530  tsmsxp  24111  noinfres  27702  ax5seg  29023  br8d  32697  br8  35969  cgrextend  36221  segconeq  36223  trisegint  36241  ifscgr  36257  cgrsub  36258  btwnxfr  36269  seglecgr12im  36323  segletr  36327  exatleN  39777  atbtwn  39819  3dim1  39840  3dim2  39841  2llnjaN  39939  4atlem10b  39978  4atlem11  39982  4atlem12  39985  2lplnj  39993  cdlemb  40167  paddasslem4  40196  pmodlem1  40219  4atex2  40450  trlval3  40560  arglem1N  40563  cdleme0moN  40598  cdleme17b  40660  cdleme20  40697  cdleme21j  40709  cdleme28c  40745  cdleme35h2  40830  cdleme38n  40837  cdlemg6c  40993  cdlemg6  40996  cdlemg7N  40999  cdlemg11a  41010  cdlemg12e  41020  cdlemg16  41030  cdlemg16ALTN  41031  cdlemg16zz  41033  cdlemg20  41058  cdlemg22  41060  cdlemg37  41062  cdlemg31d  41073  cdlemg29  41078  cdlemg33b  41080  cdlemg33  41084  cdlemg39  41089  cdlemg42  41102  cdlemk25-3  41277