Theorem imdistanda 724

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 448	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imdistand 723	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 195  df-an 384

This theorem is referenced by:  cfub  8931  cflm  8932  fzind  11307  uzss  11540  cau3lem  13888  supcvg  14373  eulerthlem2  15271  pgpfac1lem3  18245  iscnp4  20819  cncls2  20829  cncls  20830  cnntr  20831  1stcelcls  21016  cnpflf  21557  fclsnei  21575  cnpfcf  21597  alexsublem  21600  iscau4  22803  caussi  22821  equivcfil  22823  ismbf3d  23144  i1fmullem  23184  abelth  23916  ocsh  27332  fpwrelmap  28702  locfinreflem  29041  matunitlindf  32373  isdrngo3  32724  keridl  32797  pmapjat1  33953