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 3063 eloprabga 5920 ereldm 6535 mapen 6803 ordiso2 6991 subcan 8144 conjmulap 8616 ltrec 8769 divelunit 9929 fseq1m1p1 10020 fzm1 10025 fihashneq0 10697 hashfacen 10735 cvg1nlemcau 10912 lenegsq 11023 dvdsmod 11785 bezoutlemle 11926 rpexp 12064 qnumdenbi 12103 eulerthlemh 12142 odzdvds 12156 pcelnn 12231 bdxmet 13048 txmetcnp 13065 cnmet 13077 |
Copyright terms: Public domain | W3C validator |