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 947 bimsc1 958 eujust 2021 euf 2024 ceqex 2857 reu6i 2921 axsep2 4108 zfauscl 4109 copsexg 4229 euotd 4239 cnveq0 5067 iotaval 5171 iota5 5180 eufnfv 5726 isoeq1 5780 isoeq3 5782 isores2 5792 isores3 5794 isotr 5795 isoini2 5798 riota5f 5833 caovordg 6020 caovord 6024 dfoprab4f 6172 frecabcl 6378 nnaword 6490 xpf1o 6822 ltanqg 7362 ltmnqg 7363 ltasrg 7732 axpre-ltadd 7848 prmdvdsexp 12102 bdsep2 13921 bdzfauscl 13925 |
Copyright terms: Public domain | W3C validator |