Theorem simp2rr 1243

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 1134	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

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

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 1089

This theorem is referenced by:  fpr3g  8326  tfrlem5  8436  omeu  8641  gruina  10887  4sqlem18  17009  vdwlem10  17037  mdetuni0  22648  mdetmul  22650  tsmsxp  24184  ax5seglem3  28964  btwnconn1lem1  36051  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem7  36057  btwnconn1lem12  36062  linethru  36117  2llnjN  39524  2lplnja  39576  2lplnj  39577  cdlemblem  39750  dalaw  39843  pclfinN  39857  lhpmcvr4N  39983  cdlemb2  39998  cdleme01N  40178  cdleme0ex2N  40181  cdleme7c  40202  cdlemefrs29bpre0  40353  cdlemefrs29cpre1  40355  cdlemefrs32fva1  40358  cdlemefs32sn1aw  40371  cdleme41sn3a  40390  cdleme48fv  40456  cdlemk21-2N  40848  dihmeetlem13N  41276  pellex  42791  lmhmfgsplit  43043  iunrelexpmin1  43670