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 1713 equsal 1714 equsalv 1780 sb6a 1975 ralbiia 2478 dfdif3 3227 raaan 3510 exmid01 4171 isprm4 12030 |
Copyright terms: Public domain | W3C validator |