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  1859  difin  3457  difrab  3494  rabsnifsb  3756  opthreg  4677  wessep  4699  fvelimab  5732  elfvmptrab  5772  dffo4  5824  dffo5  5825  ltaddpr  7911  recgt1i  9171  elnnnn0c  9540  elnnz1  9599  recnz  9670  eluz2b2  9934  elfzp12  10432  pfxsuff1eqwrdeq  11387  cos01gt0  12445  oddnn02np1  12562  reumodprminv  12947  sgrpidmndm  13625  elply2  15592  bj-charfundc  16570