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  6322  cfub  10264  cflm  10265  fzind  12682  uzss  12867  cau3lem  15325  supcvg  15826  eulerthlem2  16742  pgpfac1lem3  20025  iscnp4  23154  cncls2  23164  cncls  23165  cnntr  23166  1stcelcls  23352  cnpflf  23892  fclsnei  23910  cnpfcf  23932  alexsublem  23935  iscau4  25194  caussi  25212  equivcfil  25214  ismbf3d  25570  i1fmullem  25610  abelth  26365  nosupbnd1lem5  27632  ocsh  31080  fpwrelmap  32499  locfinreflem  33377  matunitlindf  37026  isdrngo3  37367  keridl  37440  pmapjat1  39263