Theorem simp2rr 1241

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

Assertion

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

Proof of Theorem simp2rr

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  fpr3g  8272  tfrlem5  8382  omeu  8587  gruina  10815  4sqlem18  16899  vdwlem10  16927  mdetuni0  22343  mdetmul  22345  tsmsxp  23879  ax5seglem3  28456  btwnconn1lem1  35363  btwnconn1lem3  35365  btwnconn1lem4  35366  btwnconn1lem5  35367  btwnconn1lem6  35368  btwnconn1lem7  35369  btwnconn1lem12  35374  linethru  35429  2llnjN  38741  2lplnja  38793  2lplnj  38794  cdlemblem  38967  dalaw  39060  pclfinN  39074  lhpmcvr4N  39200  cdlemb2  39215  cdleme01N  39395  cdleme0ex2N  39398  cdleme7c  39419  cdlemefrs29bpre0  39570  cdlemefrs29cpre1  39572  cdlemefrs32fva1  39575  cdlemefs32sn1aw  39588  cdleme41sn3a  39607  cdleme48fv  39673  cdlemk21-2N  40065  dihmeetlem13N  40493  pellex  41875  lmhmfgsplit  42130  iunrelexpmin1  42761