![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > idd | GIF version |
Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.) |
Ref | Expression |
---|---|
idd | ⊢ (𝜑 → (𝜓 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (𝜓 → 𝜓) | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → (𝜓 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: imim1d 75 ancld 325 ancrd 326 anim12d 335 anim1d 336 anim2d 337 orel2 726 pm2.621 747 orim1d 787 orim2d 788 pm2.63 800 pm2.74 807 simprimdc 859 oplem1 975 equsex 1728 equsexd 1729 r19.36av 2628 r19.44av 2636 r19.45av 2637 reuss 3416 opthpr 3770 relop 4772 swoord2 6558 indpi 7319 lelttr 8023 elnnz 9239 ztri3or0 9271 xrlelttr 9780 icossicc 9934 iocssicc 9935 ioossico 9936 lmconst 13349 cnptopresti 13371 sslm 13380 bj-exlimmp 14143 |
Copyright terms: Public domain | W3C validator |