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  4645  wessep  4667  fvelimab  5683  elfvmptrab  5723  dffo4  5776  dffo5  5777  ltaddpr  7772  recgt1i  9033  elnnnn0c  9402  elnnz1  9457  recnz  9528  eluz2b2  9786  elfzp12  10283  pfxsuff1eqwrdeq  11217  cos01gt0  12260  oddnn02np1  12377  reumodprminv  12762  sgrpidmndm  13439  elply2  15394  bj-charfundc  16101