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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  fpr3g  8227  tfrlem5  8311  omeu  8512  gruina  10729  4sqlem18  16890  vdwlem10  16918  mdetuni0  22565  mdetmul  22567  tsmsxp  24099  ax5seglem3  29004  btwnconn1lem1  36281  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem7  36287  btwnconn1lem12  36292  linethru  36347  2llnjN  39823  2lplnja  39875  2lplnj  39876  cdlemblem  40049  dalaw  40142  pclfinN  40156  lhpmcvr4N  40282  cdlemb2  40297  cdleme01N  40477  cdleme0ex2N  40480  cdleme7c  40501  cdlemefrs29bpre0  40652  cdlemefrs29cpre1  40654  cdlemefrs32fva1  40657  cdlemefs32sn1aw  40670  cdleme41sn3a  40689  cdleme48fv  40755  cdlemk21-2N  41147  dihmeetlem13N  41575  pellex  43073  lmhmfgsplit  43324  iunrelexpmin1  43945