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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  imim1d  74  ancld  318  ancrd  319  anim12d  328  anim1d  329  anim2d  330  orel2  677  pm2.621  698  orim1d  733  orim2d  734  pm2.63  746  pm2.74  753  simprimdc  789  oplem1  916  equsex  1656  equsexd  1657  r19.36av  2505  r19.44av  2513  r19.45av  2514  reuss  3245  opthpr  3564  relop  4504  swoord2  6159  indpi  6532  lelttr  7199  elnnz  8361  ztri3or0  8393  xrlelttr  8876  icossicc  8983  iocssicc  8984  ioossico  8985  bj-exlimmp  10580