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  8010  omeu  8205  expmordi  13525  4sqlem18  16292  vdwlem10  16320  mvrf1  20199  mdetuni0  21224  mdetmul  21226  tsmsxp  22757  ax5seglem3  26711  fpr3g  33117  btwnconn1lem1  33543  btwnconn1lem3  33545  btwnconn1lem4  33546  btwnconn1lem5  33547  btwnconn1lem6  33548  btwnconn1lem7  33549  linethru  33609  lshpkrlem6  36245  athgt  36586  2llnjN  36697  dalaw  37016  cdlemb2  37171  4atexlemex6  37204  cdleme01N  37351  cdleme0ex2N  37354  cdleme7aa  37372  cdleme7e  37377  cdlemg33c0  37832  dihmeetlem3N  38435  pellex  39425