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  17940  mulmarep1gsum2  22477  tsmsxp  24058  noinfres  27650  ax5seg  28901  br8d  32571  br8  35728  cgrextend  35981  segconeq  35983  trisegint  36001  ifscgr  36017  cgrsub  36018  btwnxfr  36029  seglecgr12im  36083  segletr  36087  exatleN  39383  atbtwn  39425  3dim1  39446  3dim2  39447  2llnjaN  39545  4atlem10b  39584  4atlem11  39588  4atlem12  39591  2lplnj  39599  cdlemb  39773  paddasslem4  39802  pmodlem1  39825  4atex2  40056  trlval3  40166  arglem1N  40169  cdleme0moN  40204  cdleme17b  40266  cdleme20  40303  cdleme21j  40315  cdleme28c  40351  cdleme35h2  40436  cdleme38n  40443  cdlemg6c  40599  cdlemg6  40602  cdlemg7N  40605  cdlemg11a  40616  cdlemg12e  40626  cdlemg16  40636  cdlemg16ALTN  40637  cdlemg16zz  40639  cdlemg20  40664  cdlemg22  40666  cdlemg37  40668  cdlemg31d  40679  cdlemg29  40684  cdlemg33b  40686  cdlemg33  40690  cdlemg39  40695  cdlemg42  40708  cdlemk25-3  40883