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

This theorem is referenced by:  predtrss  6222  cfub  9989  cflm  9990  fzind  12401  uzss  12587  cau3lem  15047  supcvg  15549  eulerthlem2  16464  pgpfac1lem3  19661  iscnp4  22395  cncls2  22405  cncls  22406  cnntr  22407  1stcelcls  22593  cnpflf  23133  fclsnei  23151  cnpfcf  23173  alexsublem  23176  iscau4  24424  caussi  24442  equivcfil  24444  ismbf3d  24799  i1fmullem  24839  abelth  25581  ocsh  29624  fpwrelmap  31047  locfinreflem  31769  nosupbnd1lem5  33894  matunitlindf  35754  isdrngo3  36096  keridl  36169  pmapjat1  37846