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  3373  difrab  3410  opthreg  4556  wessep  4578  fvelimab  5573  elfvmptrab  5612  dffo4  5665  dffo5  5666  ltaddpr  7596  recgt1i  8855  elnnnn0c  9221  elnnz1  9276  recnz  9346  eluz2b2  9603  elfzp12  10099  cos01gt0  11770  oddnn02np1  11885  reumodprminv  12253  sgrpidmndm  12821  bj-charfundc  14563