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  734  pm2.621  755  orim1d  795  orim2d  796  pm2.63  808  pm2.74  815  simprimdc  867  oplem1  984  equsex  1776  equsexd  1778  r19.36av  2694  r19.44av  2702  r19.45av  2703  reuss  3501  opthpr  3875  relop  4904  swoord2  6796  indpi  7653  lelttr  8358  elnnz  9583  ztri3or0  9615  xrlelttr  10135  icossicc  10289  iocssicc  10290  ioossico  10291  lmconst  15068  cnptopresti  15090  sslm  15099  bj-exlimmp  16528