![]() |
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 206 ⊥wfal 1549 |
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 207 |
This theorem is referenced by: mdandyv0 46798 mdandyv1 46799 mdandyv2 46800 mdandyv3 46801 mdandyv4 46802 mdandyv5 46803 mdandyv6 46804 mdandyv7 46805 mdandyv8 46806 mdandyv9 46807 mdandyv10 46808 mdandyv11 46809 mdandyv12 46810 mdandyv13 46811 mdandyv14 46812 dandysum2p2e4 46847 |
Copyright terms: Public domain | W3C validator |