Theorem simp2lr 1122

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  tfrlem5  7363  omeu  7552  4sqlem18  15504  vdwlem10  15532  mvrf1  19246  mdetuni0  20246  mdetmul  20248  tsmsxp  21768  ax5seglem3  25611  btwnconn1lem1  31364  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem7  31370  linethru  31430  lshpkrlem6  33420  athgt  33760  2llnjN  33871  dalaw  34190  cdlemb2  34345  4atexlemex6  34378  cdleme01N  34526  cdleme0ex2N  34529  cdleme7aa  34547  cdleme7e  34552  cdlemg33c0  35008  dihmeetlem3N  35612  pellex  36417  expmordi  36530