Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biidd | GIF 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 1308 3anbi13d 1309 3anbi23d 1310 3anbi1d 1311 3anbi2d 1312 3anbi3d 1313 sb6x 1772 exdistrfor 1793 a16g 1857 rr19.3v 2869 rr19.28v 2870 euxfr2dc 2915 dfif3 3538 undifexmid 4177 exmidexmid 4180 exmidsssnc 4187 copsexg 4227 ordtriexmidlem2 4502 ordtriexmid 4503 ontriexmidim 4504 ordtri2orexmid 4505 ontr2exmid 4507 ordtri2or2exmidlem 4508 onsucsssucexmid 4509 ordsoexmid 4544 0elsucexmid 4547 ordpwsucexmid 4552 ordtri2or2exmid 4553 ontri2orexmidim 4554 dcextest 4563 riotabidv 5808 ov6g 5987 ovg 5988 dfxp3 6170 ssfilem 6849 diffitest 6861 inffiexmid 6880 unfiexmid 6891 snexxph 6923 ctssexmid 7122 exmidonfinlem 7157 ltsopi 7269 pitri3or 7271 creur 8862 creui 8863 pceu 12236 2irrexpqap 13611 subctctexmid 13956 |
Copyright terms: Public domain | W3C validator |