Theorem simp2rr 1242

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

Assertion

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

Proof of Theorem simp2rr

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

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

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 1088

This theorem is referenced by:  fpr3g  8309  tfrlem5  8419  omeu  8622  gruina  10856  4sqlem18  16996  vdwlem10  17024  mdetuni0  22643  mdetmul  22645  tsmsxp  24179  ax5seglem3  28961  btwnconn1lem1  36069  btwnconn1lem3  36071  btwnconn1lem4  36072  btwnconn1lem5  36073  btwnconn1lem6  36074  btwnconn1lem7  36075  btwnconn1lem12  36080  linethru  36135  2llnjN  39550  2lplnja  39602  2lplnj  39603  cdlemblem  39776  dalaw  39869  pclfinN  39883  lhpmcvr4N  40009  cdlemb2  40024  cdleme01N  40204  cdleme0ex2N  40207  cdleme7c  40228  cdlemefrs29bpre0  40379  cdlemefrs29cpre1  40381  cdlemefrs32fva1  40384  cdlemefs32sn1aw  40397  cdleme41sn3a  40416  cdleme48fv  40482  cdlemk21-2N  40874  dihmeetlem13N  41302  pellex  42823  lmhmfgsplit  43075  iunrelexpmin1  43698