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  22490  tsmsxp  24071  noinfres  27662  ax5seg  28917  br8d  32589  br8  35798  cgrextend  36048  segconeq  36050  trisegint  36068  ifscgr  36084  cgrsub  36085  btwnxfr  36096  seglecgr12im  36150  segletr  36154  exatleN  39449  atbtwn  39491  3dim1  39512  3dim2  39513  2llnjaN  39611  4atlem10b  39650  4atlem11  39654  4atlem12  39657  2lplnj  39665  cdlemb  39839  paddasslem4  39868  pmodlem1  39891  4atex2  40122  trlval3  40232  arglem1N  40235  cdleme0moN  40270  cdleme17b  40332  cdleme20  40369  cdleme21j  40381  cdleme28c  40417  cdleme35h2  40502  cdleme38n  40509  cdlemg6c  40665  cdlemg6  40668  cdlemg7N  40671  cdlemg11a  40682  cdlemg12e  40692  cdlemg16  40702  cdlemg16ALTN  40703  cdlemg16zz  40705  cdlemg20  40730  cdlemg22  40732  cdlemg37  40734  cdlemg31d  40745  cdlemg29  40750  cdlemg33b  40752  cdlemg33  40756  cdlemg39  40761  cdlemg42  40774  cdlemk25-3  40949