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  778  dcbi  801  orbididc  822  trubifal  1240  albiim  1309  hbbi  1374  hbbid  1400  nfbid  1411  a4sbbi  1635  sbbi  1739  cleqh  1964  ralbiim  2255 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