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

Theorem dfbi2 612
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 186 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 df-an 362 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ps  ->  ph ) )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
31, 2bitr4i 245 1  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  dfbi  613  pm4.71  614  pm5.17  863  xor  866  albiim  1612  nfbi  1738  sbbi  1964  cleqh  2353  ralbiim  2651  reu8  2914  sseq2  3142  soeq2  4271  fun11  5218  dffo3  5574  isnsg2  14574  axextprim  23384  biimpexp  23407  axextndbi  23495  aibandbiaiffaiffb  27116  aibandbiaiaiffb  27117  aibnbna  27128  equextvK  28203
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator