Theorem simp2rr 1244

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

Assertion

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

Proof of Theorem simp2rr

Step	Hyp	Ref	Expression
1		simprr 773	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1135	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  8310  tfrlem5  8420  omeu  8623  gruina  10858  4sqlem18  17000  vdwlem10  17028  mdetuni0  22627  mdetmul  22629  tsmsxp  24163  ax5seglem3  28946  btwnconn1lem1  36088  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem7  36094  btwnconn1lem12  36099  linethru  36154  2llnjN  39569  2lplnja  39621  2lplnj  39622  cdlemblem  39795  dalaw  39888  pclfinN  39902  lhpmcvr4N  40028  cdlemb2  40043  cdleme01N  40223  cdleme0ex2N  40226  cdleme7c  40247  cdlemefrs29bpre0  40398  cdlemefrs29cpre1  40400  cdlemefrs32fva1  40403  cdlemefs32sn1aw  40416  cdleme41sn3a  40435  cdleme48fv  40501  cdlemk21-2N  40893  dihmeetlem13N  41321  pellex  42846  lmhmfgsplit  43098  iunrelexpmin1  43721