Theorem imdistanda 731

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 730	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  9263  cflm  9264  fzind  11667  uzss  11900  cau3lem  14293  supcvg  14787  eulerthlem2  15689  pgpfac1lem3  18676  iscnp4  21269  cncls2  21279  cncls  21280  cnntr  21281  1stcelcls  21466  cnpflf  22006  fclsnei  22024  cnpfcf  22046  alexsublem  22049  iscau4  23277  caussi  23295  equivcfil  23297  ismbf3d  23620  i1fmullem  23660  abelth  24394  ocsh  28451  fpwrelmap  29817  locfinreflem  30216  nosupbnd1lem5  32164  matunitlindf  33720  isdrngo3  34071  keridl  34144  pmapjat1  35642