Theorem imdistani 435

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 323	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  xoranor  1320  nfan1  1508  sbcof2  1745  difin  3252  difrab  3289  opthreg  4400  wessep  4421  fvelimab  5395  elfvmptrab  5434  dffo4  5486  dffo5  5487  ltaddpr  7253  recgt1i  8456  elnnnn0c  8816  elnnz1  8871  recnz  8938  eluz2b2  9189  elfzp12  9662  cos01gt0  11202  oddnn02np1  11307