![]() |
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 1132 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 1, 3 | sylbi 217 | 1 ⊢ (𝜂 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ 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: bnj1219 34793 bnj1379 34823 bnj1175 34997 bnj1286 35012 bnj1280 35013 bnj1296 35014 bnj1398 35027 bnj1415 35031 bnj1417 35034 bnj1421 35035 bnj1442 35042 bnj1450 35043 bnj1452 35045 bnj1489 35049 bnj1312 35051 bnj1501 35060 bnj1523 35064 |
Copyright terms: Public domain | W3C validator |