Theorem simpl32 1256

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

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

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 1088

This theorem is referenced by:  initoeu2lem2  17922  mulmarep1gsum2  22489  tsmsxp  24070  noinfres  27661  ax5seg  28916  br8d  32591  br8  35800  cgrextend  36052  segconeq  36054  trisegint  36072  ifscgr  36088  cgrsub  36089  btwnxfr  36100  seglecgr12im  36154  segletr  36158  exatleN  39502  atbtwn  39544  3dim1  39565  3dim2  39566  2llnjaN  39664  4atlem10b  39703  4atlem11  39707  4atlem12  39710  2lplnj  39718  cdlemb  39892  paddasslem4  39921  pmodlem1  39944  4atex2  40175  trlval3  40285  arglem1N  40288  cdleme0moN  40323  cdleme17b  40385  cdleme20  40422  cdleme21j  40434  cdleme28c  40470  cdleme35h2  40555  cdleme38n  40562  cdlemg6c  40718  cdlemg6  40721  cdlemg7N  40724  cdlemg11a  40735  cdlemg12e  40745  cdlemg16  40755  cdlemg16ALTN  40756  cdlemg16zz  40758  cdlemg20  40783  cdlemg22  40785  cdlemg37  40787  cdlemg31d  40798  cdlemg29  40803  cdlemg33b  40805  cdlemg33  40809  cdlemg39  40814  cdlemg42  40827  cdlemk25-3  41002