![]() |
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 179 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) | |
3 | 1, 2 | mpbi 145 | 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: bitrd 188 imbi2i 226 bibi2d 232 ibib 245 ibibr 246 anclb 319 pm5.42 320 ancrb 322 equsalh 1726 equsal 1727 equsalv 1793 sb6a 1988 ralbiia 2491 dfdif3 3247 raaan 3531 snssb 3727 exmid01 4200 isprm4 12121 |
Copyright terms: Public domain | W3C validator |