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  9671  cflm  9672  fzind  12081  uzss  12266  cau3lem  14714  supcvg  15211  eulerthlem2  16119  pgpfac1lem3  19199  iscnp4  21871  cncls2  21881  cncls  21882  cnntr  21883  1stcelcls  22069  cnpflf  22609  fclsnei  22627  cnpfcf  22649  alexsublem  22652  iscau4  23882  caussi  23900  equivcfil  23902  ismbf3d  24255  i1fmullem  24295  abelth  25029  ocsh  29060  fpwrelmap  30469  locfinreflem  31104  nosupbnd1lem5  33212  matunitlindf  34905  isdrngo3  35252  keridl  35325  pmapjat1  37004