Theorem simpl32 1254

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 1191	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl3 1186	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  18068  mulmarep1gsum2  22595  tsmsxp  24178  noinfres  27781  ax5seg  28967  br8d  32629  br8  35735  cgrextend  35989  segconeq  35991  trisegint  36009  ifscgr  36025  cgrsub  36026  btwnxfr  36037  seglecgr12im  36091  segletr  36095  exatleN  39386  atbtwn  39428  3dim1  39449  3dim2  39450  2llnjaN  39548  4atlem10b  39587  4atlem11  39591  4atlem12  39594  2lplnj  39602  cdlemb  39776  paddasslem4  39805  pmodlem1  39828  4atex2  40059  trlval3  40169  arglem1N  40172  cdleme0moN  40207  cdleme17b  40269  cdleme20  40306  cdleme21j  40318  cdleme28c  40354  cdleme35h2  40439  cdleme38n  40446  cdlemg6c  40602  cdlemg6  40605  cdlemg7N  40608  cdlemg11a  40619  cdlemg12e  40629  cdlemg16  40639  cdlemg16ALTN  40640  cdlemg16zz  40642  cdlemg20  40667  cdlemg22  40669  cdlemg37  40671  cdlemg31d  40682  cdlemg29  40687  cdlemg33b  40689  cdlemg33  40693  cdlemg39  40698  cdlemg42  40711  cdlemk25-3  40886