ILE Home 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