![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jcab | Structured version Visualization version GIF version |
Description: Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.) |
Ref | Expression |
---|---|
jcab | ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 484 | . . . 4 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | imim2i 16 | . . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜓)) |
3 | simpr 486 | . . . 4 ⊢ ((𝜓 ∧ 𝜒) → 𝜒) | |
4 | 3 | imim2i 16 | . . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒)) |
5 | 2, 4 | jca 513 | . 2 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) |
6 | pm3.43 475 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒))) | |
7 | 5, 6 | impbii 208 | 1 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 df-an 398 |
This theorem is referenced by: pm4.76 520 pm5.44 544 ordi 1005 2mo2 2644 ssconb 4138 ssin 4231 2reu4lem 4526 tfr3 8399 trclfvcotr 14956 isprm2 16619 lgsquad2lem2 26888 ostthlem2 27131 pclclN 38762 ifpbibib 42261 elmapintrab 42327 elinintrab 42328 ismnuprim 43053 |
Copyright terms: Public domain | W3C validator |