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 772	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1135	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  fpr3g  8270  tfrlem5  8380  omeu  8585  gruina  10813  4sqlem18  16895  vdwlem10  16923  mdetuni0  22123  mdetmul  22125  tsmsxp  23659  ax5seglem3  28189  btwnconn1lem1  35059  btwnconn1lem3  35061  btwnconn1lem4  35062  btwnconn1lem5  35063  btwnconn1lem6  35064  btwnconn1lem7  35065  btwnconn1lem12  35070  linethru  35125  2llnjN  38438  2lplnja  38490  2lplnj  38491  cdlemblem  38664  dalaw  38757  pclfinN  38771  lhpmcvr4N  38897  cdlemb2  38912  cdleme01N  39092  cdleme0ex2N  39095  cdleme7c  39116  cdlemefrs29bpre0  39267  cdlemefrs29cpre1  39269  cdlemefrs32fva1  39272  cdlemefs32sn1aw  39285  cdleme41sn3a  39304  cdleme48fv  39370  cdlemk21-2N  39762  dihmeetlem13N  40190  pellex  41573  lmhmfgsplit  41828  iunrelexpmin1  42459