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 768	. 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  8284  tfrlem5  8394  omeu  8599  expmordi  14155  4sqlem18  16922  vdwlem10  16950  mvrf1  21915  mdetuni0  22510  mdetmul  22512  tsmsxp  24046  ax5seglem3  28729  btwnconn1lem1  35619  btwnconn1lem3  35621  btwnconn1lem4  35622  btwnconn1lem5  35623  btwnconn1lem6  35624  btwnconn1lem7  35625  linethru  35685  lshpkrlem6  38524  athgt  38866  2llnjN  38977  dalaw  39296  cdlemb2  39451  4atexlemex6  39484  cdleme01N  39631  cdleme0ex2N  39634  cdleme7aa  39652  cdleme7e  39657  cdlemg33c0  40112  dihmeetlem3N  40715  pellex  42177