![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm5.74i | Structured version Visualization version GIF version |
Description: Distribution of implication over biconditional (inference rule). (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 259 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) | |
3 | 1, 2 | mpbi 220 | 1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 |
This theorem is referenced by: bitrd 268 imbi2i 325 bibi2d 331 ibib 356 ibibr 357 anclb 571 pm5.42 572 ancrb 574 cases2 1034 cador 1696 equsalvw 2086 ax13b 2115 equsalv 2255 equsalhw 2270 equsal 2436 sbcom3 2548 2sb6rf 2589 ralbiia 3117 dfdif3 3863 frinxp 5341 dfom2 7232 dfacacn 9155 kmlem8 9171 kmlem13 9176 kmlem14 9177 axgroth2 9839 rabeqsnd 29649 bnj1171 31375 bnj1253 31392 filnetlem4 32682 bj-ssb1a 32938 bj-ssb1 32939 bj-ssbcom3lem 32956 wl-sbcom3 33685 elintima 38447 |
Copyright terms: Public domain | W3C validator |