MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfbi2 Structured version   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  1621  nfbid  1854  nfbiOLD  1857  sbbi  2145  cleqh  2533  ralbiim  2836  reu8  3123  sseq2  3363  soeq2  4516  fun11  5509  dffo3  5877  isnsg2  14963  isarchi  24245  axextprim  25143  biimpexp  25166  axextndbi  25425  aibandbiaiffaiffb  27830  aibandbiaiaiffb  27831  sbbiNEW7  29508
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