Theorem simp13r 1287

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  pceu  16475  axpasch  27212  3dimlem4  37405  3atlem4  37427  llncvrlpln2  37498  2lplnja  37560  lhpmcvr5N  37968  4atexlemswapqr  38004  4atexlemnclw  38011  trlval2  38104  cdleme21h  38275  cdleme24  38293  cdleme26ee  38301  cdleme26f  38304  cdleme26f2  38306  cdlemf1  38502  cdlemg16ALTN  38599  cdlemg17iqN  38615  cdlemg27b  38637  trlcone  38669  cdlemg48  38678  tendocan  38765  cdlemk26-3  38847  cdlemk27-3  38848  cdlemk28-3  38849  cdlemk37  38855  cdlemky  38867  cdlemk11ta  38870  cdlemkid3N  38874  cdlemk11t  38887  cdlemk46  38889  cdlemk47  38890  cdlemk51  38894  cdlemk52  38895  cdleml4N  38920  dihmeetlem1N  39231  dihmeetlem20N  39267  mapdpglem32  39646  addlimc  43079  iscnrm3rlem8  46129