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  1377  nfan1  1564  sbcof2  1810  difin  3372  difrab  3409  opthreg  4555  wessep  4577  fvelimab  5572  elfvmptrab  5611  dffo4  5664  dffo5  5665  ltaddpr  7595  recgt1i  8853  elnnnn0c  9219  elnnz1  9274  recnz  9344  eluz2b2  9601  elfzp12  10096  cos01gt0  11765  oddnn02np1  11879  reumodprminv  12247  sgrpidmndm  12775  bj-charfundc  14442