Theorem simp2rr 1240

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 1131	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  fpr3g  8289  tfrlem5  8399  omeu  8604  gruina  10841  4sqlem18  16930  vdwlem10  16958  mdetuni0  22553  mdetmul  22555  tsmsxp  24089  ax5seglem3  28798  btwnconn1lem1  35753  btwnconn1lem3  35755  btwnconn1lem4  35756  btwnconn1lem5  35757  btwnconn1lem6  35758  btwnconn1lem7  35759  btwnconn1lem12  35764  linethru  35819  2llnjN  39109  2lplnja  39161  2lplnj  39162  cdlemblem  39335  dalaw  39428  pclfinN  39442  lhpmcvr4N  39568  cdlemb2  39583  cdleme01N  39763  cdleme0ex2N  39766  cdleme7c  39787  cdlemefrs29bpre0  39938  cdlemefrs29cpre1  39940  cdlemefrs32fva1  39943  cdlemefs32sn1aw  39956  cdleme41sn3a  39975  cdleme48fv  40041  cdlemk21-2N  40433  dihmeetlem13N  40861  pellex  42320  lmhmfgsplit  42575  iunrelexpmin1  43203