Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bibi2d | GIF version |
Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
Ref | Expression |
---|---|
imbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
bibi2d | ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbid.1 | . . . . 5 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | pm5.74i 179 | . . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) |
3 | 2 | bibi2i 226 | . . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒))) |
4 | pm5.74 178 | . . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓))) | |
5 | pm5.74 178 | . . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒))) | |
6 | 3, 4, 5 | 3bitr4i 211 | . 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒))) |
7 | 6 | pm5.74ri 180 | 1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: bibi1d 232 bibi12d 234 biantr 921 bimsc1 932 eujust 1979 euf 1982 ceqex 2786 reu6i 2848 axsep2 4017 zfauscl 4018 copsexg 4136 euotd 4146 cnveq0 4965 iotaval 5069 iota5 5078 eufnfv 5616 isoeq1 5670 isoeq3 5672 isores2 5682 isores3 5684 isotr 5685 isoini2 5688 riota5f 5722 caovordg 5906 caovord 5910 dfoprab4f 6059 frecabcl 6264 nnaword 6375 xpf1o 6706 ltanqg 7176 ltmnqg 7177 ltasrg 7546 axpre-ltadd 7662 prmdvdsexp 11753 bdsep2 13011 bdzfauscl 13015 strcoll2 13108 sscoll2 13113 |
Copyright terms: Public domain | W3C validator |