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 657  pm5.17 665  dfbi 667  orbidi 740  hbbi 986  albi 1083  hbbid 1088  sbbi 1223  hbsb4t 1233  reu8 1907  sseq1 2053  sseq2 2054  poeq2 2807  soeq2 2818  freq2 2886  funeq 3476  fun11 3502  dffo3 3758  chrelat4 10422

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