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 1377 eubidh 2012 eubid 2013 axext3 2140 bm1.1 2142 eqeq1 2164 pm13.183 2850 elabgt 2853 elrab3t 2867 mob 2894 sbctt 3003 sbcabel 3018 isoeq2 5752 caovcang 5982 frecabcl 6346 expap0 10449 bezoutlemeu 11891 dfgcd3 11894 bezout 11895 prmdvdsexp 12023 ismet 12755 isxmet 12756 bdsepnft 13473 bdsepnfALT 13475 |
Copyright terms: Public domain | W3C validator |