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  4705  wessep  4727  fvelimab  5762  elfvmptrab  5805  dffo4  5859  dffo5  5860  ltaddpr  7971  recgt1i  9237  elnnnn0c  9620  elnnz1  9679  recnz  9751  eluz2b2  10020  elfzp12  10524  pfxsuff1eqwrdeq  11494  cos01gt0  12556  oddnn02np1  12673  reumodprminv  13062  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemth  13340  sgrpidmndm  13793  elply2  15973  bj-charfundc  17051