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  8215  tfrlem5  8299  omeu  8500  gruina  10706  4sqlem18  16871  vdwlem10  16899  mdetuni0  22534  mdetmul  22536  tsmsxp  24068  ax5seglem3  28907  btwnconn1lem1  36120  btwnconn1lem3  36122  btwnconn1lem4  36123  btwnconn1lem5  36124  btwnconn1lem6  36125  btwnconn1lem7  36126  btwnconn1lem12  36131  linethru  36186  2llnjN  39605  2lplnja  39657  2lplnj  39658  cdlemblem  39831  dalaw  39924  pclfinN  39938  lhpmcvr4N  40064  cdlemb2  40079  cdleme01N  40259  cdleme0ex2N  40262  cdleme7c  40283  cdlemefrs29bpre0  40434  cdlemefrs29cpre1  40436  cdlemefrs32fva1  40439  cdlemefs32sn1aw  40452  cdleme41sn3a  40471  cdleme48fv  40537  cdlemk21-2N  40929  dihmeetlem13N  41357  pellex  42867  lmhmfgsplit  43118  iunrelexpmin1  43740