![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biidd | Unicode version |
Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.) |
Ref | Expression |
---|---|
biidd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid 171 |
. 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 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3anbi12d 1324 3anbi13d 1325 3anbi23d 1326 3anbi1d 1327 3anbi2d 1328 3anbi3d 1329 sb6x 1790 exdistrfor 1811 a16g 1875 rr19.3v 2891 rr19.28v 2892 euxfr2dc 2937 dfif3 3562 undifexmid 4211 exmidexmid 4214 exmidsssnc 4221 copsexg 4262 ordtriexmidlem2 4537 ordtriexmid 4538 ontriexmidim 4539 ordtri2orexmid 4540 ontr2exmid 4542 ordtri2or2exmidlem 4543 onsucsssucexmid 4544 ordsoexmid 4579 0elsucexmid 4582 ordpwsucexmid 4587 ordtri2or2exmid 4588 ontri2orexmidim 4589 dcextest 4598 riotabidv 5853 ov6g 6033 ovg 6034 dfxp3 6218 ssfilem 6902 diffitest 6914 inffiexmid 6933 unfiexmid 6945 snexxph 6978 ctssexmid 7177 exmidonfinlem 7221 ltsopi 7348 pitri3or 7350 creur 8945 creui 8946 pceu 12326 2irrexpqap 14848 subctctexmid 15204 |
Copyright terms: Public domain | W3C validator |