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  2980  rr19.28v  2981  moeq3  3013  euxfr2  3021  dfif3  3672  otkelins2kg  4253  otkelins3kg  4254  copsexg  4607  br1stg  4730  dmsnopg  5066  rnsnop  5075  opbr1st  5501  opbr2nd  5502  ov6g  5600  ovg  5601  pmvalg  6010