Theorem simp13r 1290

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

Assertion

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

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1203	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1133	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:  pceu  16758  axpasch  28920  3dimlem4  39509  3atlem4  39531  llncvrlpln2  39602  2lplnja  39664  lhpmcvr5N  40072  4atexlemswapqr  40108  4atexlemnclw  40115  trlval2  40208  cdleme21h  40379  cdleme24  40397  cdleme26ee  40405  cdleme26f  40408  cdleme26f2  40410  cdlemf1  40606  cdlemg16ALTN  40703  cdlemg17iqN  40719  cdlemg27b  40741  trlcone  40773  cdlemg48  40782  tendocan  40869  cdlemk26-3  40951  cdlemk27-3  40952  cdlemk28-3  40953  cdlemk37  40959  cdlemky  40971  cdlemk11ta  40974  cdlemkid3N  40978  cdlemk11t  40991  cdlemk46  40993  cdlemk47  40994  cdlemk51  40998  cdlemk52  40999  cdleml4N  41024  dihmeetlem1N  41335  dihmeetlem20N  41371  mapdpglem32  41750  addlimc  45692  iscnrm3rlem8  48984