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 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  initoeu2lem2  18073  mulmarep1gsum2  22712  tsmsxp  24293  noinfres  27867  ax5seg  29269  br8d  32934  br8  36229  cgrextend  36481  segconeq  36483  trisegint  36501  ifscgr  36517  cgrsub  36518  btwnxfr  36529  seglecgr12im  36583  segletr  36587  exatleN  40159  atbtwn  40201  3dim1  40222  3dim2  40223  2llnjaN  40321  4atlem10b  40360  4atlem11  40364  4atlem12  40367  2lplnj  40375  cdlemb  40549  paddasslem4  40578  pmodlem1  40601  4atex2  40832  trlval3  40942  arglem1N  40945  cdleme0moN  40980  cdleme17b  41042  cdleme20  41079  cdleme21j  41091  cdleme28c  41127  cdleme35h2  41212  cdleme38n  41219  cdlemg6c  41375  cdlemg6  41378  cdlemg7N  41381  cdlemg11a  41392  cdlemg12e  41402  cdlemg16  41412  cdlemg16ALTN  41413  cdlemg16zz  41415  cdlemg20  41440  cdlemg22  41442  cdlemg37  41444  cdlemg31d  41455  cdlemg29  41460  cdlemg33b  41462  cdlemg33  41466  cdlemg39  41471  cdlemg42  41484  cdlemk25-3  41659