Theorem simp13r 1345

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  pceu  15955  axpasch  26290  3dimlem4  35613  3atlem4  35635  llncvrlpln2  35706  2lplnja  35768  lhpmcvr5N  36176  4atexlemswapqr  36212  4atexlemnclw  36219  trlval2  36312  cdleme21h  36483  cdleme24  36501  cdleme26ee  36509  cdleme26f  36512  cdleme26f2  36514  cdlemf1  36710  cdlemg16ALTN  36807  cdlemg17iqN  36823  cdlemg27b  36845  trlcone  36877  cdlemg48  36886  tendocan  36973  cdlemk26-3  37055  cdlemk27-3  37056  cdlemk28-3  37057  cdlemk37  37063  cdlemky  37075  cdlemk11ta  37078  cdlemkid3N  37082  cdlemk11t  37095  cdlemk46  37097  cdlemk47  37098  cdlemk51  37102  cdlemk52  37103  cdleml4N  37128  dihmeetlem1N  37439  dihmeetlem20N  37475  mapdpglem32  37854  addlimc  40781