Theorem simp2rr 1256

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

Assertion

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

Proof of Theorem simp2rr

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

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

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  fpr3g  8261  tfrlem5  8345  omeu  8549  gruina  10773  4sqlem18  16981  vdwlem10  17009  mdetuni0  22661  mdetmul  22663  tsmsxp  24195  ax5seglem3  29078  btwnconn1lem1  36401  btwnconn1lem3  36403  btwnconn1lem4  36404  btwnconn1lem5  36405  btwnconn1lem6  36406  btwnconn1lem7  36407  btwnconn1lem12  36412  linethru  36467  2llnjN  40155  2lplnja  40207  2lplnj  40208  cdlemblem  40381  dalaw  40474  pclfinN  40488  lhpmcvr4N  40614  cdlemb2  40629  cdleme01N  40809  cdleme0ex2N  40812  cdleme7c  40833  cdlemefrs29bpre0  40984  cdlemefrs29cpre1  40986  cdlemefrs32fva1  40989  cdlemefs32sn1aw  41002  cdleme41sn3a  41021  cdleme48fv  41087  cdlemk21-2N  41479  dihmeetlem13N  41907  pellex  43376  lmhmfgsplit  43627  iunrelexpmin1  44248