![]() |
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 190 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr3d.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitrd 188 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: csbcomg 3080 eloprabga 5961 ereldm 6577 mapen 6845 ordiso2 7033 subcan 8210 conjmulap 8684 ltrec 8838 divelunit 10000 fseq1m1p1 10092 fzm1 10097 qsqeqor 10627 fihashneq0 10769 hashfacen 10811 cvg1nlemcau 10988 lenegsq 11099 dvdsmod 11862 bezoutlemle 12003 rpexp 12147 qnumdenbi 12186 eulerthlemh 12225 odzdvds 12239 pcelnn 12314 grpidpropdg 12747 mndpropd 12795 mhmpropd 12811 grppropd 12847 cmnpropd 13051 ringpropd 13170 dvdsrpropdg 13269 bdxmet 13894 txmetcnp 13911 cnmet 13923 lgsne0 14332 lgsabs1 14333 |
Copyright terms: Public domain | W3C validator |