![]() |
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 269 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) | |
3 | 1, 2 | mpbi 229 | 1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: bitrd 278 imbi2i 335 bibi2d 342 ibib 367 ibibr 368 pm5.4 389 pm5.42 544 anclb 546 ancrb 548 pm5.3 573 cases2 1046 cador 1609 equsalvw 2007 ax13b 2035 sbcom3vv 2098 equsalv 2258 equsal 2415 2sb6rf 2471 sbcom3 2504 moeu 2576 ralbiia 3090 ceqsal 3507 ceqsalv 3509 ceqsralv 3511 clel2g 3643 clel4g 3648 elabg 3662 dfdif3 4110 csbie2df 4436 ralsng 4670 snssb 4779 frinxp 5750 idrefALT 6101 dfom2 7840 dfacacn 10118 kmlem8 10134 kmlem13 10139 kmlem14 10140 axgroth2 10802 rabeqsnd 31604 bnj1171 33842 bnj1253 33859 filnetlem4 35070 wl-equsalvw 36211 lcmineqlem4 40702 dvrelog2b 40736 elintima 42175 ichexmpl2 45910 |
Copyright terms: Public domain | W3C validator |