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  8225  tfrlem5  8309  omeu  8510  gruina  10731  4sqlem18  16892  vdwlem10  16920  mdetuni0  22524  mdetmul  22526  tsmsxp  24058  ax5seglem3  28894  btwnconn1lem1  36060  btwnconn1lem3  36062  btwnconn1lem4  36063  btwnconn1lem5  36064  btwnconn1lem6  36065  btwnconn1lem7  36066  btwnconn1lem12  36071  linethru  36126  2llnjN  39546  2lplnja  39598  2lplnj  39599  cdlemblem  39772  dalaw  39865  pclfinN  39879  lhpmcvr4N  40005  cdlemb2  40020  cdleme01N  40200  cdleme0ex2N  40203  cdleme7c  40224  cdlemefrs29bpre0  40375  cdlemefrs29cpre1  40377  cdlemefrs32fva1  40380  cdlemefs32sn1aw  40393  cdleme41sn3a  40412  cdleme48fv  40478  cdlemk21-2N  40870  dihmeetlem13N  41298  pellex  42808  lmhmfgsplit  43059  iunrelexpmin1  43681