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  733  pm2.621  754  orim1d  794  orim2d  795  pm2.63  807  pm2.74  814  simprimdc  866  oplem1  983  equsex  1775  equsexd  1776  r19.36av  2683  r19.44av  2691  r19.45av  2692  reuss  3487  opthpr  3856  relop  4882  swoord2  6737  indpi  7567  lelttr  8273  elnnz  9494  ztri3or0  9526  xrlelttr  10046  icossicc  10200  iocssicc  10201  ioossico  10202  lmconst  14969  cnptopresti  14991  sslm  15000  bj-exlimmp  16426