Theorem bi 396

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 140	. 2 |- ((ph <-> ps) <-> -. ((ph -> ps) -> -. (ps -> ph)))
2		df-an 198	. 2 |- (((ph -> ps) /\ (ps -> ph)) <-> -. ((ph -> ps) -> -. (ps -> ph)))
3	1, 2	bitr4 154	1 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  impbid 397  bicom 398  pm4.11 400  bicon2 403  pm5.74 442  bibi2i 460  bibi2d 470  pm5.18 497  dfbi 499  orbidi 510  hbbi 705  albi 785  hbbid 789  sbbi 890  hbsb4t 906  sseq1 1521  sseq2 1522  poeq2 2131  soeq2 2142  freq2 2175  funeq 2683

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org