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 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 271 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) | |
3 | 1, 2 | mpbi 231 | 1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: bitrd 280 imbi2i 337 bibi2d 344 ibib 369 ibibr 370 pm5.4 390 pm5.42 544 anclb 546 ancrb 548 pm5.3 573 cases2 1039 cador 1600 equsalvw 2001 ax13b 2030 sbcom3vv 2097 equsalv 2258 equsal 2430 2sb6rf 2489 2sb6rfOLD 2490 sbcom3 2541 moeu 2661 ralbiia 3161 dfdif3 4088 frinxp 5627 idrefALT 5966 dfom2 7571 dfacacn 9555 kmlem8 9571 kmlem13 9576 kmlem14 9577 axgroth2 10235 rabeqsnd 30191 bnj1171 32169 bnj1253 32186 filnetlem4 33626 wl-equsalvw 34659 elintima 39876 ichexmpl2 43509 |
Copyright terms: Public domain | W3C validator |