Theorem simp13r 1291

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

Assertion

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

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1204	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1134	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pceu  16808  axpasch  29024  3dimlem4  39924  3atlem4  39946  llncvrlpln2  40017  2lplnja  40079  lhpmcvr5N  40487  4atexlemswapqr  40523  4atexlemnclw  40530  trlval2  40623  cdleme21h  40794  cdleme24  40812  cdleme26ee  40820  cdleme26f  40823  cdleme26f2  40825  cdlemf1  41021  cdlemg16ALTN  41118  cdlemg17iqN  41134  cdlemg27b  41156  trlcone  41188  cdlemg48  41197  tendocan  41284  cdlemk26-3  41366  cdlemk27-3  41367  cdlemk28-3  41368  cdlemk37  41374  cdlemky  41386  cdlemk11ta  41389  cdlemkid3N  41393  cdlemk11t  41406  cdlemk46  41408  cdlemk47  41409  cdlemk51  41413  cdlemk52  41414  cdleml4N  41439  dihmeetlem1N  41750  dihmeetlem20N  41786  mapdpglem32  42165  addlimc  46094  iscnrm3rlem8  49434