Theorem simp2lr 1238

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086

This theorem is referenced by:  tfrlem5  7999  omeu  8194  expmordi  13527  4sqlem18  16288  vdwlem10  16316  mvrf1  20663  mdetuni0  21226  mdetmul  21228  tsmsxp  22760  ax5seglem3  26725  fpr3g  33235  btwnconn1lem1  33661  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem5  33665  btwnconn1lem6  33666  btwnconn1lem7  33667  linethru  33727  lshpkrlem6  36411  athgt  36752  2llnjN  36863  dalaw  37182  cdlemb2  37337  4atexlemex6  37370  cdleme01N  37517  cdleme0ex2N  37520  cdleme7aa  37538  cdleme7e  37543  cdlemg33c0  37998  dihmeetlem3N  38601  pellex  39776