Theorem simp2rr 1330

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

Assertion

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

Proof of Theorem simp2rr

Step	Hyp	Ref	Expression
1		simprr 791	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1170	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  tfrlem5  7742  omeu  7932  gruina  9955  4sqlem18  16037  vdwlem10  16065  mdetuni0  20795  mdetmul  20797  tsmsxp  22328  ax5seglem3  26230  btwnconn1lem1  32733  btwnconn1lem3  32735  btwnconn1lem4  32736  btwnconn1lem5  32737  btwnconn1lem6  32738  btwnconn1lem7  32739  btwnconn1lem12  32744  linethru  32799  2llnjN  35642  2lplnja  35694  2lplnj  35695  cdlemblem  35868  dalaw  35961  pclfinN  35975  lhpmcvr4N  36101  cdlemb2  36116  cdleme01N  36296  cdleme0ex2N  36299  cdleme7c  36320  cdlemefrs29bpre0  36471  cdlemefrs29cpre1  36473  cdlemefrs32fva1  36476  cdlemefs32sn1aw  36489  cdleme41sn3a  36508  cdleme48fv  36574  cdlemk21-2N  36966  dihmeetlem13N  37394  pellex  38243  lmhmfgsplit  38499  iunrelexpmin1  38841