ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfbi2 Structured version   Unicode 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  809  dcbi  843  orbididc  859  trubifal  1304  albiim  1373  hbbi  1437  hbbid  1464  nfbid  1477  spsbbi  1722  sbbi  1830  cleqh  2134  ralbiim  2441  reu8  2731  sseq2  2961  soeq2  4044  fun11  4909  dffo3  5257  bdbi  9215
  Copyright terms: Public domain W3C validator