brismu bridi |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > Home > Th. List > nfri |
Description: Inference form of nfr 360 (Contributed by la korvo, 25-Jun-2024.) |
Ref | Expression |
---|---|
nfri.0 | ⊢ na'a'u da zo'u broda |
Ref | Expression |
---|---|
nfri | ⊢ ganai broda gi ro da zo'u broda |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfri.0 | . 2 ⊢ na'a'u da zo'u broda | |
2 | nfr 360 | . 2 ⊢ ganai na'a'u da zo'u broda gi ganai broda gi ro da zo'u broda | |
3 | 1, 2 | ax-mp 10 | 1 ⊢ ganai broda gi ro da zo'u broda |
Colors of variables: sumti selbri bridi |
Syntax hints: ganai bgan 9 ro brd 177 na'a'u bnd 356 |
This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 14 ax-ge-le 34 ax-spec1 181 |
This theorem depends on definitions: df-go 52 df-nahahu 357 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |