Theorem simp2rr 1131

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

Assertion

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

Proof of Theorem simp2rr

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  tfrlem5  7476  omeu  7665  gruina  9640  4sqlem18  15666  vdwlem10  15694  mdetuni0  20427  mdetmul  20429  tsmsxp  21958  ax5seglem3  25811  btwnconn1lem1  32194  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem7  32200  btwnconn1lem12  32205  linethru  32260  2llnjN  34853  2lplnja  34905  2lplnj  34906  cdlemblem  35079  dalaw  35172  pclfinN  35186  lhpmcvr4N  35312  cdlemb2  35327  cdleme01N  35508  cdleme0ex2N  35511  cdleme7c  35532  cdlemefrs29bpre0  35684  cdlemefrs29cpre1  35686  cdlemefrs32fva1  35689  cdlemefs32sn1aw  35702  cdleme41sn3a  35721  cdleme48fv  35787  cdlemk21-2N  36179  dihmeetlem13N  36608  pellex  37399  lmhmfgsplit  37656  iunrelexpmin1  38000