![]() |
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 644 pm2.621 665 orim1d 700 orim2d 701 pm2.63 712 pm2.74 719 simprimdc 755 oplem1 881 equsex 1613 equsexd 1614 r19.36av 2455 r19.44av 2463 r19.45av 2464 eqsbc3r 2813 reuss 3212 opthpr 3534 relop 4429 swoord2 6072 indpi 6326 lelttr 6903 elnnz 8031 ztri3or0 8063 xrlelttr 8492 icossicc 8599 iocssicc 8600 ioossico 8601 bj-exlimmp 9244 |
Copyright terms: Public domain | W3C validator |