The Logic Resource Center

The Logic Resource Center

Public Alpha

The Logic Resource Center

Public Alpha

© 2025 The Logic Resource Center, LLC

Identity Elimination

Identity Elimination allows you to substitute in accord with an indentity in things you have already derived.

Constants: =
Systems: LRC_F OLI The Logic Book LRC LRC_P LRC_O

Start a Problem →

Identity Elimination

i.

ϕ

ii.

=τ1τ2

⋮

iii.

ϕ[τ1//τ2]

=E: i, ii

Forward

Select an available formula
Select an available identity
Specify a substitution instance when prompted
Click "Apply"

Backward

Select a goal
Enter your chosen identity when prompted
Specify a substitution instance after entering your identity
Click "Apply"

Forward Adding Identity as Goal

Select an available formula
Select a goal substitution instancce
Click "Apply"

Preview shown for the Point And Click derivation type in the LRC_P system