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  1388  nfan1  1578  sbcof2  1824  difin  3400  difrab  3437  opthreg  4592  wessep  4614  fvelimab  5617  elfvmptrab  5657  dffo4  5710  dffo5  5711  ltaddpr  7664  recgt1i  8925  elnnnn0c  9294  elnnz1  9349  recnz  9419  eluz2b2  9677  elfzp12  10174  cos01gt0  11928  oddnn02np1  12045  reumodprminv  12422  sgrpidmndm  13061  elply2  14971  bj-charfundc  15454