Theorem simp2lr 1240

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

Assertion

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

Proof of Theorem simp2lr

Step	Hyp	Ref	Expression
1		simplr 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant2 1133	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)

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

This theorem is referenced by:  fpr3g  8101  tfrlem5  8211  omeu  8416  expmordi  13885  4sqlem18  16663  vdwlem10  16691  mvrf1  21194  mdetuni0  21770  mdetmul  21772  tsmsxp  23306  ax5seglem3  27299  btwnconn1lem1  34389  btwnconn1lem3  34391  btwnconn1lem4  34392  btwnconn1lem5  34393  btwnconn1lem6  34394  btwnconn1lem7  34395  linethru  34455  lshpkrlem6  37129  athgt  37470  2llnjN  37581  dalaw  37900  cdlemb2  38055  4atexlemex6  38088  cdleme01N  38235  cdleme0ex2N  38238  cdleme7aa  38256  cdleme7e  38261  cdlemg33c0  38716  dihmeetlem3N  39319  pellex  40657