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  726  pm2.621  747  orim1d  787  orim2d  788  pm2.63  800  pm2.74  807  simprimdc  859  oplem1  975  equsex  1728  equsexd  1729  r19.36av  2628  r19.44av  2636  r19.45av  2637  reuss  3418  opthpr  3774  relop  4779  swoord2  6567  indpi  7343  lelttr  8048  elnnz  9265  ztri3or0  9297  xrlelttr  9808  icossicc  9962  iocssicc  9963  ioossico  9964  lmconst  13755  cnptopresti  13777  sslm  13786  bj-exlimmp  14560