![]() |
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 231 | . 2 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) |
3 | bicom 139 | . 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓)) | |
4 | bicom 139 | . 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 222 | 1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: bibi12d 234 bibi1 239 biassdc 1332 eubidh 1955 eubid 1956 axext3 2072 bm1.1 2074 eqeq1 2095 pm13.183 2755 elabgt 2758 elrab3t 2771 mob 2798 sbctt 2906 sbcabel 2921 isoeq2 5595 caovcang 5820 frecabcl 6178 expap0 10046 bezoutlemeu 11335 dfgcd3 11338 bezout 11339 prmdvdsexp 11466 bdsepnft 12051 bdsepnfALT 12053 strcollnft 12152 strcollnfALT 12154 |
Copyright terms: Public domain | W3C validator |