![]() |
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 4705 fvopab3g 5589 respreima 5644 fmptco 5682 cocan1 5787 cocan2 5788 brtposg 6254 nnmword 6518 swoer 6562 erth 6578 brecop 6624 ecopovsymg 6633 xpdom2 6830 ctssdccl 7109 omniwomnimkv 7164 nninfwlporlemd 7169 pitric 7319 ltexpi 7335 ltapig 7336 ltmpig 7337 ltanqg 7398 ltmnqg 7399 enq0breq 7434 genpassl 7522 genpassu 7523 1idprl 7588 1idpru 7589 caucvgprlemcanl 7642 ltasrg 7768 prsrlt 7785 caucvgsrlemoffcau 7796 ltpsrprg 7801 map2psrprg 7803 axpre-ltadd 7884 subsub23 8161 leadd1 8386 lemul1 8549 reapmul1lem 8550 reapmul1 8551 reapadd1 8552 apsym 8562 apadd1 8564 apti 8578 apcon4bid 8580 lediv1 8825 lt2mul2div 8835 lerec 8840 ltdiv2 8843 lediv2 8847 le2msq 8857 avgle1 9158 avgle2 9159 nn01to3 9616 qapne 9638 cnref1o 9649 xleneg 9836 xsubge0 9880 xleaddadd 9886 iooneg 9987 iccneg 9988 iccshftr 9993 iccshftl 9995 iccdil 9997 icccntr 9999 fzsplit2 10049 fzaddel 10058 fzrev 10083 elfzo 10148 fzon 10165 elfzom1b 10228 ioo0 10259 ico0 10261 ioc0 10262 flqlt 10282 negqmod0 10330 frec2uzled 10428 expeq0 10550 nn0leexp2 10689 nn0opthlem1d 10699 leisorel 10816 cjreb 10874 ltmininf 11242 minclpr 11244 xrmaxlesup 11266 xrltmininf 11277 xrminltinf 11279 tanaddaplem 11745 nndivdvds 11802 moddvds 11805 modmulconst 11829 oddm1even 11879 ltoddhalfle 11897 dvdssq 12031 phiprmpw 12221 eulerthlemh 12230 odzdvds 12244 pc2dvds 12328 1arith 12364 issubg3 13050 eqgid 13083 ablsubsub23 13126 issrgid 13162 isringid 13206 opprunitd 13277 crngunit 13278 unitpropdg 13315 cnrest2 13706 cnptoprest 13709 cnptoprest2 13710 lmss 13716 lmff 13719 txlm 13749 ismet2 13824 blres 13904 xmetec 13907 bdbl 13973 metrest 13976 cnbl0 14004 cnblcld 14005 reopnap 14008 bl2ioo 14012 limcdifap 14101 efle 14167 reapef 14169 logleb 14266 logrpap0b 14267 cxplt 14306 cxple 14307 rpcxple2 14308 rpcxplt2 14309 cxplt3 14310 cxple3 14311 apcxp2 14328 logbleb 14349 logblt 14350 lgsdilem 14398 lgsne0 14409 m1lgs 14422 iooref1o 14752 |
Copyright terms: Public domain | W3C validator |