![]() |
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-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 1256 3anbi13d 1257 3anbi23d 1258 3anbi1d 1259 3anbi2d 1260 3anbi3d 1261 sb6x 1716 exdistrfor 1735 a16g 1799 rr19.3v 2769 rr19.28v 2770 euxfr2dc 2814 dfif3 3426 undifexmid 4049 exmidexmid 4052 copsexg 4095 ordtriexmidlem2 4365 ordtriexmid 4366 ordtri2orexmid 4367 ontr2exmid 4369 ordtri2or2exmidlem 4370 onsucsssucexmid 4371 ordsoexmid 4406 0elsucexmid 4409 ordpwsucexmid 4414 ordtri2or2exmid 4415 dcextest 4424 riotabidv 5648 ov6g 5820 ovg 5821 dfxp3 6002 ssfilem 6671 diffitest 6683 inffiexmid 6702 unfiexmid 6708 snexxph 6739 ltsopi 6976 pitri3or 6978 creur 8517 creui 8518 |
Copyright terms: Public domain | W3C validator |