Theorem simp13r 1289

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

Assertion

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

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1202	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1133	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  16893  axpasch  28974  3dimlem4  39421  3atlem4  39443  llncvrlpln2  39514  2lplnja  39576  lhpmcvr5N  39984  4atexlemswapqr  40020  4atexlemnclw  40027  trlval2  40120  cdleme21h  40291  cdleme24  40309  cdleme26ee  40317  cdleme26f  40320  cdleme26f2  40322  cdlemf1  40518  cdlemg16ALTN  40615  cdlemg17iqN  40631  cdlemg27b  40653  trlcone  40685  cdlemg48  40694  tendocan  40781  cdlemk26-3  40863  cdlemk27-3  40864  cdlemk28-3  40865  cdlemk37  40871  cdlemky  40883  cdlemk11ta  40886  cdlemkid3N  40890  cdlemk11t  40903  cdlemk46  40905  cdlemk47  40906  cdlemk51  40910  cdlemk52  40911  cdleml4N  40936  dihmeetlem1N  41247  dihmeetlem20N  41283  mapdpglem32  41662  addlimc  45569  iscnrm3rlem8  48627