![]() |
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 170 |
. 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 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3anbi12d 1274 3anbi13d 1275 3anbi23d 1276 3anbi1d 1277 3anbi2d 1278 3anbi3d 1279 sb6x 1735 exdistrfor 1754 a16g 1818 rr19.3v 2793 rr19.28v 2794 euxfr2dc 2838 dfif3 3453 undifexmid 4077 exmidexmid 4080 exmidsssnc 4086 copsexg 4126 ordtriexmidlem2 4396 ordtriexmid 4397 ordtri2orexmid 4398 ontr2exmid 4400 ordtri2or2exmidlem 4401 onsucsssucexmid 4402 ordsoexmid 4437 0elsucexmid 4440 ordpwsucexmid 4445 ordtri2or2exmid 4446 dcextest 4455 riotabidv 5686 ov6g 5862 ovg 5863 dfxp3 6046 ssfilem 6722 diffitest 6734 inffiexmid 6753 unfiexmid 6759 snexxph 6790 ctssexmid 6974 ltsopi 7076 pitri3or 7078 creur 8627 creui 8628 subctctexmid 12888 |
Copyright terms: Public domain | W3C validator |