![]() |
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 189 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
5 | 1, 4 | bitrd 186 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: dfbi3dc 1329 xordidc 1331 19.32dc 1610 r19.32vdc 2508 opbrop 4465 fvopab3g 5297 respreima 5347 fmptco 5382 cocan1 5478 cocan2 5479 brtposg 5923 nnmword 6178 swoer 6221 erth 6237 brecop 6283 ecopovsymg 6292 xpdom2 6396 pitric 6625 ltexpi 6641 ltapig 6642 ltmpig 6643 ltanqg 6704 ltmnqg 6705 enq0breq 6740 genpassl 6828 genpassu 6829 1idprl 6894 1idpru 6895 caucvgprlemcanl 6948 ltasrg 7061 prsrlt 7077 caucvgsrlemoffcau 7088 axpre-ltadd 7166 subsub23 7432 leadd1 7653 lemul1 7812 reapmul1lem 7813 reapmul1 7814 reapadd1 7815 apsym 7825 apadd1 7827 apti 7841 lediv1 8066 lt2mul2div 8076 lerec 8081 ltdiv2 8084 lediv2 8088 le2msq 8098 avgle1 8390 avgle2 8391 nn01to3 8835 qapne 8857 cnref1o 8866 xleneg 9032 iooneg 9138 iccneg 9139 iccshftr 9144 iccshftl 9146 iccdil 9148 icccntr 9150 fzsplit2 9197 fzaddel 9205 fzrev 9229 elfzo 9288 fzon 9304 elfzom1b 9367 ioo0 9398 ico0 9400 ioc0 9401 flqlt 9417 negqmod0 9465 frec2uzled 9563 expeq0 9656 nn0opthlem1d 9796 cjreb 9954 abs00 10151 ltmininf 10317 nndivdvds 10409 moddvds 10412 modmulconst 10435 oddm1even 10482 ltoddhalfle 10500 dvdssq 10627 phiprmpw 10805 |
Copyright terms: Public domain | W3C validator |