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

Theorem bibi2d 231
 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 179 . . . 4
32bibi2i 226 . . 3
4 pm5.74 178 . . 3
5 pm5.74 178 . . 3
63, 4, 53bitr4i 211 . 2
76pm5.74ri 180 1
 Colors of variables: wff set class Syntax hints:   wi 4   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:  bibi1d  232  bibi12d  234  biantr  937  bimsc1  948  eujust  2002  euf  2005  ceqex  2816  reu6i  2879  axsep2  4055  zfauscl  4056  copsexg  4174  euotd  4184  cnveq0  5003  iotaval  5107  iota5  5116  eufnfv  5656  isoeq1  5710  isoeq3  5712  isores2  5722  isores3  5724  isotr  5725  isoini2  5728  riota5f  5762  caovordg  5946  caovord  5950  dfoprab4f  6099  frecabcl  6304  nnaword  6415  xpf1o  6746  ltanqg  7233  ltmnqg  7234  ltasrg  7603  axpre-ltadd  7719  prmdvdsexp  11863  bdsep2  13256  bdzfauscl  13260
 Copyright terms: Public domain W3C validator