Theorem biidd 228

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

Assertion

Ref	Expression
biidd	|- (ph -> (ps <-> ps))

Proof of Theorem biidd

Step	Hyp	Ref	Expression
1		biid 227	. 2 |- (ps <-> ps)
2	1	a1i 10	1 |- (ph -> (ps <-> ps))

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3anbi12d  1253  3anbi13d  1254  3anbi23d  1255  3anbi1d  1256  3anbi2d  1257  3anbi3d  1258  had1  1402  spnfwOLD  1692  spvwOLD  1695  exdistrf  1971  nfald2  1972  sb6x  2029  a16gALT  2049  ax11  2155  a16g-o  2186  ax11indalem  2197  ax11inda2ALT  2198  rr19.3v  2981  rr19.28v  2982  moeq3  3014  euxfr2  3022  dfif3  3673  otkelins2kg  4254  otkelins3kg  4255  copsexg  4608  br1stg  4731  dmsnopg  5067  rnsnop  5076  opbr1st  5502  opbr2nd  5503  ov6g  5601  ovg  5602  pmvalg  6011