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: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: imim1d 75 ancld 323 ancrd 324 anim12d 333 anim1d 334 anim2d 335 orel2 715 pm2.621 736 orim1d 776 orim2d 777 pm2.63 789 pm2.74 796 simprimdc 844 oplem1 959 equsex 1706 equsexd 1707 r19.36av 2580 r19.44av 2588 r19.45av 2589 reuss 3352 opthpr 3694 relop 4684 swoord2 6452 indpi 7143 lelttr 7845 elnnz 9057 ztri3or0 9089 xrlelttr 9582 icossicc 9736 iocssicc 9737 ioossico 9738 lmconst 12374 cnptopresti 12396 sslm 12405 bj-exlimmp 12965 |
Copyright terms: Public domain | W3C validator |