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  8267  tfrlem5  8351  omeu  8552  gruina  10778  4sqlem18  16940  vdwlem10  16968  mdetuni0  22515  mdetmul  22517  tsmsxp  24049  ax5seglem3  28865  btwnconn1lem1  36082  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem7  36088  btwnconn1lem12  36093  linethru  36148  2llnjN  39568  2lplnja  39620  2lplnj  39621  cdlemblem  39794  dalaw  39887  pclfinN  39901  lhpmcvr4N  40027  cdlemb2  40042  cdleme01N  40222  cdleme0ex2N  40225  cdleme7c  40246  cdlemefrs29bpre0  40397  cdlemefrs29cpre1  40399  cdlemefrs32fva1  40402  cdlemefs32sn1aw  40415  cdleme41sn3a  40434  cdleme48fv  40500  cdlemk21-2N  40892  dihmeetlem13N  41320  pellex  42830  lmhmfgsplit  43082  iunrelexpmin1  43704