Theorem biidd 188

Description: Principle of identity with antecedent.

Assertion

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

Proof of Theorem biidd

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

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  3anbi12d 1169  3anbi13d 1170  3anbi23d 1171  3anbi1d 1172  3anbi2d 1173  3anbi3d 1174  sb6x 1553  ax11 1589  sbidmOLD 1628  a16g 1653  a16gOLD 1654  ax11indalem 1759  ax11inda2ALT 1760  moeq3 2432  euxfr2 2437  sbcgf 2520  copsexg 3537  soeq1 3608  ordtri3or 3691  reuxfr2d 3844  reuxfr2 3845  weinxp 4059  tz6.12-2 4696  oprabval6g 4962  eloprabi 5060  fparlem3 5083  fparlem4 5084  trsbc 5843  aceq1 5891  aceq2 5893  axpowndlem4 6104  axpownd 6105  axinfndlem1 6109  axacndlem4 6114  ltsopr 6288  brtxp 14067  altdftru 14283  supdef 14604  istoset2 14628  isseg1 15304  isseg2 15305  isplibg4a 15315  isplibg4b 15317  oprabvalg 15706  oprpiece1res1 15880  oprpiece1res2 15881  tlmbrf 15905  pcorev 16087  trsbcVD 16701  elstrscaf 16716  poslem 16774  islvec 17188

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

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain