Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.74i | GIF version |
Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
pm5.74i.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
pm5.74i | ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.74i.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | pm5.74 178 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) | |
3 | 1, 2 | mpbi 144 | 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: bitrd 187 imbi2i 225 bibi2d 231 ibib 244 ibibr 245 anclb 317 pm5.42 318 ancrb 320 equsalh 1704 equsal 1705 sb6a 1961 ralbiia 2447 dfdif3 3181 raaan 3464 exmid01 4116 isprm4 11789 |
Copyright terms: Public domain | W3C validator |