![]() |
Mathbox for Jarvin Udandy |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bothfbothsame | 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 |
---|---|
bothfbothsame.1 | ⊢ (𝜑 ↔ ⊥) |
bothfbothsame.2 | ⊢ (𝜓 ↔ ⊥) |
Ref | Expression |
---|---|
bothfbothsame | ⊢ (𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bothfbothsame.1 | . 2 ⊢ (𝜑 ↔ ⊥) | |
2 | bothfbothsame.2 | . 2 ⊢ (𝜓 ↔ ⊥) | |
3 | 1, 2 | bitr4i 278 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ⊥wfal 1554 |
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: mdandyv0 45258 mdandyv1 45259 mdandyv2 45260 mdandyv3 45261 mdandyv4 45262 mdandyv5 45263 mdandyv6 45264 mdandyv7 45265 mdandyv8 45266 mdandyv9 45267 mdandyv10 45268 mdandyv11 45269 mdandyv12 45270 mdandyv13 45271 mdandyv14 45272 dandysum2p2e4 45307 |
Copyright terms: Public domain | W3C validator |