Theorem simpl32 1253

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  initoeu2lem2  17969  mulmarep1gsum2  22296  tsmsxp  23879  noinfres  27461  ax5seg  28463  br8d  32106  br8  35030  cgrextend  35284  segconeq  35286  trisegint  35304  ifscgr  35320  cgrsub  35321  btwnxfr  35332  seglecgr12im  35386  segletr  35390  exatleN  38578  atbtwn  38620  3dim1  38641  3dim2  38642  2llnjaN  38740  4atlem10b  38779  4atlem11  38783  4atlem12  38786  2lplnj  38794  cdlemb  38968  paddasslem4  38997  pmodlem1  39020  4atex2  39251  trlval3  39361  arglem1N  39364  cdleme0moN  39399  cdleme17b  39461  cdleme20  39498  cdleme21j  39510  cdleme28c  39546  cdleme35h2  39631  cdleme38n  39638  cdlemg6c  39794  cdlemg6  39797  cdlemg7N  39800  cdlemg11a  39811  cdlemg12e  39821  cdlemg16  39831  cdlemg16ALTN  39832  cdlemg16zz  39834  cdlemg20  39859  cdlemg22  39861  cdlemg37  39863  cdlemg31d  39874  cdlemg29  39879  cdlemg33b  39881  cdlemg33  39885  cdlemg39  39890  cdlemg42  39903  cdlemk25-3  40078