Theorem imdistanda 582

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  predtrss  6314  cfub  10297  cflm  10298  fzind  12766  uzss  12957  cau3lem  15489  supcvg  15992  eulerthlem2  16920  pgpfac1lem3  20254  isdrng5  20969  matunitlindf  22957  iscnp4  23542  cncls2  23552  cncls  23553  cnntr  23554  1stcelcls  23741  cnpflf  24281  fclsnei  24299  cnpfcf  24321  alexsublem  24324  iscau4  25561  caussi  25579  equivcfil  25581  ismbf3d  25936  i1fmullem  25976  abelth  26731  nosupbnd1lem5  28002  ocsh  31818  fpwrelmap  33258  locfinreflem  34405  isdrngo3  38813  keridl  38886  pmapjat1  40830  grlimpredg  49018