![]() |
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 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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: dfbi3dc 1343 xordidc 1345 19.32dc 1625 r19.32vdc 2538 opbrop 4556 fvopab3g 5426 respreima 5480 fmptco 5518 cocan1 5620 cocan2 5621 brtposg 6081 nnmword 6344 swoer 6387 erth 6403 brecop 6449 ecopovsymg 6458 xpdom2 6654 ctssdclemr 6911 pitric 7030 ltexpi 7046 ltapig 7047 ltmpig 7048 ltanqg 7109 ltmnqg 7110 enq0breq 7145 genpassl 7233 genpassu 7234 1idprl 7299 1idpru 7300 caucvgprlemcanl 7353 ltasrg 7466 prsrlt 7482 caucvgsrlemoffcau 7493 axpre-ltadd 7571 subsub23 7838 leadd1 8059 lemul1 8221 reapmul1lem 8222 reapmul1 8223 reapadd1 8224 apsym 8234 apadd1 8236 apti 8250 apcon4bid 8252 lediv1 8485 lt2mul2div 8495 lerec 8500 ltdiv2 8503 lediv2 8507 le2msq 8517 avgle1 8812 avgle2 8813 nn01to3 9259 qapne 9281 cnref1o 9290 xleneg 9461 xsubge0 9505 xleaddadd 9511 iooneg 9612 iccneg 9613 iccshftr 9618 iccshftl 9620 iccdil 9622 icccntr 9624 fzsplit2 9671 fzaddel 9680 fzrev 9705 elfzo 9767 fzon 9784 elfzom1b 9847 ioo0 9878 ico0 9880 ioc0 9881 flqlt 9897 negqmod0 9945 frec2uzled 10043 expeq0 10165 nn0opthlem1d 10307 leisorel 10421 cjreb 10479 ltmininf 10845 minclpr 10847 xrmaxlesup 10867 xrltmininf 10878 xrminltinf 10880 tanaddaplem 11243 nndivdvds 11294 moddvds 11297 modmulconst 11320 oddm1even 11367 ltoddhalfle 11385 dvdssq 11512 phiprmpw 11690 cnrest2 12186 cnptoprest 12189 cnptoprest2 12190 lmss 12196 lmff 12199 txlm 12229 ismet2 12282 blres 12362 xmetec 12365 bdbl 12431 metrest 12434 cnbl0 12456 cnblcld 12457 bl2ioo 12461 limcdifap 12512 |
Copyright terms: Public domain | W3C validator |