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

Theorem dfbi2 368
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 110 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 104 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
31simpri 106 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓))
42, 3impbii 117 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm4.71  369  pm5.17dc  810  dcbi  844  orbididc  860  trubifal  1307  albiim  1376  hbbi  1440  hbbid  1467  nfbid  1480  spsbbi  1725  sbbi  1833  cleqh  2137  ralbiim  2444  reu8  2734  sseq2  2964  soeq2  4050  fun11  4929  dffo3  5277  bdbi  9795
  Copyright terms: Public domain W3C validator