![]() |
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 1113 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 1, 3 | sylbi 209 | 1 ⊢ (𝜂 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: bnj1219 31720 bnj1379 31750 bnj1175 31921 bnj1286 31936 bnj1280 31937 bnj1296 31938 bnj1398 31951 bnj1415 31955 bnj1417 31958 bnj1421 31959 bnj1442 31966 bnj1450 31967 bnj1452 31969 bnj1489 31973 bnj1312 31975 bnj1501 31984 bnj1523 31988 |
Copyright terms: Public domain | W3C validator |