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  6324  cfub  10244  cflm  10245  fzind  12660  uzss  12845  cau3lem  15301  supcvg  15802  eulerthlem2  16715  pgpfac1lem3  19947  iscnp4  22767  cncls2  22777  cncls  22778  cnntr  22779  1stcelcls  22965  cnpflf  23505  fclsnei  23523  cnpfcf  23545  alexsublem  23548  iscau4  24796  caussi  24814  equivcfil  24816  ismbf3d  25171  i1fmullem  25211  abelth  25953  nosupbnd1lem5  27215  ocsh  30536  fpwrelmap  31958  locfinreflem  32820  matunitlindf  36486  isdrngo3  36827  keridl  36900  pmapjat1  38724