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  16817  axpasch  29010  3dimlem4  39910  3atlem4  39932  llncvrlpln2  40003  2lplnja  40065  lhpmcvr5N  40473  4atexlemswapqr  40509  4atexlemnclw  40516  trlval2  40609  cdleme21h  40780  cdleme24  40798  cdleme26ee  40806  cdleme26f  40809  cdleme26f2  40811  cdlemf1  41007  cdlemg16ALTN  41104  cdlemg17iqN  41120  cdlemg27b  41142  trlcone  41174  cdlemg48  41183  tendocan  41270  cdlemk26-3  41352  cdlemk27-3  41353  cdlemk28-3  41354  cdlemk37  41360  cdlemky  41372  cdlemk11ta  41375  cdlemkid3N  41379  cdlemk11t  41392  cdlemk46  41394  cdlemk47  41395  cdlemk51  41399  cdlemk52  41400  cdleml4N  41425  dihmeetlem1N  41736  dihmeetlem20N  41772  mapdpglem32  42151  addlimc  46076  iscnrm3rlem8  49422