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 277 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ⊥wfal 1551 |
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 44444 mdandyv1 44445 mdandyv2 44446 mdandyv3 44447 mdandyv4 44448 mdandyv5 44449 mdandyv6 44450 mdandyv7 44451 mdandyv8 44452 mdandyv9 44453 mdandyv10 44454 mdandyv11 44455 mdandyv12 44456 mdandyv13 44457 mdandyv14 44458 dandysum2p2e4 44493 |
Copyright terms: Public domain | W3C validator |