Theorem imdistanda 729

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  cfub  9109  cflm  9110  fzind  11513  uzss  11746  cau3lem  14138  supcvg  14632  eulerthlem2  15534  pgpfac1lem3  18522  iscnp4  21115  cncls2  21125  cncls  21126  cnntr  21127  1stcelcls  21312  cnpflf  21852  fclsnei  21870  cnpfcf  21892  alexsublem  21895  iscau4  23123  caussi  23141  equivcfil  23143  ismbf3d  23466  i1fmullem  23506  abelth  24240  ocsh  28270  fpwrelmap  29636  locfinreflem  30035  nosupbnd1lem5  31983  matunitlindf  33537  isdrngo3  33888  keridl  33961  pmapjat1  35457