Theorem imdistani 445

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  syldanl  449  xoranor  1419  nfan1  1610  sbcof2  1856  difin  3441  difrab  3478  opthreg  4648  wessep  4670  fvelimab  5692  elfvmptrab  5732  dffo4  5785  dffo5  5786  ltaddpr  7792  recgt1i  9053  elnnnn0c  9422  elnnz1  9477  recnz  9548  eluz2b2  9806  elfzp12  10303  pfxsuff1eqwrdeq  11239  cos01gt0  12282  oddnn02np1  12399  reumodprminv  12784  sgrpidmndm  13461  elply2  15417  bj-charfundc  16195