Theorem simp2rr 1240

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  tfrlem5  7999  omeu  8194  gruina  10229  4sqlem18  16288  vdwlem10  16316  mdetuni0  21226  mdetmul  21228  tsmsxp  22760  ax5seglem3  26725  fpr3g  33235  btwnconn1lem1  33661  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem5  33665  btwnconn1lem6  33666  btwnconn1lem7  33667  btwnconn1lem12  33672  linethru  33727  2llnjN  36863  2lplnja  36915  2lplnj  36916  cdlemblem  37089  dalaw  37182  pclfinN  37196  lhpmcvr4N  37322  cdlemb2  37337  cdleme01N  37517  cdleme0ex2N  37520  cdleme7c  37541  cdlemefrs29bpre0  37692  cdlemefrs29cpre1  37694  cdlemefrs32fva1  37697  cdlemefs32sn1aw  37710  cdleme41sn3a  37729  cdleme48fv  37795  cdlemk21-2N  38187  dihmeetlem13N  38615  pellex  39776  lmhmfgsplit  40030  iunrelexpmin1  40409