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  18026  mulmarep1gsum2  22510  tsmsxp  24091  noinfres  27684  ax5seg  28863  br8d  32536  br8  35719  cgrextend  35972  segconeq  35974  trisegint  35992  ifscgr  36008  cgrsub  36009  btwnxfr  36020  seglecgr12im  36074  segletr  36078  exatleN  39369  atbtwn  39411  3dim1  39432  3dim2  39433  2llnjaN  39531  4atlem10b  39570  4atlem11  39574  4atlem12  39577  2lplnj  39585  cdlemb  39759  paddasslem4  39788  pmodlem1  39811  4atex2  40042  trlval3  40152  arglem1N  40155  cdleme0moN  40190  cdleme17b  40252  cdleme20  40289  cdleme21j  40301  cdleme28c  40337  cdleme35h2  40422  cdleme38n  40429  cdlemg6c  40585  cdlemg6  40588  cdlemg7N  40591  cdlemg11a  40602  cdlemg12e  40612  cdlemg16  40622  cdlemg16ALTN  40623  cdlemg16zz  40625  cdlemg20  40650  cdlemg22  40652  cdlemg37  40654  cdlemg31d  40665  cdlemg29  40670  cdlemg33b  40672  cdlemg33  40676  cdlemg39  40681  cdlemg42  40694  cdlemk25-3  40869