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

Theorem dfbi2 388
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 117 . . 3  |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) ) )  /\  ( ( (
ph  ->  ps )  /\  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
21simpli 111 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ps )  /\  ( ps  ->  ph )
) )
31simpri 113 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ps  ->  ph ) )  ->  ( ph 
<->  ps ) )
42, 3impbii 126 1  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm4.71  389  pm5.17dc  904  dcbi  936  orbididc  953  trubifal  1416  albiim  1487  hbbi  1548  hbbid  1575  nfbid  1588  spsbbi  1844  sbbi  1959  cleqh  2277  ralbiim  2611  reu8  2933  sseq2  3179  soeq2  4313  fun11  5279  dffo3  5659  bdbi  14234
  Copyright terms: Public domain W3C validator