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

Theorem dfbi2 633
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  634  pm4.71  635  pm5.17  897  xor  900  albiim  1744  nfbid  1990  sbbi  2196  cleqhOLD  2539  ralbiim  2961  reu8  3268  sseq2  3487  soeq2  4792  fun11  5664  dffo3  6050  isnsg2  16840  isarchi  28500  axextprim  30330  biimpexp  30350  axextndbi  30452  bj-cleqh  31351  ifpdfbi  36081  ifpidg  36099  ifp1bi  36110  ifpbibib  36118  rp-fakeanorass  36121  frege54cor0a  36361  dffo3f  37344  aibandbiaiffaiffb  38238  aibandbiaiaiffb  38239
  Copyright terms: Public domain W3C validator