Theorem imdistanda 573

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  predtrss  6240  cfub  10051  cflm  10052  fzind  12464  uzss  12651  cau3lem  15111  supcvg  15613  eulerthlem2  16528  pgpfac1lem3  19725  iscnp4  22459  cncls2  22469  cncls  22470  cnntr  22471  1stcelcls  22657  cnpflf  23197  fclsnei  23215  cnpfcf  23237  alexsublem  23240  iscau4  24488  caussi  24506  equivcfil  24508  ismbf3d  24863  i1fmullem  24903  abelth  25645  ocsh  29690  fpwrelmap  31113  locfinreflem  31835  nosupbnd1lem5  33960  matunitlindf  35819  isdrngo3  36161  keridl  36234  pmapjat1  37909