Theorem jcab 520

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 485	. . . 4 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	imim2i 16	. . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜓))
3		simpr 487	. . . 4 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
4	3	imim2i 16	. . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒))
5	2, 4	jca 514	. 2 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)))
6		pm3.43 476	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒)))
7	5, 6	impbii 211	1 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm4.76  521  pm5.44  545  ordi  1002  2mo2  2728  ssconb  4113  ssin  4206  2reu4lem  4464  tfr3  8029  trclfvcotr  14363  isprm2  16020  lgsquad2lem2  25955  ostthlem2  26198  pclclN  37021  ifpbibib  39869  elmapintrab  39929  elinintrab  39930  ismnuprim  40623