Theorem simp13r 1307

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

Assertion

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

Proof of Theorem simp13r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  pceu  16912  axpasch  29302  3dimlem4  40266  3atlem4  40288  llncvrlpln2  40359  2lplnja  40421  lhpmcvr5N  40829  4atexlemswapqr  40865  4atexlemnclw  40872  trlval2  40965  cdleme21h  41136  cdleme24  41154  cdleme26ee  41162  cdleme26f  41165  cdleme26f2  41167  cdlemf1  41363  cdlemg16ALTN  41460  cdlemg17iqN  41476  cdlemg27b  41498  trlcone  41530  cdlemg48  41539  tendocan  41626  cdlemk26-3  41708  cdlemk27-3  41709  cdlemk28-3  41710  cdlemk37  41716  cdlemky  41728  cdlemk11ta  41731  cdlemkid3N  41735  cdlemk11t  41748  cdlemk46  41750  cdlemk47  41751  cdlemk51  41755  cdlemk52  41756  cdleml4N  41781  dihmeetlem1N  42092  dihmeetlem20N  42128  mapdpglem32  42507  addlimc  46390  iscnrm3rlem8  49753