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

This theorem is referenced by:  fpr3g  8085  tfrlem5  8195  omeu  8392  gruina  10558  4sqlem18  16644  vdwlem10  16672  mdetuni0  21751  mdetmul  21753  tsmsxp  23287  ax5seglem3  27280  btwnconn1lem1  34368  btwnconn1lem3  34370  btwnconn1lem4  34371  btwnconn1lem5  34372  btwnconn1lem6  34373  btwnconn1lem7  34374  btwnconn1lem12  34379  linethru  34434  2llnjN  37560  2lplnja  37612  2lplnj  37613  cdlemblem  37786  dalaw  37879  pclfinN  37893  lhpmcvr4N  38019  cdlemb2  38034  cdleme01N  38214  cdleme0ex2N  38217  cdleme7c  38238  cdlemefrs29bpre0  38389  cdlemefrs29cpre1  38391  cdlemefrs32fva1  38394  cdlemefs32sn1aw  38407  cdleme41sn3a  38426  cdleme48fv  38492  cdlemk21-2N  38884  dihmeetlem13N  39312  pellex  40637  lmhmfgsplit  40891  iunrelexpmin1  41269