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

Theorem dfbi2 365
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 ((φψ) ↔ ((φψ) (ψφ)))

Proof of Theorem dfbi2
StepHypRef Expression
1 df-bi 108 . . 3 (((φψ) → ((φψ) (ψφ))) (((φψ) (ψφ)) → (φψ)))
21simpli 102 . 2 ((φψ) → ((φψ) (ψφ)))
31simpri 104 . 2 (((φψ) (ψφ)) → (φψ))
42, 3impbii 115 1 ((φψ) ↔ ((φψ) (ψφ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 95  wb 96
This theorem is referenced by:  pm4.71  366  dfbi1  777  pm5.17  801  pm5.17dc  802  dcbi  824  orbididc  840  trubifal  1245  albiim  1314  hbbi  1377  hbbid  1402  a4sbbi  1606  sbbi  1704  xor  1905
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99
This theorem depends on definitions:  df-bi 108
  Copyright terms: Public domain W3C validator