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  8288  tfrlem5  8372  omeu  8576  gruina  10831  4sqlem18  17060  vdwlem10  17088  mdetuni0  22849  mdetmul  22851  tsmsxp  24387  ax5seglem3  29396  btwnconn1lem1  36675  btwnconn1lem3  36677  btwnconn1lem4  36678  btwnconn1lem5  36679  btwnconn1lem6  36680  btwnconn1lem7  36681  btwnconn1lem12  36686  linethru  36741  2llnjN  40448  2lplnja  40500  2lplnj  40501  cdlemblem  40674  dalaw  40767  pclfinN  40781  lhpmcvr4N  40907  cdlemb2  40922  cdleme01N  41102  cdleme0ex2N  41105  cdleme7c  41126  cdlemefrs29bpre0  41277  cdlemefrs29cpre1  41279  cdlemefrs32fva1  41282  cdlemefs32sn1aw  41295  cdleme41sn3a  41314  cdleme48fv  41380  cdlemk21-2N  41772  dihmeetlem13N  42200  pellex  43684  lmhmfgsplit  43935  iunrelexpmin1  44556