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  8221  tfrlem5  8305  omeu  8506  gruina  10716  4sqlem18  16876  vdwlem10  16904  mdetuni0  22537  mdetmul  22539  tsmsxp  24071  ax5seglem3  28911  btwnconn1lem1  36152  btwnconn1lem3  36154  btwnconn1lem4  36155  btwnconn1lem5  36156  btwnconn1lem6  36157  btwnconn1lem7  36158  btwnconn1lem12  36163  linethru  36218  2llnjN  39686  2lplnja  39738  2lplnj  39739  cdlemblem  39912  dalaw  40005  pclfinN  40019  lhpmcvr4N  40145  cdlemb2  40160  cdleme01N  40340  cdleme0ex2N  40343  cdleme7c  40364  cdlemefrs29bpre0  40515  cdlemefrs29cpre1  40517  cdlemefrs32fva1  40520  cdlemefs32sn1aw  40533  cdleme41sn3a  40552  cdleme48fv  40618  cdlemk21-2N  41010  dihmeetlem13N  41438  pellex  42952  lmhmfgsplit  43203  iunrelexpmin1  43825