Theorem biidd 172

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 171	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 9	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpbi23d  1006  3anbi12d  1354  3anbi13d  1355  3anbi23d  1356  3anbi1d  1357  3anbi2d  1358  3anbi3d  1359  sb6x  1832  exdistrfor  1853  a16g  1917  rr19.3v  2965  rr19.28v  2966  euxfr2dc  3011  dfif3  3654  undifexmid  4332  exmidexmid  4335  exmidsssnc  4342  copsexg  4386  ordtriexmidlem2  4669  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  ontr2exmid  4674  ordtri2or2exmidlem  4675  onsucsssucexmid  4676  ordsoexmid  4711  0elsucexmid  4714  ordpwsucexmid  4719  ordtri2or2exmid  4720  ontri2orexmidim  4721  dcextest  4730  riotabidv  6043  ov6g  6230  ovg  6231  dfxp3  6434  ssfilem  7181  ssfilemd  7183  diffitest  7195  inffiexmid  7217  unfiexmid  7229  snexxph  7272  ctssexmid  7496  exmidonfinlem  7551  ltsopi  7693  pitri3or  7695  creur  9297  creui  9298  pceu  13103  2irrexpqap  16214  3dom  17223  subctctexmid  17235  wexmiddiffilem  17248