ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfbi2 Structured version   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  pm5.17dc  794  dcbi  823  orbididc  844  trubifal  1267  albiim  1336  hbbi  1403  hbbid  1428  nfbid  1440  spsbbi  1678  sbbi  1782  cleqh  2056  ralbiim  2347  reu8  2631  sseq2  2866
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