Theorem simp2rr 1243

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

Assertion

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

Proof of Theorem simp2rr

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  fpr3g  8221  tfrlem5  8331  omeu  8537  gruina  10763  4sqlem18  16845  vdwlem10  16873  mdetuni0  22007  mdetmul  22009  tsmsxp  23543  ax5seglem3  27943  btwnconn1lem1  34748  btwnconn1lem3  34750  btwnconn1lem4  34751  btwnconn1lem5  34752  btwnconn1lem6  34753  btwnconn1lem7  34754  btwnconn1lem12  34759  linethru  34814  2llnjN  38103  2lplnja  38155  2lplnj  38156  cdlemblem  38329  dalaw  38422  pclfinN  38436  lhpmcvr4N  38562  cdlemb2  38577  cdleme01N  38757  cdleme0ex2N  38760  cdleme7c  38781  cdlemefrs29bpre0  38932  cdlemefrs29cpre1  38934  cdlemefrs32fva1  38937  cdlemefs32sn1aw  38950  cdleme41sn3a  38969  cdleme48fv  39035  cdlemk21-2N  39427  dihmeetlem13N  39855  pellex  41216  lmhmfgsplit  41471  iunrelexpmin1  42102