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  6324  cfub  10253  cflm  10254  fzind  12722  uzss  12913  cau3lem  15444  supcvg  15947  eulerthlem2  16877  pgpfac1lem3  20207  isdrng5  20918  matunitlindf  22904  iscnp4  23489  cncls2  23499  cncls  23500  cnntr  23501  1stcelcls  23688  cnpflf  24228  fclsnei  24246  cnpfcf  24268  alexsublem  24271  iscau4  25508  caussi  25526  equivcfil  25528  ismbf3d  25883  i1fmullem  25923  abelth  26674  nosupbnd1lem5  27946  ocsh  31750  fpwrelmap  33191  locfinreflem  34337  isdrngo3  38696  keridl  38769  pmapjat1  40713  grlimpredg  48901