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 179 | . . . 4 |
3 | 2 | bibi2i 226 | . . 3 |
4 | pm5.74 178 | . . 3 | |
5 | pm5.74 178 | . . 3 | |
6 | 3, 4, 5 | 3bitr4i 211 | . 2 |
7 | 6 | pm5.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 941 bimsc1 952 eujust 2015 euf 2018 ceqex 2848 reu6i 2912 axsep2 4095 zfauscl 4096 copsexg 4216 euotd 4226 cnveq0 5054 iotaval 5158 iota5 5167 eufnfv 5709 isoeq1 5763 isoeq3 5765 isores2 5775 isores3 5777 isotr 5778 isoini2 5781 riota5f 5816 caovordg 6000 caovord 6004 dfoprab4f 6153 frecabcl 6358 nnaword 6470 xpf1o 6801 ltanqg 7332 ltmnqg 7333 ltasrg 7702 axpre-ltadd 7818 prmdvdsexp 12059 bdsep2 13609 bdzfauscl 13613 |
Copyright terms: Public domain | W3C validator |