| 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 270 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) | |
| 3 | 1, 2 | mpbi 230 | 1 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: bitrd 279 imbi2i 336 bibi2d 342 ibib 367 ibibr 368 pm5.4 388 pm5.42 543 anclb 545 ancrb 547 pm5.3 572 cases2 1048 cador 1608 equsalvw 2003 ax13b 2031 sbbiiev 2092 equsalv 2267 equsal 2422 2sb6rf 2478 sbcom3 2511 moeu 2583 ralbiia 3091 ceqsal 3519 ceqsalv 3521 ceqsralv 3522 clel2g 3659 clel4g 3663 elabg 3676 dfdif3OLD 4118 csbie2df 4443 rabeqsnd 4669 ralsng 4675 snssb 4782 frinxp 5768 idrefALT 6131 dfom2 7889 dfacacn 10182 kmlem8 10198 kmlem13 10203 kmlem14 10204 axgroth2 10865 bnj1171 35014 bnj1253 35031 orbi2iALT 35690 filnetlem4 36382 wl-equsalvw 37539 lcmineqlem4 42033 dvrelog2b 42067 aks6d1c1 42117 aks6d1c4 42125 aks6d1c6lem3 42173 elintima 43666 ichexmpl2 47457 |
| Copyright terms: Public domain | W3C validator |