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 323 ancrd 324 anim12d 333 anim1d 334 anim2d 335 orel2 716 pm2.621 737 orim1d 777 orim2d 778 pm2.63 790 pm2.74 797 simprimdc 845 oplem1 960 equsex 1708 equsexd 1709 r19.36av 2608 r19.44av 2616 r19.45av 2617 reuss 3388 opthpr 3735 relop 4736 swoord2 6510 indpi 7262 lelttr 7965 elnnz 9177 ztri3or0 9209 xrlelttr 9710 icossicc 9864 iocssicc 9865 ioossico 9866 lmconst 12627 cnptopresti 12649 sslm 12658 bj-exlimmp 13354 |
Copyright terms: Public domain | W3C validator |