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  716  pm2.621  737  orim1d  777  orim2d  778  pm2.63  790  pm2.74  797  simprimdc  845  oplem1  960  equsex  1707  equsexd  1708  r19.36av  2585  r19.44av  2593  r19.45av  2594  reuss  3362  opthpr  3707  relop  4697  swoord2  6467  indpi  7174  lelttr  7876  elnnz  9088  ztri3or0  9120  xrlelttr  9619  icossicc  9773  iocssicc  9774  ioossico  9775  lmconst  12424  cnptopresti  12446  sslm  12455  bj-exlimmp  13147