![]() |
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 4101 ssin 4194 2reu4lem 4487 tfr3 8349 trclfvcotr 14903 isprm2 16566 lgsquad2lem2 26756 ostthlem2 26999 pclclN 38404 ifpbibib 41874 elmapintrab 41940 elinintrab 41941 ismnuprim 42666 |
Copyright terms: Public domain | W3C validator |