![]() |
brismu bridi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > Home > Th. List > cur-swap12 |
Description: cur 59 with swapped antecedents. (Contributed by la korvo, 8-Jul-2025.) |
Ref | Expression |
---|---|
cur-swap12.0 | ⊢ ganai broda gi ganai brode gi brodi |
Ref | Expression |
---|---|
cur-swap12 | ⊢ ganai ge brode gi broda gi brodi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cur-swap12.0 | . . 3 ⊢ ganai broda gi ganai brode gi brodi | |
2 | 1 | ganai-swap12 29 | . 2 ⊢ ganai brode gi ganai broda gi brodi |
3 | 2 | cur 59 | 1 ⊢ ganai ge brode gi broda gi brodi |
Colors of variables: sumti selbri bridi |
This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-ge-le 48 ax-ge-re 49 |
This theorem is referenced by: mpan9 76 foml19.41 432 |
Copyright terms: Public domain | W3C validator |