Theorem simp2rr 1245

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

Assertion

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

Proof of Theorem simp2rr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  fpr3g  8235  tfrlem5  8319  omeu  8520  gruina  10741  4sqlem18  16933  vdwlem10  16961  mdetuni0  22586  mdetmul  22588  tsmsxp  24120  ax5seglem3  29000  btwnconn1lem1  36269  btwnconn1lem3  36271  btwnconn1lem4  36272  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem7  36275  btwnconn1lem12  36280  linethru  36335  2llnjN  40013  2lplnja  40065  2lplnj  40066  cdlemblem  40239  dalaw  40332  pclfinN  40346  lhpmcvr4N  40472  cdlemb2  40487  cdleme01N  40667  cdleme0ex2N  40670  cdleme7c  40691  cdlemefrs29bpre0  40842  cdlemefrs29cpre1  40844  cdlemefrs32fva1  40847  cdlemefs32sn1aw  40860  cdleme41sn3a  40879  cdleme48fv  40945  cdlemk21-2N  41337  dihmeetlem13N  41765  pellex  43263  lmhmfgsplit  43514  iunrelexpmin1  44135