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 221 | . 2 |
3 | bicom 128 | . 2 | |
4 | bicom 128 | . 2 | |
5 | 2, 3, 4 | 3bitr4g 212 | 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: bibi12d 224 bibi1 229 biassdc 1286 eubidh 1906 eubid 1907 axext3 2023 bm1.1 2025 eqeq1 2046 pm13.183 2681 elabgt 2684 elrab3t 2697 mob 2723 sbctt 2824 sbcabel 2839 isoeq2 5442 caovcang 5662 expap0 9285 bdsepnft 10007 bdsepnfALT 10009 strcollnft 10109 strcollnfALT 10111 |
Copyright terms: Public domain | W3C validator |