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  323  ancrd  324  anim12d  333  anim1d  334  anim2d  335  orel2  715  pm2.621  736  orim1d  776  orim2d  777  pm2.63  789  pm2.74  796  simprimdc  844  oplem1  959  equsex  1706  equsexd  1707  r19.36av  2580  r19.44av  2588  r19.45av  2589  reuss  3352  opthpr  3694  relop  4684  swoord2  6452  indpi  7143  lelttr  7845  elnnz  9057  ztri3or0  9089  xrlelttr  9582  icossicc  9736  iocssicc  9737  ioossico  9738  lmconst  12374  cnptopresti  12396  sslm  12405  bj-exlimmp  12965