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  3462  difrab  3499  rabsnifsb  3762  opthreg  4683  wessep  4705  fvelimab  5738  elfvmptrab  5778  dffo4  5830  dffo5  5831  ltaddpr  7928  recgt1i  9192  elnnnn0c  9561  elnnz1  9620  recnz  9692  eluz2b2  9956  elfzp12  10458  pfxsuff1eqwrdeq  11419  cos01gt0  12478  oddnn02np1  12595  reumodprminv  12980  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemth  13229  sgrpidmndm  13685  elply2  15730  bj-charfundc  16718