|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simp332 | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) | 
| Ref | Expression | 
|---|---|
| simp332 | ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simp32 1210 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓) | |
| 2 | 1 | 3ad2ant3 1135 | 1 ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ 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: ivthALT 36337 dalemclqjt 39638 dath2 39740 cdlema1N 39794 cdleme26eALTN 40364 cdlemk7u 40873 cdlemk11u 40874 cdlemk12u 40875 cdlemk23-3 40905 cdlemk33N 40912 cdlemk11ta 40932 cdlemk11tc 40948 cdlemk54 40961 | 
| Copyright terms: Public domain | W3C validator |