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

Theorem dfbi2 385
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 116 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 110 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
31simpri 112 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓))
42, 3impbii 125 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.71  386  pm5.17dc  889  dcbi  920  orbididc  937  trubifal  1394  albiim  1463  hbbi  1527  hbbid  1554  nfbid  1567  spsbbi  1816  sbbi  1930  cleqh  2237  ralbiim  2564  reu8  2875  sseq2  3116  soeq2  4233  fun11  5185  dffo3  5560  bdbi  13013
  Copyright terms: Public domain W3C validator