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: wi 4 wb 104 |
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 1375 xordidc 1377 19.32dc 1657 r19.32vdc 2580 opbrop 4618 fvopab3g 5494 respreima 5548 fmptco 5586 cocan1 5688 cocan2 5689 brtposg 6151 nnmword 6414 swoer 6457 erth 6473 brecop 6519 ecopovsymg 6528 xpdom2 6725 ctssdccl 6996 pitric 7129 ltexpi 7145 ltapig 7146 ltmpig 7147 ltanqg 7208 ltmnqg 7209 enq0breq 7244 genpassl 7332 genpassu 7333 1idprl 7398 1idpru 7399 caucvgprlemcanl 7452 ltasrg 7578 prsrlt 7595 caucvgsrlemoffcau 7606 ltpsrprg 7611 map2psrprg 7613 axpre-ltadd 7694 subsub23 7967 leadd1 8192 lemul1 8355 reapmul1lem 8356 reapmul1 8357 reapadd1 8358 apsym 8368 apadd1 8370 apti 8384 apcon4bid 8386 lediv1 8627 lt2mul2div 8637 lerec 8642 ltdiv2 8645 lediv2 8649 le2msq 8659 avgle1 8960 avgle2 8961 nn01to3 9409 qapne 9431 cnref1o 9440 xleneg 9620 xsubge0 9664 xleaddadd 9670 iooneg 9771 iccneg 9772 iccshftr 9777 iccshftl 9779 iccdil 9781 icccntr 9783 fzsplit2 9830 fzaddel 9839 fzrev 9864 elfzo 9926 fzon 9943 elfzom1b 10006 ioo0 10037 ico0 10039 ioc0 10040 flqlt 10056 negqmod0 10104 frec2uzled 10202 expeq0 10324 nn0opthlem1d 10466 leisorel 10580 cjreb 10638 ltmininf 11006 minclpr 11008 xrmaxlesup 11028 xrltmininf 11039 xrminltinf 11041 tanaddaplem 11445 nndivdvds 11499 moddvds 11502 modmulconst 11525 oddm1even 11572 ltoddhalfle 11590 dvdssq 11719 phiprmpw 11898 cnrest2 12405 cnptoprest 12408 cnptoprest2 12409 lmss 12415 lmff 12418 txlm 12448 ismet2 12523 blres 12603 xmetec 12606 bdbl 12672 metrest 12675 cnbl0 12703 cnblcld 12704 reopnap 12707 bl2ioo 12711 limcdifap 12800 |
Copyright terms: Public domain | W3C validator |