![]() |
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 171 | . 2 ⊢ (𝜓 ↔ 𝜓) | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
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 1323 3anbi13d 1324 3anbi23d 1325 3anbi1d 1326 3anbi2d 1327 3anbi3d 1328 sb6x 1789 exdistrfor 1810 a16g 1874 rr19.3v 2888 rr19.28v 2889 euxfr2dc 2934 dfif3 3559 undifexmid 4205 exmidexmid 4208 exmidsssnc 4215 copsexg 4256 ordtriexmidlem2 4531 ordtriexmid 4532 ontriexmidim 4533 ordtri2orexmid 4534 ontr2exmid 4536 ordtri2or2exmidlem 4537 onsucsssucexmid 4538 ordsoexmid 4573 0elsucexmid 4576 ordpwsucexmid 4581 ordtri2or2exmid 4582 ontri2orexmidim 4583 dcextest 4592 riotabidv 5846 ov6g 6026 ovg 6027 dfxp3 6209 ssfilem 6889 diffitest 6901 inffiexmid 6920 unfiexmid 6931 snexxph 6963 ctssexmid 7162 exmidonfinlem 7206 ltsopi 7333 pitri3or 7335 creur 8930 creui 8931 pceu 12309 2irrexpqap 14749 subctctexmid 15104 |
Copyright terms: Public domain | W3C validator |