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 279 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ⊥wfal 1540 |
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 208 |
This theorem is referenced by: mdandyv0 43062 mdandyv1 43063 mdandyv2 43064 mdandyv3 43065 mdandyv4 43066 mdandyv5 43067 mdandyv6 43068 mdandyv7 43069 mdandyv8 43070 mdandyv9 43071 mdandyv10 43072 mdandyv11 43073 mdandyv12 43074 mdandyv13 43075 mdandyv14 43076 dandysum2p2e4 43111 |
Copyright terms: Public domain | W3C validator |