Theorem jcab 903

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ordi  904  pm4.76  906  pm5.44  948  2mo2  2538  ssconb  3705  ssin  3797  tfr3  7382  trclfvcotr  13598  isprm2  15233  lgsquad2lem2  24910  ostthlem2  25117  pclclN  34195  ifpbibib  36874  elmapintrab  36901  elinintrab  36902  2reu4a  39838