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

Theorem dfbi2 380
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 115 . . 3  |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) ) )  /\  ( ( (
ph  ->  ps )  /\  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
21simpli 109 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ps )  /\  ( ps  ->  ph )
) )
31simpri 111 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ps  ->  ph ) )  ->  ( ph 
<->  ps ) )
42, 3impbii 124 1  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm4.71  381  pm5.17dc  846  dcbi  880  orbididc  897  trubifal  1350  albiim  1419  hbbi  1483  hbbid  1510  nfbid  1523  spsbbi  1769  sbbi  1878  cleqh  2184  ralbiim  2499  reu8  2802  sseq2  3037  soeq2  4119  fun11  5048  dffo3  5411  bdbi  11186
  Copyright terms: Public domain W3C validator