Theorem imdistani 441

Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)

Hypothesis

Ref	Expression
imdistani.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imdistani	⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Proof of Theorem imdistani

Step	Hyp	Ref	Expression
1		imdistani.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	anc2li 327	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  xoranor  1355  nfan1  1543  sbcof2  1782  difin  3308  difrab  3345  opthreg  4466  wessep  4487  fvelimab  5470  elfvmptrab  5509  dffo4  5561  dffo5  5562  ltaddpr  7398  recgt1i  8649  elnnnn0c  9015  elnnz1  9070  recnz  9137  eluz2b2  9390  elfzp12  9872  cos01gt0  11458  oddnn02np1  11566