| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp132 | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp132 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp32 1212 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓) | |
| 2 | 1 | 3ad2ant1 1134 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: ax5seglem3 29016 3atlem1 39856 3atlem2 39857 3atlem5 39860 2llnjaN 39939 4atlem11b 39981 4atlem12b 39984 lplncvrlvol2 39988 dalemtea 40003 dath2 40110 cdlemblem 40166 dalawlem1 40244 lhpexle3lem 40384 4atexlemex6 40447 cdleme22f2 40720 cdleme22g 40721 cdlemg7aN 40998 cdlemg34 41085 cdlemj1 41194 cdlemk23-3 41275 cdlemk25-3 41277 cdlemk26b-3 41278 |
| Copyright terms: Public domain | W3C validator |