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

Theorem dfbi2 380
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 115 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 109 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
31simpri 111 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓))
42, 3impbii 124 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm4.71  381  pm5.17dc  844  dcbi  878  orbididc  895  trubifal  1348  albiim  1417  hbbi  1481  hbbid  1508  nfbid  1521  spsbbi  1767  sbbi  1876  cleqh  2182  ralbiim  2497  reu8  2799  sseq2  3032  soeq2  4106  fun11  5033  dffo3  5390  bdbi  11059
  Copyright terms: Public domain W3C validator