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  727  pm2.621  748  orim1d  788  orim2d  789  pm2.63  801  pm2.74  808  simprimdc  860  oplem1  977  equsex  1742  equsexd  1743  r19.36av  2648  r19.44av  2656  r19.45av  2657  reuss  3444  opthpr  3802  relop  4816  swoord2  6622  indpi  7409  lelttr  8115  elnnz  9336  ztri3or0  9368  xrlelttr  9881  icossicc  10035  iocssicc  10036  ioossico  10037  lmconst  14452  cnptopresti  14474  sslm  14483  bj-exlimmp  15415