Theorem simp13r 1290

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

Assertion

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

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1203	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1134	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  16884  axpasch  28956  3dimlem4  39466  3atlem4  39488  llncvrlpln2  39559  2lplnja  39621  lhpmcvr5N  40029  4atexlemswapqr  40065  4atexlemnclw  40072  trlval2  40165  cdleme21h  40336  cdleme24  40354  cdleme26ee  40362  cdleme26f  40365  cdleme26f2  40367  cdlemf1  40563  cdlemg16ALTN  40660  cdlemg17iqN  40676  cdlemg27b  40698  trlcone  40730  cdlemg48  40739  tendocan  40826  cdlemk26-3  40908  cdlemk27-3  40909  cdlemk28-3  40910  cdlemk37  40916  cdlemky  40928  cdlemk11ta  40931  cdlemkid3N  40935  cdlemk11t  40948  cdlemk46  40950  cdlemk47  40951  cdlemk51  40955  cdlemk52  40956  cdleml4N  40981  dihmeetlem1N  41292  dihmeetlem20N  41328  mapdpglem32  41707  addlimc  45663  iscnrm3rlem8  48844