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  8334  tfrlem5  8418  omeu  8624  gruina  10933  4sqlem18  17172  vdwlem10  17200  mdetuni0  22969  mdetmul  22971  tsmsxp  24507  ax5seglem3  29542  btwnconn1lem1  37043  btwnconn1lem3  37045  btwnconn1lem4  37046  btwnconn1lem5  37047  btwnconn1lem6  37048  btwnconn1lem7  37049  btwnconn1lem12  37054  linethru  37109  2llnjN  40827  2lplnja  40879  2lplnj  40880  cdlemblem  41053  dalaw  41146  pclfinN  41160  lhpmcvr4N  41286  cdlemb2  41301  cdleme01N  41481  cdleme0ex2N  41484  cdleme7c  41505  cdlemefrs29bpre0  41656  cdlemefrs29cpre1  41658  cdlemefrs32fva1  41661  cdlemefs32sn1aw  41674  cdleme41sn3a  41693  cdleme48fv  41759  cdlemk21-2N  42151  dihmeetlem13N  42579  pellex  44046  lmhmfgsplit  44292  iunrelexpmin1  44911