Theorem imdistani 442

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 327	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  xoranor  1367  nfan1  1552  sbcof2  1798  difin  3358  difrab  3395  opthreg  4532  wessep  4554  fvelimab  5541  elfvmptrab  5580  dffo4  5632  dffo5  5633  ltaddpr  7534  recgt1i  8789  elnnnn0c  9155  elnnz1  9210  recnz  9280  eluz2b2  9537  elfzp12  10030  cos01gt0  11699  oddnn02np1  11813  reumodprminv  12181  bj-charfundc  13650