![]() |
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-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: imim1d 75 ancld 325 ancrd 326 anim12d 335 anim1d 336 anim2d 337 orel2 726 pm2.621 747 orim1d 787 orim2d 788 pm2.63 800 pm2.74 807 simprimdc 859 oplem1 975 equsex 1728 equsexd 1729 r19.36av 2628 r19.44av 2636 r19.45av 2637 reuss 3416 opthpr 3772 relop 4777 swoord2 6564 indpi 7340 lelttr 8044 elnnz 9261 ztri3or0 9293 xrlelttr 9804 icossicc 9958 iocssicc 9959 ioossico 9960 lmconst 13609 cnptopresti 13631 sslm 13640 bj-exlimmp 14403 |
Copyright terms: Public domain | W3C validator |