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  8284  tfrlem5  8394  omeu  8597  gruina  10832  4sqlem18  16982  vdwlem10  17010  mdetuni0  22559  mdetmul  22561  tsmsxp  24093  ax5seglem3  28910  btwnconn1lem1  36105  btwnconn1lem3  36107  btwnconn1lem4  36108  btwnconn1lem5  36109  btwnconn1lem6  36110  btwnconn1lem7  36111  btwnconn1lem12  36116  linethru  36171  2llnjN  39586  2lplnja  39638  2lplnj  39639  cdlemblem  39812  dalaw  39905  pclfinN  39919  lhpmcvr4N  40045  cdlemb2  40060  cdleme01N  40240  cdleme0ex2N  40243  cdleme7c  40264  cdlemefrs29bpre0  40415  cdlemefrs29cpre1  40417  cdlemefrs32fva1  40420  cdlemefs32sn1aw  40433  cdleme41sn3a  40452  cdleme48fv  40518  cdlemk21-2N  40910  dihmeetlem13N  41338  pellex  42858  lmhmfgsplit  43110  iunrelexpmin1  43732