Theorem simpl32 1251

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  initoeu2lem2  17277  mulmarep1gsum2  21185  tsmsxp  22765  ax5seg  26726  br8d  30363  br8  32994  cgrextend  33471  segconeq  33473  trisegint  33491  ifscgr  33507  cgrsub  33508  btwnxfr  33519  seglecgr12im  33573  segletr  33577  exatleN  36542  atbtwn  36584  3dim1  36605  3dim2  36606  2llnjaN  36704  4atlem10b  36743  4atlem11  36747  4atlem12  36750  2lplnj  36758  cdlemb  36932  paddasslem4  36961  pmodlem1  36984  4atex2  37215  trlval3  37325  arglem1N  37328  cdleme0moN  37363  cdleme17b  37425  cdleme20  37462  cdleme21j  37474  cdleme28c  37510  cdleme35h2  37595  cdleme38n  37602  cdlemg6c  37758  cdlemg6  37761  cdlemg7N  37764  cdlemg11a  37775  cdlemg12e  37785  cdlemg16  37795  cdlemg16ALTN  37796  cdlemg16zz  37798  cdlemg20  37823  cdlemg22  37825  cdlemg37  37827  cdlemg31d  37838  cdlemg29  37843  cdlemg33b  37845  cdlemg33  37849  cdlemg39  37854  cdlemg42  37867  cdlemk25-3  38042