Theorem imdistanda 578

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 577	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:  predtrss  6294  cfub  10191  cflm  10192  fzind  12657  uzss  12848  cau3lem  15354  supcvg  15858  eulerthlem2  16789  pgpfac1lem3  20091  iscnp4  23292  cncls2  23302  cncls  23303  cnntr  23304  1stcelcls  23490  cnpflf  24030  fclsnei  24048  cnpfcf  24070  alexsublem  24073  iscau4  25310  caussi  25328  equivcfil  25330  ismbf3d  25685  i1fmullem  25725  abelth  26470  nosupbnd1lem5  27742  ocsh  31421  fpwrelmap  32874  locfinreflem  34081  matunitlindf  38055  isdrngo3  38396  keridl  38469  pmapjat1  40415  grlimpredg  48558