Theorem imdistani 442

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  1359  nfan1  1544  sbcof2  1790  difin  3344  difrab  3381  opthreg  4515  wessep  4537  fvelimab  5524  elfvmptrab  5563  dffo4  5615  dffo5  5616  ltaddpr  7517  recgt1i  8769  elnnnn0c  9135  elnnz1  9190  recnz  9257  eluz2b2  9514  elfzp12  10001  cos01gt0  11659  oddnn02np1  11770  bj-charfundc  13383