ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfbi2 Unicode version

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

Proof of Theorem dfbi2
StepHypRef Expression
1 df-bi 114 . . 3  |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) ) )  /\  ( ( (
ph  ->  ps )  /\  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
21simpli 108 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ps )  /\  ( ps  ->  ph )
) )
31simpri 110 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ps  ->  ph ) )  ->  ( ph 
<->  ps ) )
42, 3impbii 121 1  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm4.71  375  pm5.17dc  821  dcbi  855  orbididc  871  trubifal  1323  albiim  1392  hbbi  1456  hbbid  1483  nfbid  1496  spsbbi  1741  sbbi  1849  cleqh  2153  ralbiim  2464  reu8  2759  sseq2  2994  soeq2  4080  fun11  4993  dffo3  5341  bdbi  10305
  Copyright terms: Public domain W3C validator