![]() |
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 1133 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 1, 3 | sylbi 216 | 1 ⊢ (𝜂 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: bnj1219 33706 bnj1379 33736 bnj1175 33910 bnj1286 33925 bnj1280 33926 bnj1296 33927 bnj1398 33940 bnj1415 33944 bnj1417 33947 bnj1421 33948 bnj1442 33955 bnj1450 33956 bnj1452 33958 bnj1489 33962 bnj1312 33964 bnj1501 33973 bnj1523 33977 |
Copyright terms: Public domain | W3C validator |