![]() |
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 46864 mdandyv1 46865 mdandyv2 46866 mdandyv3 46867 mdandyv4 46868 mdandyv5 46869 mdandyv6 46870 mdandyv7 46871 mdandyv8 46872 mdandyv9 46873 mdandyv10 46874 mdandyv11 46875 mdandyv12 46876 mdandyv13 46877 mdandyv14 46878 dandysum2p2e4 46913 |
Copyright terms: Public domain | W3C validator |