Theorem jcab 517

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.)

Assertion

Ref	Expression
jcab	⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)))

Proof of Theorem 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 208	1 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  pm4.76  518  pm5.44  542  ordi  1004  2mo2  2638  ssconb  4133  ssin  4226  2reu4lem  4521  tfr3  8411  trclfvcotr  14974  isprm2  16638  lgsquad2lem2  27292  ostthlem2  27535  pclclN  39288  ifpbibib  42853  elmapintrab  42919  elinintrab  42920  ismnuprim  43644