![]() |
Mathbox for Jarvin Udandy |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bothtbothsame | Structured version Visualization version GIF version |
Description: Given both a, b are equivalent to ⊤, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
Ref | Expression |
---|---|
bothtbothsame.1 | ⊢ (𝜑 ↔ ⊤) |
bothtbothsame.2 | ⊢ (𝜓 ↔ ⊤) |
Ref | Expression |
---|---|
bothtbothsame | ⊢ (𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bothtbothsame.1 | . 2 ⊢ (𝜑 ↔ ⊤) | |
2 | bothtbothsame.2 | . 2 ⊢ (𝜓 ↔ ⊤) | |
3 | 1, 2 | bitr4i 278 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ⊤wtru 1535 |
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 |
This theorem is referenced by: mdandyv1 46255 mdandyv2 46256 mdandyv3 46257 mdandyv4 46258 mdandyv5 46259 mdandyv6 46260 mdandyv7 46261 mdandyv8 46262 mdandyv9 46263 mdandyv10 46264 mdandyv11 46265 mdandyv12 46266 mdandyv13 46267 mdandyv14 46268 mdandyv15 46269 dandysum2p2e4 46303 |
Copyright terms: Public domain | W3C validator |