Theorem simp2rr 1241

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

Assertion

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

Proof of Theorem simp2rr

Step	Hyp	Ref	Expression
1		simprr 772	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1132	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:  fpr3g  8290  tfrlem5  8400  omeu  8605  gruina  10841  4sqlem18  16930  vdwlem10  16958  mdetuni0  22522  mdetmul  22524  tsmsxp  24058  ax5seglem3  28741  btwnconn1lem1  35683  btwnconn1lem3  35685  btwnconn1lem4  35686  btwnconn1lem5  35687  btwnconn1lem6  35688  btwnconn1lem7  35689  btwnconn1lem12  35694  linethru  35749  2llnjN  39040  2lplnja  39092  2lplnj  39093  cdlemblem  39266  dalaw  39359  pclfinN  39373  lhpmcvr4N  39499  cdlemb2  39514  cdleme01N  39694  cdleme0ex2N  39697  cdleme7c  39718  cdlemefrs29bpre0  39869  cdlemefrs29cpre1  39871  cdlemefrs32fva1  39874  cdlemefs32sn1aw  39887  cdleme41sn3a  39906  cdleme48fv  39972  cdlemk21-2N  40364  dihmeetlem13N  40792  pellex  42255  lmhmfgsplit  42510  iunrelexpmin1  43138