Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr3d | Unicode version |
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.) |
Ref | Expression |
---|---|
3bitr3d.1 | |
3bitr3d.2 | |
3bitr3d.3 |
Ref | Expression |
---|---|
3bitr3d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3d.2 | . . 3 | |
2 | 3bitr3d.1 | . . 3 | |
3 | 1, 2 | bitr3d 189 | . 2 |
4 | 3bitr3d.3 | . 2 | |
5 | 3, 4 | bitrd 187 | 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: csbcomg 3025 eloprabga 5858 ereldm 6472 mapen 6740 ordiso2 6920 subcan 8017 conjmulap 8489 ltrec 8641 divelunit 9785 fseq1m1p1 9875 fzm1 9880 fihashneq0 10541 hashfacen 10579 cvg1nlemcau 10756 lenegsq 10867 dvdsmod 11560 bezoutlemle 11696 rpexp 11831 qnumdenbi 11870 bdxmet 12670 txmetcnp 12687 cnmet 12699 |
Copyright terms: Public domain | W3C validator |