![]() |
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 1541 |
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 45971 mdandyv2 45972 mdandyv3 45973 mdandyv4 45974 mdandyv5 45975 mdandyv6 45976 mdandyv7 45977 mdandyv8 45978 mdandyv9 45979 mdandyv10 45980 mdandyv11 45981 mdandyv12 45982 mdandyv13 45983 mdandyv14 45984 mdandyv15 45985 dandysum2p2e4 46019 |
Copyright terms: Public domain | W3C validator |