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  4330  exmidexmid  4333  exmidsssnc  4340  copsexg  4384  ordtriexmidlem2  4667  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  ontr2exmid  4672  ordtri2or2exmidlem  4673  onsucsssucexmid  4674  ordsoexmid  4709  0elsucexmid  4712  ordpwsucexmid  4717  ordtri2or2exmid  4718  ontri2orexmidim  4719  dcextest  4728  riotabidv  6040  ov6g  6227  ovg  6228  dfxp3  6430  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  unfiexmid  7225  snexxph  7267  ctssexmid  7490  exmidonfinlem  7545  ltsopi  7687  pitri3or  7689  creur  9289  creui  9290  pceu  13074  2irrexpqap  16080  3dom  17018  subctctexmid  17030  wexmiddiffilem  17043