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: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3anbi12d 1302 3anbi13d 1303 3anbi23d 1304 3anbi1d 1305 3anbi2d 1306 3anbi3d 1307 sb6x 1766 exdistrfor 1787 a16g 1851 rr19.3v 2860 rr19.28v 2861 euxfr2dc 2906 dfif3 3528 undifexmid 4166 exmidexmid 4169 exmidsssnc 4176 copsexg 4216 ordtriexmidlem2 4491 ordtriexmid 4492 ontriexmidim 4493 ordtri2orexmid 4494 ontr2exmid 4496 ordtri2or2exmidlem 4497 onsucsssucexmid 4498 ordsoexmid 4533 0elsucexmid 4536 ordpwsucexmid 4541 ordtri2or2exmid 4542 ontri2orexmidim 4543 dcextest 4552 riotabidv 5794 ov6g 5970 ovg 5971 dfxp3 6154 ssfilem 6832 diffitest 6844 inffiexmid 6863 unfiexmid 6874 snexxph 6906 ctssexmid 7105 exmidonfinlem 7140 ltsopi 7252 pitri3or 7254 creur 8845 creui 8846 pceu 12206 2irrexpqap 13443 subctctexmid 13722 |
Copyright terms: Public domain | W3C validator |