![]() |
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 74 ancld 318 ancrd 319 anim12d 328 anim1d 329 anim2d 330 orel2 680 pm2.621 701 orim1d 736 orim2d 737 pm2.63 749 pm2.74 756 simprimdc 794 oplem1 921 equsex 1663 equsexd 1664 r19.36av 2518 r19.44av 2526 r19.45av 2527 reuss 3280 opthpr 3616 relop 4586 swoord2 6322 indpi 6901 lelttr 7573 elnnz 8760 ztri3or0 8792 xrlelttr 9271 icossicc 9378 iocssicc 9379 ioossico 9380 bj-exlimmp 11670 |
Copyright terms: Public domain | W3C validator |