![]() |
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 1075 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 1, 3 | sylbi 206 | 1 ⊢ (𝜂 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ 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: bnj1219 30125 bnj1379 30155 bnj1175 30326 bnj1286 30341 bnj1280 30342 bnj1296 30343 bnj1398 30356 bnj1415 30360 bnj1417 30363 bnj1421 30364 bnj1442 30371 bnj1450 30372 bnj1452 30374 bnj1489 30378 bnj1312 30380 bnj1501 30389 bnj1523 30393 |
Copyright terms: Public domain | W3C validator |