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

Theorem dfbi2 383
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 116 . . 3  |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) ) )  /\  ( ( (
ph  ->  ps )  /\  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
21simpli 110 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ps )  /\  ( ps  ->  ph )
) )
31simpri 112 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ps  ->  ph ) )  ->  ( ph 
<->  ps ) )
42, 3impbii 125 1  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.71  384  pm5.17dc  872  dcbi  903  orbididc  920  trubifal  1377  albiim  1446  hbbi  1510  hbbid  1537  nfbid  1550  spsbbi  1798  sbbi  1908  cleqh  2215  ralbiim  2541  reu8  2851  sseq2  3089  soeq2  4206  fun11  5158  dffo3  5533  bdbi  12847
  Copyright terms: Public domain W3C validator