Theorem simp2lr 1239

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  fpr3g  8072  tfrlem5  8182  omeu  8378  expmordi  13813  4sqlem18  16591  vdwlem10  16619  mvrf1  21104  mdetuni0  21678  mdetmul  21680  tsmsxp  23214  ax5seglem3  27202  btwnconn1lem1  34316  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem5  34320  btwnconn1lem6  34321  btwnconn1lem7  34322  linethru  34382  lshpkrlem6  37056  athgt  37397  2llnjN  37508  dalaw  37827  cdlemb2  37982  4atexlemex6  38015  cdleme01N  38162  cdleme0ex2N  38165  cdleme7aa  38183  cdleme7e  38188  cdlemg33c0  38643  dihmeetlem3N  39246  pellex  40573