![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr4d | GIF 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 1285 xordidc 1287 19.32dc 1566 r19.32vdc 2453 r19.12sn 3427 opbrop 4362 fvopab3g 5188 respreima 5238 fmptco 5273 cocan1 5370 cocan2 5371 brtposg 5810 nnmword 6027 swoer 6070 erth 6086 brecop 6132 ecopovsymg 6141 xpdom2 6241 pitric 6305 ltexpi 6321 ltapig 6322 ltmpig 6323 ltanqg 6384 ltmnqg 6385 enq0breq 6419 genpassl 6507 genpassu 6508 1idprl 6566 1idpru 6567 cauappcvgprlemcan 6616 ltasrg 6698 axpre-ltadd 6770 subsub23 7013 leadd1 7220 lemul1 7377 reapmul1lem 7378 reapmul1 7379 reapadd1 7380 apsym 7390 apadd1 7392 apti 7406 lediv1 7616 lt2mul2div 7626 lerec 7631 ltdiv2 7634 lediv2 7638 le2msq 7648 avgle1 7942 avgle2 7943 nn01to3 8328 qapne 8350 cnref1o 8357 xleneg 8520 iooneg 8626 iccneg 8627 iccshftr 8632 iccshftl 8634 iccdil 8636 icccntr 8638 fzsplit2 8684 fzaddel 8692 fzrev 8716 elfzo 8776 fzon 8792 elfzom1b 8855 expeq0 8940 cjreb 9094 |
Copyright terms: Public domain | W3C validator |