Theorem simp13r 1170

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

Assertion

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

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1083	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1075	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:  pceu  15389  axpasch  25621  3dimlem4  33768  3atlem4  33790  llncvrlpln2  33861  2lplnja  33923  lhpmcvr5N  34331  4atexlemswapqr  34367  4atexlemnclw  34374  trlval2  34468  cdleme21h  34640  cdleme24  34658  cdleme26ee  34666  cdleme26f  34669  cdleme26f2  34671  cdlemf1  34867  cdlemg16ALTN  34964  cdlemg17iqN  34980  cdlemg27b  35002  trlcone  35034  cdlemg48  35043  tendocan  35130  cdlemk26-3  35212  cdlemk27-3  35213  cdlemk28-3  35214  cdlemk37  35220  cdlemky  35232  cdlemk11ta  35235  cdlemkid3N  35239  cdlemk11t  35252  cdlemk46  35254  cdlemk47  35255  cdlemk51  35259  cdlemk52  35260  cdleml4N  35285  dihmeetlem1N  35597  dihmeetlem20N  35633  mapdpglem32  36012  addlimc  38715