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

Theorem dfbi2 626
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 369 . 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 367
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 369
This theorem is referenced by:  dfbi  627  pm4.71  628  pm5.17  887  xor  890  albiim  1718  nfbid  1959  sbbi  2164  cleqhOLD  2516  ralbiim  2936  reu8  3242  sseq2  3461  soeq2  4761  fun11  5588  dffo3  5978  isnsg2  16445  isarchi  28059  axextprim  29778  biimpexp  29798  axextndbi  29905  bj-cleqh  30905  ifpdfbi  35528  ifpidg  35546  ifp1bi  35557  ifpbibib  35565  rp-fakeanorass  35568  frege54cor0a  35808  aibandbiaiffaiffb  37424  aibandbiaiaiffb  37425
  Copyright terms: Public domain W3C validator