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  1397  nfan1  1588  sbcof2  1834  difin  3412  difrab  3449  opthreg  4609  wessep  4631  fvelimab  5645  elfvmptrab  5685  dffo4  5738  dffo5  5739  ltaddpr  7723  recgt1i  8984  elnnnn0c  9353  elnnz1  9408  recnz  9479  eluz2b2  9737  elfzp12  10234  pfxsuff1eqwrdeq  11164  cos01gt0  12124  oddnn02np1  12241  reumodprminv  12626  sgrpidmndm  13302  elply2  15257  bj-charfundc  15858