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  6320  cfub  10250  cflm  10251  fzind  12719  uzss  12910  cau3lem  15442  supcvg  15945  eulerthlem2  16873  pgpfac1lem3  20206  isdrng5  20917  matunitlindf  22903  iscnp4  23488  cncls2  23498  cncls  23499  cnntr  23500  1stcelcls  23687  cnpflf  24227  fclsnei  24245  cnpfcf  24267  alexsublem  24270  iscau4  25507  caussi  25525  equivcfil  25527  ismbf3d  25882  i1fmullem  25922  abelth  26677  nosupbnd1lem5  27948  ocsh  31764  fpwrelmap  33204  locfinreflem  34350  isdrngo3  38709  keridl  38782  pmapjat1  40726  grlimpredg  48914