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  731  pm2.621  752  orim1d  792  orim2d  793  pm2.63  805  pm2.74  812  simprimdc  864  oplem1  981  equsex  1774  equsexd  1775  r19.36av  2682  r19.44av  2690  r19.45av  2691  reuss  3485  opthpr  3850  relop  4872  swoord2  6718  indpi  7537  lelttr  8243  elnnz  9464  ztri3or0  9496  xrlelttr  10010  icossicc  10164  iocssicc  10165  ioossico  10166  lmconst  14898  cnptopresti  14920  sslm  14929  bj-exlimmp  16157