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  1422  nfan1  1613  sbcof2  1858  difin  3446  difrab  3483  rabsnifsb  3741  opthreg  4660  wessep  4682  fvelimab  5711  elfvmptrab  5751  dffo4  5803  dffo5  5804  ltaddpr  7860  recgt1i  9121  elnnnn0c  9490  elnnz1  9545  recnz  9616  eluz2b2  9880  elfzp12  10377  pfxsuff1eqwrdeq  11327  cos01gt0  12385  oddnn02np1  12502  reumodprminv  12887  sgrpidmndm  13564  elply2  15526  bj-charfundc  16504