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  18170  mulmarep1gsum2  22869  tsmsxp  24454  noinfres  28061  ax5seg  29498  br8d  33184  br8  36490  cgrextend  36743  segconeq  36745  trisegint  36763  ifscgr  36779  cgrsub  36780  btwnxfr  36791  seglecgr12im  36845  segletr  36849  exatleN  40429  atbtwn  40471  3dim1  40492  3dim2  40493  2llnjaN  40591  4atlem10b  40630  4atlem11  40634  4atlem12  40637  2lplnj  40645  cdlemb  40819  paddasslem4  40848  pmodlem1  40871  4atex2  41102  trlval3  41212  arglem1N  41215  cdleme0moN  41250  cdleme17b  41312  cdleme20  41349  cdleme21j  41361  cdleme28c  41397  cdleme35h2  41482  cdleme38n  41489  cdlemg6c  41645  cdlemg6  41648  cdlemg7N  41651  cdlemg11a  41662  cdlemg12e  41672  cdlemg16  41682  cdlemg16ALTN  41683  cdlemg16zz  41685  cdlemg20  41710  cdlemg22  41712  cdlemg37  41714  cdlemg31d  41725  cdlemg29  41730  cdlemg33b  41732  cdlemg33  41736  cdlemg39  41741  cdlemg42  41754  cdlemk25-3  41929