Theorem imdistanda 571

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  predtrss  6265  cfub  10132  cflm  10133  fzind  12563  uzss  12747  cau3lem  15254  supcvg  15755  eulerthlem2  16685  pgpfac1lem3  19984  iscnp4  23171  cncls2  23181  cncls  23182  cnntr  23183  1stcelcls  23369  cnpflf  23909  fclsnei  23927  cnpfcf  23949  alexsublem  23952  iscau4  25199  caussi  25217  equivcfil  25219  ismbf3d  25575  i1fmullem  25615  abelth  26371  nosupbnd1lem5  27644  ocsh  31253  fpwrelmap  32706  locfinreflem  33843  matunitlindf  37637  isdrngo3  37978  keridl  38051  pmapjat1  39871  grlimpredg  48008