Theorem biid 187

Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117.

Assertion

Ref	Expression
biid	|- (ph <-> ph)

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 73	. 2 |- (ph -> ph)
2	1, 1	impbii 174	1 |- (ph <-> ph)

Syntax hints:   <-> wb 163

This theorem is referenced by:  biidd 188  pm5.19 732  3anbi1i 1058  3anbi2i 1059  3anbi3i 1060  tru 1264  eqid 1884  abid2 2011  abid2f 2012  ralbii 2127  rexbii 2128  ceqsexg 2392  wecmpep 3650  ordon 3863  eqfnfv2OLD 4768  dford2 5711  aceq5 5902  aceqkm 5943  zorn 5959  elfz2nn0 7667  climadd 8377  climmul 8388  climcmp 8398  cvgcmp3cetlem2 8450  cvgcmp3ce 8451  ivthlem8 8550  grpidinv 9332  vacnlem4 9670  spwval 10002  spwnex 10004  spwpr4 10006  spwpr4OLD 10007  axgroth5 10132  grothpw 10134  axgroth6 10137  eqid1 10146  projlem 10850  osumlem2 11214  osumlem3 11215  osumlem4 11216  stri 11829  hstri 11837  stcltrthi 11850  bnj193 12063  bnj976 12861  bnj1339 13089  bnj1366 13091  bnj1383 13101  bnj1386 13103  bnj1494 13162  bnj57 13197  bnj59 13198  bnj110 13199  bnj153 13247  bnj516 13257  bnj517 13259  bnj543 13269  bnj544 13270  bnj546 13272  bnj605 13292  bnj579 13302  bnj608 13305  bnj601 13309  bnj616 13311  bnj852 13313  bnj881 13319  bnj893 13324  bnj906 13328  bnj909 13330  bnj917 13333  bnj938 13337  bnj940 13339  bnj977 13354  bnj1003 13368  bnj1029 13382  bnj1034 13385  bnj1124 13424  bnj1128 13428  bnj1127 13429  bnj1125 13430  bnj1147 13432  bnj1151 13436  bnj1188 13451  bnj1203 13454  bnj69 13455  bnj1204 13459  bnj1246 13462  bnj1248 13464  bnj1279 13473  bnj1311 13491  bnj1318 13493  bnj1333 13500  bnj1365 13504  bnj1367 13511  bnj1399 13516  bnj1407 13518  bnj1409 13519  bnj1411 13521  bnj1414 13525  bnj1420 13531  bnj1451 13542  bnj1423 13544  bnj1452 13547  bnj1493 13558  bnj1514 13565  bnj1500 13571  bnj1522 13578  dfon2 13858  axsltsolem1 14006  supdef 14604  cbvprodi 14662  vecval1b 14794  supnuf 15041  ishoma 15136  plibgax0 15320  plibgax1 15321  plibgax2 15322  plibgax3 15323  plibgax4a 15324  plibgax4b 15325  reconnlem3 15448  reconnlem4 15449  reconnlem5 15450  reconn 15451  rrndstprj2 16018  iota2 16393  stbval 16731  stb3xpl 16743  grpidinvNEW 17113  paddval 17259

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