Theorem imdistanda 582

Description: Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
imdistanda.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
imdistanda	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))

Proof of Theorem imdistanda

Step	Hyp	Ref	Expression
1		imdistanda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 418	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imdistand 581	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  predtrss  6325  cfub  10326  cflm  10327  fzind  12797  uzss  12988  cau3lem  15522  supcvg  16025  eulerthlem2  16959  pgpfac1lem3  20293  isdrng5  21008  matunitlindf  22996  iscnp4  23581  cncls2  23591  cncls  23592  cnntr  23593  1stcelcls  23780  cnpflf  24320  fclsnei  24338  cnpfcf  24360  alexsublem  24363  iscau4  25600  caussi  25618  equivcfil  25620  ismbf3d  25975  i1fmullem  26015  abelth  26768  nosupbnd1lem5  28069  ocsh  31885  fpwrelmap  33367  locfinreflem  34514  isdrngo3  38936  keridl  39009  pmapjat1  40953  grlimpredg  49139