![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitrd | Unicode version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.) |
Ref | Expression |
---|---|
3bitrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitrd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitrd.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitrd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitrd.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitrd 177 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitrd.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitrd 177 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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: sbceqal 2808 sbcnel12g 2861 elxp4 4751 elxp5 4752 f1eq123d 5064 foeq123d 5065 f1oeq123d 5066 ofrfval 5662 eloprabi 5764 smoeq 5846 ecidg 6106 enqbreq2 6341 ltanqg 6384 apneg 7395 mulext1 7396 ltdiv23 7639 lediv23 7640 halfpos 7933 addltmul 7938 ztri3or 8064 iccf1o 8642 fzshftral 8740 fzoshftral 8864 cjap 9134 |
Copyright terms: Public domain | W3C validator |