| Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj835 | Structured version Visualization version GIF version | ||
| Description: ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| bnj835.1 | ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) |
| bnj835.2 | ⊢ (𝜑 → 𝜏) |
| Ref | Expression |
|---|---|
| bnj835 | ⊢ (𝜂 → 𝜏) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bnj835.1 | . 2 ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | |
| 2 | bnj835.2 | . . 3 ⊢ (𝜑 → 𝜏) | |
| 3 | 2 | 3ad2ant1 1134 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
| 4 | 1, 3 | sylbi 217 | 1 ⊢ (𝜂 → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ 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: bnj1219 34814 bnj1379 34844 bnj1175 35018 bnj1286 35033 bnj1280 35034 bnj1296 35035 bnj1398 35048 bnj1415 35052 bnj1417 35055 bnj1421 35056 bnj1442 35063 bnj1450 35064 bnj1452 35066 bnj1489 35070 bnj1312 35072 bnj1501 35081 bnj1523 35085 |
| Copyright terms: Public domain | W3C validator |