Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bibi1d | Unicode version |
Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbid.1 |
Ref | Expression |
---|---|
bibi1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbid.1 | . . 3 | |
2 | 1 | bibi2d 231 | . 2 |
3 | bicom 139 | . 2 | |
4 | bicom 139 | . 2 | |
5 | 2, 3, 4 | 3bitr4g 222 | 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: bibi12d 234 bibi1 239 biassdc 1358 eubidh 1983 eubid 1984 axext3 2100 bm1.1 2102 eqeq1 2124 pm13.183 2796 elabgt 2799 elrab3t 2812 mob 2839 sbctt 2947 sbcabel 2962 isoeq2 5671 caovcang 5900 frecabcl 6264 expap0 10291 bezoutlemeu 11622 dfgcd3 11625 bezout 11626 prmdvdsexp 11753 ismet 12440 isxmet 12441 bdsepnft 13012 bdsepnfALT 13014 strcollnft 13109 strcollnfALT 13111 |
Copyright terms: Public domain | W3C validator |