Theorem imdistanda 575

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  cfub  9660  cflm  9661  fzind  12068  uzss  12253  cau3lem  14706  supcvg  15203  eulerthlem2  16109  pgpfac1lem3  19192  mhpvarcl  20798  iscnp4  21868  cncls2  21878  cncls  21879  cnntr  21880  1stcelcls  22066  cnpflf  22606  fclsnei  22624  cnpfcf  22646  alexsublem  22649  iscau4  23883  caussi  23901  equivcfil  23903  ismbf3d  24258  i1fmullem  24298  abelth  25036  ocsh  29066  fpwrelmap  30495  locfinreflem  31193  nosupbnd1lem5  33325  matunitlindf  35055  isdrngo3  35397  keridl  35470  pmapjat1  37149