| 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 39853 3atlem2 39854 3atlem5 39857 2llnjaN 39936 4atlem11b 39978 4atlem12b 39981 lplncvrlvol2 39985 dalemtea 40000 dath2 40107 cdlemblem 40163 dalawlem1 40241 lhpexle3lem 40381 4atexlemex6 40444 cdleme22f2 40717 cdleme22g 40718 cdlemg7aN 40995 cdlemg34 41082 cdlemj1 41191 cdlemk23-3 41272 cdlemk25-3 41274 cdlemk26b-3 41275 |
| Copyright terms: Public domain | W3C validator |