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  69  ancld  308  ancrd  309  anim12d  318  anim1d  319  anim2d  320  orel2  645  pm2.621  666  orim1d  701  orim2d  702  pm2.63  713  pm2.74  720  simprimdc  756  oplem1  882  equsex  1616  equsexd  1617  r19.36av  2461  r19.44av  2469  r19.45av  2470  eqsbc3r  2819  reuss  3218  opthpr  3543  relop  4486  swoord2  6136  indpi  6440  lelttr  7106  elnnz  8255  ztri3or0  8287  xrlelttr  8722  icossicc  8829  iocssicc  8830  ioossico  8831  bj-exlimmp  9909