Theorem imdistanda 574

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  cfub  9674  cflm  9675  fzind  12083  uzss  12268  cau3lem  14717  supcvg  15214  eulerthlem2  16122  pgpfac1lem3  19202  iscnp4  21874  cncls2  21884  cncls  21885  cnntr  21886  1stcelcls  22072  cnpflf  22612  fclsnei  22630  cnpfcf  22652  alexsublem  22655  iscau4  23885  caussi  23903  equivcfil  23905  ismbf3d  24258  i1fmullem  24298  abelth  25032  ocsh  29063  fpwrelmap  30472  locfinreflem  31108  nosupbnd1lem5  33216  matunitlindf  34894  isdrngo3  35241  keridl  35314  pmapjat1  36993