MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfbi2 Unicode version

Theorem dfbi2 610
Description: A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
dfbi2  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )

Proof of Theorem dfbi2
StepHypRef Expression
1 dfbi1 185 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 df-an 361 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ps  ->  ph ) )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
31, 2bitr4i 244 1  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  dfbi  611  pm4.71  612  pm5.17  859  xor  862  albiim  1618  nfbid  1844  nfbiOLD  1847  sbbi  2097  cleqh  2477  ralbiim  2779  reu8  3066  sseq2  3306  soeq2  4457  fun11  5449  dffo3  5816  isnsg2  14890  axextprim  24922  biimpexp  24945  axextndbi  25178  aibandbiaiffaiffb  27523  aibandbiaiaiffb  27524  sbbiNEW7  28899
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator