Theorem imdistani 449

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 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  syldanl  453  xoranor  1426  nfan1  1617  sbcof2  1863  difin  3468  difrab  3507  rabsnifsb  3777  opthreg  4703  wessep  4725  fvelimab  5759  elfvmptrab  5802  dffo4  5856  dffo5  5857  ltaddpr  7964  recgt1i  9229  elnnnn0c  9610  elnnz1  9669  recnz  9741  eluz2b2  10005  elfzp12  10508  pfxsuff1eqwrdeq  11473  cos01gt0  12532  oddnn02np1  12649  reumodprminv  13034  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemth  13283  sgrpidmndm  13735  elply2  15838  bj-charfundc  16846