Theorem simp2rr 1245

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

Assertion

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

Proof of Theorem simp2rr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  fpr3g  8228  tfrlem5  8312  omeu  8513  gruina  10732  4sqlem18  16924  vdwlem10  16952  mdetuni0  22596  mdetmul  22598  tsmsxp  24130  ax5seglem3  29014  btwnconn1lem1  36285  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem5  36289  btwnconn1lem6  36290  btwnconn1lem7  36291  btwnconn1lem12  36296  linethru  36351  2llnjN  40027  2lplnja  40079  2lplnj  40080  cdlemblem  40253  dalaw  40346  pclfinN  40360  lhpmcvr4N  40486  cdlemb2  40501  cdleme01N  40681  cdleme0ex2N  40684  cdleme7c  40705  cdlemefrs29bpre0  40856  cdlemefrs29cpre1  40858  cdlemefrs32fva1  40861  cdlemefs32sn1aw  40874  cdleme41sn3a  40893  cdleme48fv  40959  cdlemk21-2N  41351  dihmeetlem13N  41779  pellex  43281  lmhmfgsplit  43532  iunrelexpmin1  44153