Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bibi2d | Unicode version |
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.) |
Ref | Expression |
---|---|
imbid.1 |
Ref | Expression |
---|---|
bibi2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbid.1 | . . . . 5 | |
2 | 1 | pm5.74i 169 | . . . 4 |
3 | 2 | bibi2i 216 | . . 3 |
4 | pm5.74 168 | . . 3 | |
5 | pm5.74 168 | . . 3 | |
6 | 3, 4, 5 | 3bitr4i 201 | . 2 |
7 | 6 | pm5.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 |