![]() |
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 486 | . . . 4 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | imim2i 16 | . . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜓)) |
3 | simpr 488 | . . . 4 ⊢ ((𝜓 ∧ 𝜒) → 𝜒) | |
4 | 3 | imim2i 16 | . . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒)) |
5 | 2, 4 | jca 515 | . 2 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) |
6 | pm3.43 477 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒))) | |
7 | 5, 6 | impbii 212 | 1 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: pm4.76 522 pm5.44 546 ordi 1003 2mo2 2709 ssconb 4065 ssin 4157 2reu4lem 4423 tfr3 8018 trclfvcotr 14360 isprm2 16016 lgsquad2lem2 25969 ostthlem2 26212 pclclN 37187 ifpbibib 40218 elmapintrab 40276 elinintrab 40277 ismnuprim 41002 |
Copyright terms: Public domain | W3C validator |