| 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 1008 2mo2 2647 ssconb 4142 ssin 4239 2reu4lem 4522 tfr3 8439 trclfvcotr 15048 isprm2 16719 lgsquad2lem2 27429 ostthlem2 27672 pclclN 39893 ifpbibib 43523 elmapintrab 43589 elinintrab 43590 ismnuprim 44313 |
| Copyright terms: Public domain | W3C validator |