Theorem simpl32 1136

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl32	⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl32

Step	Hyp	Ref	Expression
1		simp32 1091	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓)
2	1	adantr 480	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  initoeu2lem2  16488  mulmarep1gsum2  20199  tsmsxp  21768  ax5seg  25618  br8d  28802  br8  30899  cgrextend  31285  segconeq  31287  trisegint  31305  ifscgr  31321  cgrsub  31322  btwnxfr  31333  seglecgr12im  31387  segletr  31391  exatleN  33708  atbtwn  33750  3dim1  33771  3dim2  33772  2llnjaN  33870  4atlem10b  33909  4atlem11  33913  4atlem12  33916  2lplnj  33924  cdlemb  34098  paddasslem4  34127  pmodlem1  34150  4atex2  34381  trlval3  34492  arglem1N  34495  cdleme0moN  34530  cdleme17b  34592  cdleme20  34630  cdleme21j  34642  cdleme28c  34678  cdleme35h2  34763  cdleme38n  34770  cdlemg6c  34926  cdlemg6  34929  cdlemg7N  34932  cdlemg11a  34943  cdlemg12e  34953  cdlemg16  34963  cdlemg16ALTN  34964  cdlemg16zz  34966  cdlemg20  34991  cdlemg22  34993  cdlemg37  34995  cdlemg31d  35006  cdlemg29  35011  cdlemg33b  35013  cdlemg33  35017  cdlemg39  35022  cdlemg42  35035  cdlemk25-3  35210  elwwlks2ons3  41159