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 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

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  453  xoranor  1426  nfan1  1617  sbcof2  1863  difin  3468  difrab  3507  rabsnifsb  3776  opthreg  4701  wessep  4723  fvelimab  5756  elfvmptrab  5798  dffo4  5850  dffo5  5851  ltaddpr  7958  recgt1i  9222  elnnnn0c  9591  elnnz1  9650  recnz  9722  eluz2b2  9986  elfzp12  10489  pfxsuff1eqwrdeq  11454  cos01gt0  12513  oddnn02np1  12630  reumodprminv  13015  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemth  13264  sgrpidmndm  13716  elply2  15819  bj-charfundc  16817