![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bibi1d | GIF version |
Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
bibi1d | ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | bibi2d 232 | . 2 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) |
3 | bicom 140 | . 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓)) | |
4 | bicom 140 | . 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 223 | 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: bibi12d 235 bibi1 240 biassdc 1406 eubidh 2044 eubid 2045 axext3 2172 bm1.1 2174 eqeq1 2196 pm13.183 2890 elabgt 2893 elrab3t 2907 mob 2934 sbctt 3044 sbcabel 3059 isoeq2 5819 caovcang 6053 frecabcl 6418 expap0 10568 bezoutlemeu 12026 dfgcd3 12029 bezout 12030 prmdvdsexp 12166 ismet 14241 isxmet 14242 bdsepnft 15036 bdsepnfALT 15038 |
Copyright terms: Public domain | W3C validator |