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  1708  equsexd  1709  r19.36av  2608  r19.44av  2616  r19.45av  2617  reuss  3388  opthpr  3735  relop  4736  swoord2  6510  indpi  7262  lelttr  7965  elnnz  9177  ztri3or0  9209  xrlelttr  9710  icossicc  9864  iocssicc  9865  ioossico  9866  lmconst  12627  cnptopresti  12649  sslm  12658  bj-exlimmp  13354