Theorem bi 514

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 515  bicom 519  pm4.11 521  con2bi 524  pm5.74 582  bibi2i 607  bibi2d 617  pm5.18 659  pm5.17 667  dfbi 669  orbidi 742  hbbi 1008  albi 1105  hbbid 1110  sbbi 1237  hbsb4t 1247  reu8 1932  sseq1 2078  sseq2 2079  poeq2 2838  soeq2 2849  freq2 2918  funeq 3527  fun11 3554  dffo3 3810  chrelat4 10237

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