![]() |
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 191 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 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: dfbi3dc 1408 xordidc 1410 19.32dc 1690 r19.32vdc 2639 opbrop 4723 fvopab3g 5610 respreima 5665 fmptco 5703 cocan1 5809 cocan2 5810 brtposg 6280 nnmword 6544 swoer 6588 erth 6606 brecop 6652 ecopovsymg 6661 xpdom2 6858 pw2f1odclem 6863 ctssdccl 7141 omniwomnimkv 7196 nninfwlporlemd 7201 pitric 7351 ltexpi 7367 ltapig 7368 ltmpig 7369 ltanqg 7430 ltmnqg 7431 enq0breq 7466 genpassl 7554 genpassu 7555 1idprl 7620 1idpru 7621 caucvgprlemcanl 7674 ltasrg 7800 prsrlt 7817 caucvgsrlemoffcau 7828 ltpsrprg 7833 map2psrprg 7835 axpre-ltadd 7916 subsub23 8193 leadd1 8418 lemul1 8581 reapmul1lem 8582 reapmul1 8583 reapadd1 8584 apsym 8594 apadd1 8596 apti 8610 apcon4bid 8612 lediv1 8857 lt2mul2div 8867 lerec 8872 ltdiv2 8875 lediv2 8879 le2msq 8889 avgle1 9190 avgle2 9191 nn01to3 9649 qapne 9671 cnref1o 9682 xleneg 9869 xsubge0 9913 xleaddadd 9919 iooneg 10020 iccneg 10021 iccshftr 10026 iccshftl 10028 iccdil 10030 icccntr 10032 fzsplit2 10082 fzaddel 10091 fzrev 10116 elfzo 10181 fzon 10198 elfzom1b 10261 ioo0 10292 ico0 10294 ioc0 10295 flqlt 10316 negqmod0 10364 frec2uzled 10462 expeq0 10585 nn0leexp2 10725 nn0opthlem1d 10735 leisorel 10852 cjreb 10910 ltmininf 11278 minclpr 11280 xrmaxlesup 11302 xrltmininf 11313 xrminltinf 11315 tanaddaplem 11781 nndivdvds 11838 moddvds 11841 modmulconst 11865 oddm1even 11915 ltoddhalfle 11933 dvdssq 12067 phiprmpw 12257 eulerthlemh 12266 odzdvds 12280 pc2dvds 12365 1arith 12402 issubg3 13148 eqgid 13182 resghm2b 13218 conjghm 13232 conjnmzb 13236 ablsubsub23 13281 issrgid 13352 isringid 13396 opprsubgg 13451 opprunitd 13477 crngunit 13478 unitpropdg 13515 issubrng 13563 opprsubrngg 13575 lsslss 13714 lsspropdg 13764 cnrest2 14213 cnptoprest 14216 cnptoprest2 14217 lmss 14223 lmff 14226 txlm 14256 ismet2 14331 blres 14411 xmetec 14414 bdbl 14480 metrest 14483 cnbl0 14511 cnblcld 14512 reopnap 14515 bl2ioo 14519 limcdifap 14608 efle 14674 reapef 14676 logleb 14773 logrpap0b 14774 cxplt 14813 cxple 14814 rpcxple2 14815 rpcxplt2 14816 cxplt3 14817 cxple3 14818 apcxp2 14835 logbleb 14856 logblt 14857 lgsdilem 14906 lgsne0 14917 m1lgs 14930 iooref1o 15261 |
Copyright terms: Public domain | W3C validator |