![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > idd | Unicode version |
Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.) |
Ref | Expression |
---|---|
idd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: imim1d 69 ancld 308 ancrd 309 anim12d 318 anim1d 319 anim2d 320 orel2 645 pm2.621 666 orim1d 701 orim2d 702 pm2.63 713 pm2.74 720 simprimdc 756 oplem1 882 equsex 1616 equsexd 1617 r19.36av 2461 r19.44av 2469 r19.45av 2470 eqsbc3r 2819 reuss 3218 opthpr 3543 relop 4486 swoord2 6136 indpi 6440 lelttr 7106 elnnz 8255 ztri3or0 8287 xrlelttr 8722 icossicc 8829 iocssicc 8830 ioossico 8831 bj-exlimmp 9909 |
Copyright terms: Public domain | W3C validator |