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

Theorem bibi2d 221
 Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypothesis
Ref Expression
imbid.1
Assertion
Ref Expression
bibi2d

Proof of Theorem bibi2d
StepHypRef Expression
1 imbid.1 . . . . 5
21pm5.74i 169 . . . 4
32bibi2i 216 . . 3
4 pm5.74 168 . . 3
5 pm5.74 168 . . 3
63, 4, 53bitr4i 201 . 2
76pm5.74ri 170 1
 Colors of variables: wff set class Syntax hints:   wi 4   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:  bibi1d  222  bibi12d  224  biantr  859  bimsc1  870  eujust  1902  euf  1905  ceqex  2671  reu6i  2732  axsep2  3876  zfauscl  3877  copsexg  3981  euotd  3991  cnveq0  4777  iotaval  4878  iota5  4887  eufnfv  5389  isoeq1  5441  isoeq3  5443  isores2  5453  isores3  5455  isotr  5456  isoini2  5458  riota5f  5492  caovordg  5668  caovord  5672  dfoprab4f  5819  nnaword  6084  ltanqg  6498  ltmnqg  6499  ltasrg  6855  axpre-ltadd  6960  bdsep2  10006  bdzfauscl  10010  strcoll2  10108  sscoll2  10113
 Copyright terms: Public domain W3C validator