Theorem biidd 161

Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)

Assertion

Ref	Expression
biidd	⊢ (𝜑 → (𝜓 ↔ 𝜓))

Proof of Theorem biidd

Step	Hyp	Ref	Expression
1		biid 160	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 9	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3anbi12d  1208  3anbi13d  1209  3anbi23d  1210  3anbi1d  1211  3anbi2d  1212  3anbi3d  1213  sb6x  1662  exdistrfor  1681  a16g  1744  rr19.3v  2682  rr19.28v  2683  euxfr2dc  2726  dfif3  3343  copsexg  3981  ordtriexmidlem2  4246  ordtriexmid  4247  ordtri2orexmid  4248  ontr2exmid  4250  ordtri2or2exmidlem  4251  onsucsssucexmid  4252  ordsoexmid  4286  0elsucexmid  4289  ordpwsucexmid  4294  ordtri2or2exmid  4296  riotabidv  5470  ov6g  5638  ovg  5639  dfxp3  5820  ssfiexmid  6336  diffitest  6344  ltsopi  6418  pitri3or  6420  creur  7911  creui  7912