Theorem simp2rr 1262

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

Assertion

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

Proof of Theorem simp2rr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fpr3g  8287  tfrlem5  8371  omeu  8577  gruina  10884  4sqlem18  17120  vdwlem10  17148  mdetuni0  22916  mdetmul  22918  tsmsxp  24454  ax5seglem3  29491  btwnconn1lem1  36822  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem5  36826  btwnconn1lem6  36827  btwnconn1lem7  36828  btwnconn1lem12  36833  linethru  36888  2llnjN  40592  2lplnja  40644  2lplnj  40645  cdlemblem  40818  dalaw  40911  pclfinN  40925  lhpmcvr4N  41051  cdlemb2  41066  cdleme01N  41246  cdleme0ex2N  41249  cdleme7c  41270  cdlemefrs29bpre0  41421  cdlemefrs29cpre1  41423  cdlemefrs32fva1  41426  cdlemefs32sn1aw  41439  cdleme41sn3a  41458  cdleme48fv  41524  cdlemk21-2N  41916  dihmeetlem13N  42344  pellex  43795  lmhmfgsplit  44046  iunrelexpmin1  44667