Mathbox for Jarvin Udandy |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bothfbothsame | Structured version Visualization version Unicode 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 267 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wfal 1488 |
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 197 |
This theorem is referenced by: mdandyv0 41116 mdandyv1 41117 mdandyv2 41118 mdandyv3 41119 mdandyv4 41120 mdandyv5 41121 mdandyv6 41122 mdandyv7 41123 mdandyv8 41124 mdandyv9 41125 mdandyv10 41126 mdandyv11 41127 mdandyv12 41128 mdandyv13 41129 mdandyv14 41130 dandysum2p2e4 41165 |
Copyright terms: Public domain | W3C validator |