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 180 | . 2 |
5 | 1, 4 | bitrd 177 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
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: dfbi3dc 1288 xordidc 1290 19.32dc 1569 r19.32vdc 2459 r19.12sn 3436 opbrop 4419 fvopab3g 5245 respreima 5295 fmptco 5330 cocan1 5427 cocan2 5428 brtposg 5869 nnmword 6091 swoer 6134 erth 6150 brecop 6196 ecopovsymg 6205 xpdom2 6305 pitric 6419 ltexpi 6435 ltapig 6436 ltmpig 6437 ltanqg 6498 ltmnqg 6499 enq0breq 6534 genpassl 6622 genpassu 6623 1idprl 6688 1idpru 6689 caucvgprlemcanl 6742 ltasrg 6855 prsrlt 6871 caucvgsrlemoffcau 6882 axpre-ltadd 6960 subsub23 7216 leadd1 7425 lemul1 7584 reapmul1lem 7585 reapmul1 7586 reapadd1 7587 apsym 7597 apadd1 7599 apti 7613 lediv1 7835 lt2mul2div 7845 lerec 7850 ltdiv2 7853 lediv2 7857 le2msq 7867 avgle1 8165 avgle2 8166 nn01to3 8552 qapne 8574 cnref1o 8582 xleneg 8750 iooneg 8856 iccneg 8857 iccshftr 8862 iccshftl 8864 iccdil 8866 icccntr 8868 fzsplit2 8914 fzaddel 8922 fzrev 8946 elfzo 9006 fzon 9022 elfzom1b 9085 flqlt 9125 negqmod0 9173 expeq0 9286 cjreb 9466 abs00 9662 |
Copyright terms: Public domain | W3C validator |