Theorem imdistanda 571

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  predtrss  6354  cfub  10318  cflm  10319  fzind  12741  uzss  12926  cau3lem  15403  supcvg  15904  eulerthlem2  16829  pgpfac1lem3  20121  iscnp4  23292  cncls2  23302  cncls  23303  cnntr  23304  1stcelcls  23490  cnpflf  24030  fclsnei  24048  cnpfcf  24070  alexsublem  24073  iscau4  25332  caussi  25350  equivcfil  25352  ismbf3d  25708  i1fmullem  25748  abelth  26503  nosupbnd1lem5  27775  ocsh  31315  fpwrelmap  32747  locfinreflem  33786  matunitlindf  37578  isdrngo3  37919  keridl  37992  pmapjat1  39810