Theorem jcab 522

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm4.76  523  pm5.44  547  ordi  1013  2mo2  2651  ssconb  4072  ssin  4167  2reu4lem  4451  tfr3  8328  trclfvcotr  14962  isprm2  16642  lgsquad2lem2  27366  ostthlem2  27609  pclclN  40383  ifpbibib  43954  elmapintrab  44020  elinintrab  44021  ismnuprim  44738