Theorem simpl32 1262

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

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

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 1094

This theorem is referenced by:  initoeu2lem2  17980  mulmarep1gsum2  22564  tsmsxp  24145  noinfres  27711  ax5seg  29032  br8d  32707  br8  35991  cgrextend  36243  segconeq  36245  trisegint  36263  ifscgr  36279  cgrsub  36280  btwnxfr  36291  seglecgr12im  36345  segletr  36349  exatleN  39903  atbtwn  39945  3dim1  39966  3dim2  39967  2llnjaN  40065  4atlem10b  40104  4atlem11  40108  4atlem12  40111  2lplnj  40119  cdlemb  40293  paddasslem4  40322  pmodlem1  40345  4atex2  40576  trlval3  40686  arglem1N  40689  cdleme0moN  40724  cdleme17b  40786  cdleme20  40823  cdleme21j  40835  cdleme28c  40871  cdleme35h2  40956  cdleme38n  40963  cdlemg6c  41119  cdlemg6  41122  cdlemg7N  41125  cdlemg11a  41136  cdlemg12e  41146  cdlemg16  41156  cdlemg16ALTN  41157  cdlemg16zz  41159  cdlemg20  41184  cdlemg22  41186  cdlemg37  41188  cdlemg31d  41199  cdlemg29  41204  cdlemg33b  41206  cdlemg33  41210  cdlemg39  41215  cdlemg42  41228  cdlemk25-3  41403