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  730  pm2.621  751  orim1d  791  orim2d  792  pm2.63  804  pm2.74  811  simprimdc  863  oplem1  980  equsex  1754  equsexd  1755  r19.36av  2662  r19.44av  2670  r19.45av  2671  reuss  3465  opthpr  3829  relop  4849  swoord2  6680  indpi  7497  lelttr  8203  elnnz  9424  ztri3or0  9456  xrlelttr  9970  icossicc  10124  iocssicc  10125  ioossico  10126  lmconst  14855  cnptopresti  14877  sslm  14886  bj-exlimmp  16043