Theorem simp13r 1296

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

Assertion

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

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1209	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1139	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:  pceu  16815  axpasch  29035  3dimlem4  39963  3atlem4  39985  llncvrlpln2  40056  2lplnja  40118  lhpmcvr5N  40526  4atexlemswapqr  40562  4atexlemnclw  40569  trlval2  40662  cdleme21h  40833  cdleme24  40851  cdleme26ee  40859  cdleme26f  40862  cdleme26f2  40864  cdlemf1  41060  cdlemg16ALTN  41157  cdlemg17iqN  41173  cdlemg27b  41195  trlcone  41227  cdlemg48  41236  tendocan  41323  cdlemk26-3  41405  cdlemk27-3  41406  cdlemk28-3  41407  cdlemk37  41413  cdlemky  41425  cdlemk11ta  41428  cdlemkid3N  41432  cdlemk11t  41445  cdlemk46  41447  cdlemk47  41448  cdlemk51  41452  cdlemk52  41453  cdleml4N  41478  dihmeetlem1N  41789  dihmeetlem20N  41825  mapdpglem32  42204  addlimc  46098  iscnrm3rlem8  49444