Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bibi12d | GIF version |
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbi12d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
imbi12d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Ref | Expression |
---|---|
bibi12d | ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi12d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | bibi1d 222 | . 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
3 | imbi12d.2 | . . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 3 | bibi2d 221 | . 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
5 | 2, 4 | bitrd 177 | 1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm5.32 426 bi2bian9 540 cleqh 2137 abbi 2151 cleqf 2201 vtoclb 2611 vtoclbg 2614 ceqsexg 2672 elabgf 2685 reu6 2730 ru 2763 sbcbig 2809 sbcne12g 2868 sbcnestgf 2897 preq12bg 3544 nalset 3887 opthg 3975 opelopabsb 3997 wetriext 4301 opeliunxp2 4476 resieq 4622 elimasng 4693 cbviota 4872 iota2df 4891 fnbrfvb 5214 fvelimab 5229 fmptco 5330 fsng 5336 fressnfv 5350 funfvima3 5392 isorel 5448 isocnv 5451 isocnv2 5452 isotr 5456 ovg 5639 caovcang 5662 caovordg 5668 caovord3d 5671 caovord 5672 dftpos4 5878 ecopovsym 6202 ecopovsymg 6205 nneneq 6320 ltanqg 6498 ltmnqg 6499 elinp 6572 prnmaxl 6586 prnminu 6587 ltasrg 6855 axpre-ltadd 6960 zextle 8331 zextlt 8332 climshft 9825 bj-nalset 10015 bj-d0clsepcl 10049 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |