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  1388  nfan1  1578  sbcof2  1824  difin  3401  difrab  3438  opthreg  4593  wessep  4615  fvelimab  5620  elfvmptrab  5660  dffo4  5713  dffo5  5714  ltaddpr  7683  recgt1i  8944  elnnnn0c  9313  elnnz1  9368  recnz  9438  eluz2b2  9696  elfzp12  10193  cos01gt0  11947  oddnn02np1  12064  reumodprminv  12449  sgrpidmndm  13124  elply2  15079  bj-charfundc  15562