Theorem simp2lr 1237

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  tfrlem5  8018  omeu  8213  expmordi  13534  4sqlem18  16300  vdwlem10  16328  mvrf1  20207  mdetuni0  21232  mdetmul  21234  tsmsxp  22765  ax5seglem3  26719  fpr3g  33124  btwnconn1lem1  33550  btwnconn1lem3  33552  btwnconn1lem4  33553  btwnconn1lem5  33554  btwnconn1lem6  33555  btwnconn1lem7  33556  linethru  33616  lshpkrlem6  36253  athgt  36594  2llnjN  36705  dalaw  37024  cdlemb2  37179  4atexlemex6  37212  cdleme01N  37359  cdleme0ex2N  37362  cdleme7aa  37380  cdleme7e  37385  cdlemg33c0  37840  dihmeetlem3N  38443  pellex  39439