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  3442  difrab  3479  rabsnifsb  3735  opthreg  4652  wessep  4674  fvelimab  5698  elfvmptrab  5738  dffo4  5791  dffo5  5792  ltaddpr  7810  recgt1i  9071  elnnnn0c  9440  elnnz1  9495  recnz  9566  eluz2b2  9830  elfzp12  10327  pfxsuff1eqwrdeq  11273  cos01gt0  12317  oddnn02np1  12434  reumodprminv  12819  sgrpidmndm  13496  elply2  15452  bj-charfundc  16353