Theorem simp2lr 1242

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 1134	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)

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

This theorem is referenced by:  fpr3g  8221  tfrlem5  8305  omeu  8506  expmordi  14076  4sqlem18  16876  vdwlem10  16904  mvrf1  21924  mdetuni0  22537  mdetmul  22539  tsmsxp  24071  ax5seglem3  28911  btwnconn1lem1  36152  btwnconn1lem3  36154  btwnconn1lem4  36155  btwnconn1lem5  36156  btwnconn1lem6  36157  btwnconn1lem7  36158  linethru  36218  lshpkrlem6  39234  athgt  39575  2llnjN  39686  dalaw  40005  cdlemb2  40160  4atexlemex6  40193  cdleme01N  40340  cdleme0ex2N  40343  cdleme7aa  40361  cdleme7e  40366  cdlemg33c0  40821  dihmeetlem3N  41424  pellex  42952