![]() |
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 190 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | bitrd 187 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: dfbi3dc 1376 xordidc 1378 19.32dc 1658 r19.32vdc 2583 opbrop 4626 fvopab3g 5502 respreima 5556 fmptco 5594 cocan1 5696 cocan2 5697 brtposg 6159 nnmword 6422 swoer 6465 erth 6481 brecop 6527 ecopovsymg 6536 xpdom2 6733 ctssdccl 7004 omniwomnimkv 7049 pitric 7153 ltexpi 7169 ltapig 7170 ltmpig 7171 ltanqg 7232 ltmnqg 7233 enq0breq 7268 genpassl 7356 genpassu 7357 1idprl 7422 1idpru 7423 caucvgprlemcanl 7476 ltasrg 7602 prsrlt 7619 caucvgsrlemoffcau 7630 ltpsrprg 7635 map2psrprg 7637 axpre-ltadd 7718 subsub23 7991 leadd1 8216 lemul1 8379 reapmul1lem 8380 reapmul1 8381 reapadd1 8382 apsym 8392 apadd1 8394 apti 8408 apcon4bid 8410 lediv1 8651 lt2mul2div 8661 lerec 8666 ltdiv2 8669 lediv2 8673 le2msq 8683 avgle1 8984 avgle2 8985 nn01to3 9436 qapne 9458 cnref1o 9469 xleneg 9650 xsubge0 9694 xleaddadd 9700 iooneg 9801 iccneg 9802 iccshftr 9807 iccshftl 9809 iccdil 9811 icccntr 9813 fzsplit2 9861 fzaddel 9870 fzrev 9895 elfzo 9957 fzon 9974 elfzom1b 10037 ioo0 10068 ico0 10070 ioc0 10071 flqlt 10087 negqmod0 10135 frec2uzled 10233 expeq0 10355 nn0opthlem1d 10498 leisorel 10612 cjreb 10670 ltmininf 11038 minclpr 11040 xrmaxlesup 11060 xrltmininf 11071 xrminltinf 11073 tanaddaplem 11481 nndivdvds 11535 moddvds 11538 modmulconst 11561 oddm1even 11608 ltoddhalfle 11626 dvdssq 11755 phiprmpw 11934 cnrest2 12444 cnptoprest 12447 cnptoprest2 12448 lmss 12454 lmff 12457 txlm 12487 ismet2 12562 blres 12642 xmetec 12645 bdbl 12711 metrest 12714 cnbl0 12742 cnblcld 12743 reopnap 12746 bl2ioo 12750 limcdifap 12839 efle 12905 reapef 12907 logleb 13004 logrpap0b 13005 cxplt 13044 cxple 13045 rpcxple2 13046 rpcxplt2 13047 cxplt3 13048 cxple3 13049 apcxp2 13066 logbleb 13086 logblt 13087 iooref1o 13426 |
Copyright terms: Public domain | W3C validator |