![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr4di | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr4di.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bitr4di.2 | ⊢ (𝜃 ↔ 𝜒) |
Ref | Expression |
---|---|
bitr4di | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4di.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | bitr4di.2 | . . 3 ⊢ (𝜃 ↔ 𝜒) | |
3 | 2 | bicomi 132 | . 2 ⊢ (𝜒 ↔ 𝜃) |
4 | 1, 3 | bitrdi 196 | 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: 3bitr4g 223 bibi2i 227 equsalh 1726 eueq3dc 2911 sbcel12g 3072 sbceqg 3073 sbcnel12g 3074 reldisj 3474 r19.3rm 3511 eldifpr 3618 eldiftp 3637 rabxp 4659 elrng 4813 iss 4948 eliniseg 4993 fcnvres 5394 dffv3g 5506 funimass4 5561 fndmdif 5616 fneqeql 5619 funimass3 5627 elrnrexdmb 5651 dff4im 5657 fconst4m 5731 elunirn 5760 riota1 5842 riota2df 5844 f1ocnvfv3 5857 eqfnov 5974 caoftrn 6101 mpoxopovel 6235 rntpos 6251 ordgt0ge1 6429 iinerm 6600 erinxp 6602 qliftfun 6610 mapdm0 6656 elfi2 6964 fifo 6972 inl11 7057 ctssdccl 7103 isomnimap 7128 ismkvmap 7145 iswomnimap 7157 omniwomnimkv 7158 pr2nelem 7183 indpi 7319 genpdflem 7484 genpdisj 7500 genpassl 7501 genpassu 7502 ltnqpri 7571 ltpopr 7572 ltexprlemm 7577 ltexprlemdisj 7583 ltexprlemloc 7584 ltrennb 7831 letri3 8015 letr 8017 ltneg 8396 leneg 8399 reapltxor 8523 apsym 8540 suprnubex 8886 suprleubex 8887 elnnnn0 9195 zrevaddcl 9279 znnsub 9280 znn0sub 9294 prime 9328 eluz2 9510 eluz2b1 9577 nn01to3 9593 qrevaddcl 9620 xrletri3 9778 xrletr 9782 iccid 9899 elicopnf 9943 fzsplit2 10023 fzsn 10039 fzpr 10050 uzsplit 10065 fvinim0ffz 10214 lt2sqi 10580 le2sqi 10581 abs00ap 11042 iooinsup 11256 mertenslem2 11515 fprod2dlemstep 11601 gcddiv 11990 algcvgblem 12019 isprm3 12088 phisum 12210 ring1 13049 crngunit 13092 eltg2b 13187 discld 13269 opnssneib 13289 restbasg 13301 ssidcn 13343 cnptoprest2 13373 lmss 13379 txrest 13409 txlm 13412 imasnopn 13432 bldisj 13534 xmeter 13569 bl2ioo 13675 limcdifap 13764 bj-sseq 14166 nnti 14366 pw1nct 14375 |
Copyright terms: Public domain | W3C validator |