Theorem simp2lr 1241

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  8292  tfrlem5  8402  omeu  8605  expmordi  14189  4sqlem18  16982  vdwlem10  17010  mvrf1  21960  mdetuni0  22575  mdetmul  22577  tsmsxp  24109  ax5seglem3  28876  btwnconn1lem1  36047  btwnconn1lem3  36049  btwnconn1lem4  36050  btwnconn1lem5  36051  btwnconn1lem6  36052  btwnconn1lem7  36053  linethru  36113  lshpkrlem6  39075  athgt  39417  2llnjN  39528  dalaw  39847  cdlemb2  40002  4atexlemex6  40035  cdleme01N  40182  cdleme0ex2N  40185  cdleme7aa  40203  cdleme7e  40208  cdlemg33c0  40663  dihmeetlem3N  41266  pellex  42809