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  6298  cfub  10209  cflm  10210  fzind  12639  uzss  12823  cau3lem  15328  supcvg  15829  eulerthlem2  16759  pgpfac1lem3  20016  iscnp4  23157  cncls2  23167  cncls  23168  cnntr  23169  1stcelcls  23355  cnpflf  23895  fclsnei  23913  cnpfcf  23935  alexsublem  23938  iscau4  25186  caussi  25204  equivcfil  25206  ismbf3d  25562  i1fmullem  25602  abelth  26358  nosupbnd1lem5  27631  ocsh  31219  fpwrelmap  32663  locfinreflem  33837  matunitlindf  37619  isdrngo3  37960  keridl  38033  pmapjat1  39854