![]() |
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 75 ancld 321 ancrd 322 anim12d 331 anim1d 332 anim2d 333 orel2 698 pm2.621 719 orim1d 759 orim2d 760 pm2.63 772 pm2.74 779 simprimdc 825 oplem1 940 equsex 1687 equsexd 1688 r19.36av 2554 r19.44av 2562 r19.45av 2563 reuss 3321 opthpr 3663 relop 4647 swoord2 6411 indpi 7092 lelttr 7769 elnnz 8962 ztri3or0 8994 xrlelttr 9476 icossicc 9630 iocssicc 9631 ioossico 9632 lmconst 12221 cnptopresti 12243 sslm 12252 bj-exlimmp 12660 |
Copyright terms: Public domain | W3C validator |