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

Theorem dfbi2 628
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 192 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 df-an 371 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ps  ->  ph ) )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
31, 2bitr4i 252 1  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  dfbi  629  pm4.71  630  pm5.17  888  xor  891  albiim  1700  nfbid  1934  sbbi  2143  cleqhOLD  2573  ralbiim  2989  reu8  3295  sseq2  3521  soeq2  4829  fun11  5659  dffo3  6047  isnsg2  16357  isarchi  27878  axextprim  29248  biimpexp  29268  axextndbi  29411  aibandbiaiffaiffb  32250  aibandbiaiaiffb  32251  bj-cleqh  34459  bj-ifidg  37808  bj-if1bi  37821  bj-ifbibib  37822  bj-ifdfbi  37831  rp-fakeanorass  37838  frege54cor0a  37991
  Copyright terms: Public domain W3C validator