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 ⊢ (𝜑 → (𝜓 → 𝜓))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1d  75  ancld  325  ancrd  326  anim12d  335  anim1d  336  anim2d  337  orel2  738  pm2.621  759  orim1d  799  orim2d  800  pm2.63  812  pm2.74  819  simprimdc  871  oplem1  988  equsex  1780  equsexd  1782  r19.36av  2702  r19.44av  2710  r19.45av  2711  reuss  3514  opthpr  3897  relop  4930  swoord2  6837  indpi  7709  lelttr  8414  elnnz  9656  ztri3or0  9688  xrlelttr  10210  icossicc  10364  iocssicc  10365  ioossico  10366  issubassa3  15014  lmconst  15319  cnptopresti  15341  sslm  15350  bj-exlimmp  16809