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  8259  tfrlem5  8343  omeu  8547  gruina  10771  4sqlem18  16979  vdwlem10  17007  mdetuni0  22659  mdetmul  22661  tsmsxp  24193  ax5seglem3  29076  btwnconn1lem1  36390  btwnconn1lem3  36392  btwnconn1lem4  36393  btwnconn1lem5  36394  btwnconn1lem6  36395  btwnconn1lem7  36396  btwnconn1lem12  36401  linethru  36456  2llnjN  40144  2lplnja  40196  2lplnj  40197  cdlemblem  40370  dalaw  40463  pclfinN  40477  lhpmcvr4N  40603  cdlemb2  40618  cdleme01N  40798  cdleme0ex2N  40801  cdleme7c  40822  cdlemefrs29bpre0  40973  cdlemefrs29cpre1  40975  cdlemefrs32fva1  40978  cdlemefs32sn1aw  40991  cdleme41sn3a  41010  cdleme48fv  41076  cdlemk21-2N  41468  dihmeetlem13N  41896  pellex  43365  lmhmfgsplit  43616  iunrelexpmin1  44237