Theorem simpl32 1246

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1078

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 208  df-an 397  df-3an 1080

This theorem is referenced by:  initoeu2lem2  17092  mulmarep1gsum2  20855  tsmsxp  22434  ax5seg  26395  br8d  30026  br8  32545  cgrextend  33023  segconeq  33025  trisegint  33043  ifscgr  33059  cgrsub  33060  btwnxfr  33071  seglecgr12im  33125  segletr  33129  exatleN  36021  atbtwn  36063  3dim1  36084  3dim2  36085  2llnjaN  36183  4atlem10b  36222  4atlem11  36226  4atlem12  36229  2lplnj  36237  cdlemb  36411  paddasslem4  36440  pmodlem1  36463  4atex2  36694  trlval3  36804  arglem1N  36807  cdleme0moN  36842  cdleme17b  36904  cdleme20  36941  cdleme21j  36953  cdleme28c  36989  cdleme35h2  37074  cdleme38n  37081  cdlemg6c  37237  cdlemg6  37240  cdlemg7N  37243  cdlemg11a  37254  cdlemg12e  37264  cdlemg16  37274  cdlemg16ALTN  37275  cdlemg16zz  37277  cdlemg20  37302  cdlemg22  37304  cdlemg37  37306  cdlemg31d  37317  cdlemg29  37322  cdlemg33b  37324  cdlemg33  37328  cdlemg39  37333  cdlemg42  37346  cdlemk25-3  37521