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 1129 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 1, 3 | sylbi 219 | 1 ⊢ (𝜂 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: bnj1219 32067 bnj1379 32097 bnj1175 32271 bnj1286 32286 bnj1280 32287 bnj1296 32288 bnj1398 32301 bnj1415 32305 bnj1417 32308 bnj1421 32309 bnj1442 32316 bnj1450 32317 bnj1452 32319 bnj1489 32323 bnj1312 32325 bnj1501 32334 bnj1523 32338 |
Copyright terms: Public domain | W3C validator |