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  323  ancrd  324  anim12d  333  anim1d  334  anim2d  335  orel2  722  pm2.621  743  orim1d  783  orim2d  784  pm2.63  796  pm2.74  803  simprimdc  855  oplem1  971  equsex  1722  equsexd  1723  r19.36av  2622  r19.44av  2630  r19.45av  2631  reuss  3409  opthpr  3760  relop  4762  swoord2  6547  indpi  7308  lelttr  8012  elnnz  9226  ztri3or0  9258  xrlelttr  9767  icossicc  9921  iocssicc  9922  ioossico  9923  lmconst  13095  cnptopresti  13117  sslm  13126  bj-exlimmp  13889