Theorem simp13r 1302

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  pceu  16872  axpasch  29098  3dimlem4  40048  3atlem4  40070  llncvrlpln2  40141  2lplnja  40203  lhpmcvr5N  40611  4atexlemswapqr  40647  4atexlemnclw  40654  trlval2  40747  cdleme21h  40918  cdleme24  40936  cdleme26ee  40944  cdleme26f  40947  cdleme26f2  40949  cdlemf1  41145  cdlemg16ALTN  41242  cdlemg17iqN  41258  cdlemg27b  41280  trlcone  41312  cdlemg48  41321  tendocan  41408  cdlemk26-3  41490  cdlemk27-3  41491  cdlemk28-3  41492  cdlemk37  41498  cdlemky  41510  cdlemk11ta  41513  cdlemkid3N  41517  cdlemk11t  41530  cdlemk46  41532  cdlemk47  41533  cdlemk51  41537  cdlemk52  41538  cdleml4N  41563  dihmeetlem1N  41874  dihmeetlem20N  41910  mapdpglem32  42289  addlimc  46182  iscnrm3rlem8  49528