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  8077  tfrlem5  8187  omeu  8383  expmordi  13829  4sqlem18  16607  vdwlem10  16635  mvrf1  21138  mdetuni0  21714  mdetmul  21716  tsmsxp  23250  ax5seglem3  27242  btwnconn1lem1  34358  btwnconn1lem3  34360  btwnconn1lem4  34361  btwnconn1lem5  34362  btwnconn1lem6  34363  btwnconn1lem7  34364  linethru  34424  lshpkrlem6  37098  athgt  37439  2llnjN  37550  dalaw  37869  cdlemb2  38024  4atexlemex6  38057  cdleme01N  38204  cdleme0ex2N  38207  cdleme7aa  38225  cdleme7e  38230  cdlemg33c0  38685  dihmeetlem3N  39288  pellex  40615