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  1356  nfan1  1544  sbcof2  1783  difin  3318  difrab  3355  opthreg  4479  wessep  4500  fvelimab  5485  elfvmptrab  5524  dffo4  5576  dffo5  5577  ltaddpr  7429  recgt1i  8680  elnnnn0c  9046  elnnz1  9101  recnz  9168  eluz2b2  9424  elfzp12  9910  cos01gt0  11505  oddnn02np1  11613