Theorem simpl32 1252

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

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

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 1086

This theorem is referenced by:  initoeu2lem2  18037  mulmarep1gsum2  22567  tsmsxp  24150  noinfres  27752  ax5seg  28872  br8d  32530  br8  35578  cgrextend  35832  segconeq  35834  trisegint  35852  ifscgr  35868  cgrsub  35869  btwnxfr  35880  seglecgr12im  35934  segletr  35938  exatleN  39103  atbtwn  39145  3dim1  39166  3dim2  39167  2llnjaN  39265  4atlem10b  39304  4atlem11  39308  4atlem12  39311  2lplnj  39319  cdlemb  39493  paddasslem4  39522  pmodlem1  39545  4atex2  39776  trlval3  39886  arglem1N  39889  cdleme0moN  39924  cdleme17b  39986  cdleme20  40023  cdleme21j  40035  cdleme28c  40071  cdleme35h2  40156  cdleme38n  40163  cdlemg6c  40319  cdlemg6  40322  cdlemg7N  40325  cdlemg11a  40336  cdlemg12e  40346  cdlemg16  40356  cdlemg16ALTN  40357  cdlemg16zz  40359  cdlemg20  40384  cdlemg22  40386  cdlemg37  40388  cdlemg31d  40399  cdlemg29  40404  cdlemg33b  40406  cdlemg33  40410  cdlemg39  40415  cdlemg42  40428  cdlemk25-3  40603