Theorem imdistanda 725

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 724	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 196  df-an 385

This theorem is referenced by:  cfub  8954  cflm  8955  fzind  11351  uzss  11584  cau3lem  13942  supcvg  14427  eulerthlem2  15325  pgpfac1lem3  18299  iscnp4  20877  cncls2  20887  cncls  20888  cnntr  20889  1stcelcls  21074  cnpflf  21615  fclsnei  21633  cnpfcf  21655  alexsublem  21658  iscau4  22885  caussi  22903  equivcfil  22905  ismbf3d  23227  i1fmullem  23267  abelth  23999  ocsh  27526  fpwrelmap  28896  locfinreflem  29235  matunitlindf  32577  isdrngo3  32928  keridl  33001  pmapjat1  34157