Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bibi2i | GIF version |
Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.) |
Ref | Expression |
---|---|
bibi.a | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
bibi2i | ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜑)) | |
2 | bibi.a | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | bitrdi 195 | . 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓)) |
4 | id 19 | . . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓)) | |
5 | 4, 2 | bitr4di 197 | . 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑)) |
6 | 3, 5 | impbii 125 | 1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ↔ 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: bibi1i 227 bibi12i 228 bibi2d 231 pm4.71r 388 sblbis 1953 sbrbif 1955 abeq2 2279 abid2f 2338 necon4biddc 2415 pm13.183 2868 disj3 3467 euabsn2 3652 a9evsep 4111 inex1 4123 zfpair2 4195 sucel 4395 bdinex1 13934 bj-zfpair2 13945 bj-d0clsepcl 13960 |
Copyright terms: Public domain | W3C validator |