Theorem simp2rr 1250

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

Assertion

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

Proof of Theorem simp2rr

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  fpr3g  8232  tfrlem5  8316  omeu  8517  gruina  10739  4sqlem18  16931  vdwlem10  16959  mdetuni0  22611  mdetmul  22613  tsmsxp  24145  ax5seglem3  29025  btwnconn1lem1  36322  btwnconn1lem3  36324  btwnconn1lem4  36325  btwnconn1lem5  36326  btwnconn1lem6  36327  btwnconn1lem7  36328  btwnconn1lem12  36333  linethru  36388  2llnjN  40066  2lplnja  40118  2lplnj  40119  cdlemblem  40292  dalaw  40385  pclfinN  40399  lhpmcvr4N  40525  cdlemb2  40540  cdleme01N  40720  cdleme0ex2N  40723  cdleme7c  40744  cdlemefrs29bpre0  40895  cdlemefrs29cpre1  40897  cdlemefrs32fva1  40900  cdlemefs32sn1aw  40913  cdleme41sn3a  40932  cdleme48fv  40998  cdlemk21-2N  41390  dihmeetlem13N  41818  pellex  43287  lmhmfgsplit  43538  iunrelexpmin1  44159