Theorem idd 21

Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.)

Assertion

Ref	Expression
idd	⊢ (𝜑 → (𝜓 → 𝜓))

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2	1	a1i 9	1 ⊢ (𝜑 → (𝜓 → 𝜓))

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  728  pm2.621  749  orim1d  789  orim2d  790  pm2.63  802  pm2.74  809  simprimdc  861  oplem1  978  equsex  1752  equsexd  1753  r19.36av  2658  r19.44av  2666  r19.45av  2667  reuss  3455  opthpr  3815  relop  4832  swoord2  6657  indpi  7462  lelttr  8168  elnnz  9389  ztri3or0  9421  xrlelttr  9935  icossicc  10089  iocssicc  10090  ioossico  10091  lmconst  14732  cnptopresti  14754  sslm  14763  bj-exlimmp  15779