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 280 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ⊤wtru 1538 |
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 |
This theorem is referenced by: mdandyv1 43206 mdandyv2 43207 mdandyv3 43208 mdandyv4 43209 mdandyv5 43210 mdandyv6 43211 mdandyv7 43212 mdandyv8 43213 mdandyv9 43214 mdandyv10 43215 mdandyv11 43216 mdandyv12 43217 mdandyv13 43218 mdandyv14 43219 mdandyv15 43220 dandysum2p2e4 43254 |
Copyright terms: Public domain | W3C validator |