![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr4d | Unicode version |
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.) |
Ref | Expression |
---|---|
3bitr4d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr4d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr4d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr4d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr4d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 3bitr4d.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitr4d 189 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | bitrd 186 |
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 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: dfbi3dc 1333 xordidc 1335 19.32dc 1614 r19.32vdc 2516 opbrop 4517 fvopab3g 5377 respreima 5427 fmptco 5464 cocan1 5566 cocan2 5567 brtposg 6019 nnmword 6275 swoer 6318 erth 6334 brecop 6380 ecopovsymg 6389 xpdom2 6545 pitric 6878 ltexpi 6894 ltapig 6895 ltmpig 6896 ltanqg 6957 ltmnqg 6958 enq0breq 6993 genpassl 7081 genpassu 7082 1idprl 7147 1idpru 7148 caucvgprlemcanl 7201 ltasrg 7314 prsrlt 7330 caucvgsrlemoffcau 7341 axpre-ltadd 7419 subsub23 7685 leadd1 7906 lemul1 8068 reapmul1lem 8069 reapmul1 8070 reapadd1 8071 apsym 8081 apadd1 8083 apti 8097 lediv1 8328 lt2mul2div 8338 lerec 8343 ltdiv2 8346 lediv2 8350 le2msq 8360 avgle1 8654 avgle2 8655 nn01to3 9100 qapne 9122 cnref1o 9131 xleneg 9297 iooneg 9403 iccneg 9404 iccshftr 9409 iccshftl 9411 iccdil 9413 icccntr 9415 fzsplit2 9462 fzaddel 9470 fzrev 9494 elfzo 9556 fzon 9573 elfzom1b 9636 ioo0 9667 ico0 9669 ioc0 9670 flqlt 9686 negqmod0 9734 frec2uzled 9832 expeq0 9982 nn0opthlem1d 10124 leisorel 10238 cjreb 10296 abs00 10493 ltmininf 10661 tanaddaplem 11025 nndivdvds 11076 moddvds 11079 modmulconst 11102 oddm1even 11149 ltoddhalfle 11167 dvdssq 11294 phiprmpw 11472 |
Copyright terms: Public domain | W3C validator |