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

Theorem dfbi2 374
 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 114 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 108 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
31simpri 110 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓))
42, 3impbii 121 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  pm4.71  375  pm5.17dc  821  dcbi  855  orbididc  871  trubifal  1323  albiim  1392  hbbi  1456  hbbid  1483  nfbid  1496  spsbbi  1741  sbbi  1849  cleqh  2153  ralbiim  2464  reu8  2760  sseq2  2995  soeq2  4081  fun11  4994  dffo3  5342  bdbi  10333
 Copyright terms: Public domain W3C validator