![]() |
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 191 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
5 | 1, 4 | bitrd 188 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: dfbi3dc 1397 xordidc 1399 19.32dc 1679 r19.32vdc 2626 opbrop 4707 fvopab3g 5592 respreima 5647 fmptco 5685 cocan1 5791 cocan2 5792 brtposg 6258 nnmword 6522 swoer 6566 erth 6582 brecop 6628 ecopovsymg 6637 xpdom2 6834 ctssdccl 7113 omniwomnimkv 7168 nninfwlporlemd 7173 pitric 7323 ltexpi 7339 ltapig 7340 ltmpig 7341 ltanqg 7402 ltmnqg 7403 enq0breq 7438 genpassl 7526 genpassu 7527 1idprl 7592 1idpru 7593 caucvgprlemcanl 7646 ltasrg 7772 prsrlt 7789 caucvgsrlemoffcau 7800 ltpsrprg 7805 map2psrprg 7807 axpre-ltadd 7888 subsub23 8165 leadd1 8390 lemul1 8553 reapmul1lem 8554 reapmul1 8555 reapadd1 8556 apsym 8566 apadd1 8568 apti 8582 apcon4bid 8584 lediv1 8829 lt2mul2div 8839 lerec 8844 ltdiv2 8847 lediv2 8851 le2msq 8861 avgle1 9162 avgle2 9163 nn01to3 9620 qapne 9642 cnref1o 9653 xleneg 9840 xsubge0 9884 xleaddadd 9890 iooneg 9991 iccneg 9992 iccshftr 9997 iccshftl 9999 iccdil 10001 icccntr 10003 fzsplit2 10053 fzaddel 10062 fzrev 10087 elfzo 10152 fzon 10169 elfzom1b 10232 ioo0 10263 ico0 10265 ioc0 10266 flqlt 10286 negqmod0 10334 frec2uzled 10432 expeq0 10554 nn0leexp2 10693 nn0opthlem1d 10703 leisorel 10820 cjreb 10878 ltmininf 11246 minclpr 11248 xrmaxlesup 11270 xrltmininf 11281 xrminltinf 11283 tanaddaplem 11749 nndivdvds 11806 moddvds 11809 modmulconst 11833 oddm1even 11883 ltoddhalfle 11901 dvdssq 12035 phiprmpw 12225 eulerthlemh 12234 odzdvds 12248 pc2dvds 12332 1arith 12368 issubg3 13062 eqgid 13096 ablsubsub23 13139 issrgid 13175 isringid 13219 opprunitd 13290 crngunit 13291 unitpropdg 13328 lsslss 13479 lsspropdg 13529 cnrest2 13897 cnptoprest 13900 cnptoprest2 13901 lmss 13907 lmff 13910 txlm 13940 ismet2 14015 blres 14095 xmetec 14098 bdbl 14164 metrest 14167 cnbl0 14195 cnblcld 14196 reopnap 14199 bl2ioo 14203 limcdifap 14292 efle 14358 reapef 14360 logleb 14457 logrpap0b 14458 cxplt 14497 cxple 14498 rpcxple2 14499 rpcxplt2 14500 cxplt3 14501 cxple3 14502 apcxp2 14519 logbleb 14540 logblt 14541 lgsdilem 14589 lgsne0 14600 m1lgs 14613 iooref1o 14944 |
Copyright terms: Public domain | W3C validator |