Theorem simp2rr 1260

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

Assertion

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

Proof of Theorem simp2rr

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  fpr3g  8270  tfrlem5  8354  omeu  8558  gruina  10791  4sqlem18  17012  vdwlem10  17040  mdetuni0  22739  mdetmul  22741  tsmsxp  24273  ax5seglem3  29190  btwnconn1lem1  36450  btwnconn1lem3  36452  btwnconn1lem4  36453  btwnconn1lem5  36454  btwnconn1lem6  36455  btwnconn1lem7  36456  btwnconn1lem12  36461  linethru  36516  2llnjN  40203  2lplnja  40255  2lplnj  40256  cdlemblem  40429  dalaw  40522  pclfinN  40536  lhpmcvr4N  40662  cdlemb2  40677  cdleme01N  40857  cdleme0ex2N  40860  cdleme7c  40881  cdlemefrs29bpre0  41032  cdlemefrs29cpre1  41034  cdlemefrs32fva1  41037  cdlemefs32sn1aw  41050  cdleme41sn3a  41069  cdleme48fv  41135  cdlemk21-2N  41527  dihmeetlem13N  41955  pellex  43424  lmhmfgsplit  43675  iunrelexpmin1  44296