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  17984  mulmarep1gsum2  22468  tsmsxp  24049  noinfres  27641  ax5seg  28872  br8d  32545  br8  35750  cgrextend  36003  segconeq  36005  trisegint  36023  ifscgr  36039  cgrsub  36040  btwnxfr  36051  seglecgr12im  36105  segletr  36109  exatleN  39405  atbtwn  39447  3dim1  39468  3dim2  39469  2llnjaN  39567  4atlem10b  39606  4atlem11  39610  4atlem12  39613  2lplnj  39621  cdlemb  39795  paddasslem4  39824  pmodlem1  39847  4atex2  40078  trlval3  40188  arglem1N  40191  cdleme0moN  40226  cdleme17b  40288  cdleme20  40325  cdleme21j  40337  cdleme28c  40373  cdleme35h2  40458  cdleme38n  40465  cdlemg6c  40621  cdlemg6  40624  cdlemg7N  40627  cdlemg11a  40638  cdlemg12e  40648  cdlemg16  40658  cdlemg16ALTN  40659  cdlemg16zz  40661  cdlemg20  40686  cdlemg22  40688  cdlemg37  40690  cdlemg31d  40701  cdlemg29  40706  cdlemg33b  40708  cdlemg33  40712  cdlemg39  40717  cdlemg42  40730  cdlemk25-3  40905