Theorem simp2rr 1262

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

Assertion

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

Proof of Theorem simp2rr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fpr3g  8291  tfrlem5  8375  omeu  8579  gruina  10821  4sqlem18  17047  vdwlem10  17075  mdetuni0  22815  mdetmul  22817  tsmsxp  24349  ax5seglem3  29318  btwnconn1lem1  36600  btwnconn1lem3  36602  btwnconn1lem4  36603  btwnconn1lem5  36604  btwnconn1lem6  36605  btwnconn1lem7  36606  btwnconn1lem12  36611  linethru  36666  2llnjN  40382  2lplnja  40434  2lplnj  40435  cdlemblem  40608  dalaw  40701  pclfinN  40715  lhpmcvr4N  40841  cdlemb2  40856  cdleme01N  41036  cdleme0ex2N  41039  cdleme7c  41060  cdlemefrs29bpre0  41211  cdlemefrs29cpre1  41213  cdlemefrs32fva1  41216  cdlemefs32sn1aw  41229  cdleme41sn3a  41248  cdleme48fv  41314  cdlemk21-2N  41706  dihmeetlem13N  42134  pellex  43603  lmhmfgsplit  43854  iunrelexpmin1  44475