Theorem bi 513

Description: A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49.

Assertion

Ref	Expression
bi	|- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))

Proof of Theorem bi

Step	Hyp	Ref	Expression
1		bii 158	. 2 |- ((ph <-> ps) <-> -. ((ph -> ps) -> -. (ps -> ph)))
2		df-an 225	. 2 |- (((ph -> ps) /\ (ps -> ph)) <-> -. ((ph -> ps) -> -. (ps -> ph)))
3	1, 2	bitr4 176	1 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  impbid 514  bicom 518  pm4.11 520  con2bi 523  pm5.74 581  bibi2i 606  bibi2d 616  pm5.18 658  pm5.17 666  dfbi 668  orbidi 741  hbbi 1007  albi 1103  hbbid 1108  sbbi 1234  hbsb4t 1244  reu8 1926  sseq1 2072  sseq2 2073  poeq2 2834  soeq2 2845  freq2 2913  funeq 3521  fun11 3548  dffo3 3804  chrelat4 10208

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 147  df-an 225

Copyright terms: Public domain