![]() |
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 482 | . . . 4 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
2 | 1 | imim2i 16 | . . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜓)) |
3 | simpr 484 | . . . 4 ⊢ ((𝜓 ∧ 𝜒) → 𝜒) | |
4 | 3 | imim2i 16 | . . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒)) |
5 | 2, 4 | jca 511 | . 2 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) |
6 | pm3.43 473 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒))) | |
7 | 5, 6 | impbii 209 | 1 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
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 df-an 396 |
This theorem is referenced by: pm4.76 518 pm5.44 542 ordi 1007 2mo2 2645 ssconb 4152 ssin 4247 2reu4lem 4528 tfr3 8438 trclfvcotr 15045 isprm2 16716 lgsquad2lem2 27444 ostthlem2 27687 pclclN 39874 ifpbibib 43500 elmapintrab 43566 elinintrab 43567 ismnuprim 44290 |
Copyright terms: Public domain | W3C validator |