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

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

Proof of Theorem dfbi2
StepHypRef Expression
1 dfbi1 195 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 df-an 373 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ps  ->  ph ) )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
31, 2bitr4i 256 1  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  dfbi  635  pm4.71  636  pm5.17  899  xor  902  albiim  1752  nfbid  2016  sbbi  2230  ralbiim  2922  reu8  3234  sseq2  3454  soeq2  4775  fun11  5648  dffo3  6037  isnsg2  16847  isarchi  28499  axextprim  30328  biimpexp  30348  axextndbi  30451  ifpdfbi  36117  ifpidg  36135  ifp1bi  36146  ifpbibib  36154  rp-fakeanorass  36157  frege54cor0a  36459  dffo3f  37450  aibandbiaiffaiffb  38481  aibandbiaiaiffb  38482
  Copyright terms: Public domain W3C validator