![]() |
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 169 |
. 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 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3anbi12d 1245 3anbi13d 1246 3anbi23d 1247 3anbi1d 1248 3anbi2d 1249 3anbi3d 1250 sb6x 1703 exdistrfor 1722 a16g 1786 rr19.3v 2734 rr19.28v 2735 euxfr2dc 2778 dfif3 3372 copsexg 4007 ordtriexmidlem2 4272 ordtriexmid 4273 ordtri2orexmid 4274 ontr2exmid 4276 ordtri2or2exmidlem 4277 onsucsssucexmid 4278 ordsoexmid 4313 0elsucexmid 4316 ordpwsucexmid 4321 ordtri2or2exmid 4322 riotabidv 5501 ov6g 5669 ovg 5670 dfxp3 5851 ssfilem 6410 diffitest 6421 unfiexmid 6438 ltsopi 6572 pitri3or 6574 creur 8103 creui 8104 |
Copyright terms: Public domain | W3C validator |