Theorem simp13r 1286

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  pceu  16841  axpasch  28870  3dimlem4  39174  3atlem4  39196  llncvrlpln2  39267  2lplnja  39329  lhpmcvr5N  39737  4atexlemswapqr  39773  4atexlemnclw  39780  trlval2  39873  cdleme21h  40044  cdleme24  40062  cdleme26ee  40070  cdleme26f  40073  cdleme26f2  40075  cdlemf1  40271  cdlemg16ALTN  40368  cdlemg17iqN  40384  cdlemg27b  40406  trlcone  40438  cdlemg48  40447  tendocan  40534  cdlemk26-3  40616  cdlemk27-3  40617  cdlemk28-3  40618  cdlemk37  40624  cdlemky  40636  cdlemk11ta  40639  cdlemkid3N  40643  cdlemk11t  40656  cdlemk46  40658  cdlemk47  40659  cdlemk51  40663  cdlemk52  40664  cdleml4N  40689  dihmeetlem1N  41000  dihmeetlem20N  41036  mapdpglem32  41415  addlimc  45303  iscnrm3rlem8  48315