Theorem simp2rr 1243

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

Assertion

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

Proof of Theorem simp2rr

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  fpr3g  8132  tfrlem5  8242  omeu  8447  gruina  10620  4sqlem18  16708  vdwlem10  16736  mdetuni0  21815  mdetmul  21817  tsmsxp  23351  ax5seglem3  27344  btwnconn1lem1  34434  btwnconn1lem3  34436  btwnconn1lem4  34437  btwnconn1lem5  34438  btwnconn1lem6  34439  btwnconn1lem7  34440  btwnconn1lem12  34445  linethru  34500  2llnjN  37623  2lplnja  37675  2lplnj  37676  cdlemblem  37849  dalaw  37942  pclfinN  37956  lhpmcvr4N  38082  cdlemb2  38097  cdleme01N  38277  cdleme0ex2N  38280  cdleme7c  38301  cdlemefrs29bpre0  38452  cdlemefrs29cpre1  38454  cdlemefrs32fva1  38457  cdlemefs32sn1aw  38470  cdleme41sn3a  38489  cdleme48fv  38555  cdlemk21-2N  38947  dihmeetlem13N  39375  pellex  40694  lmhmfgsplit  40949  iunrelexpmin1  41354