Theorem imdistanda 581

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  predtrss  6323  cfub  10231  cflm  10232  fzind  12693  uzss  12884  cau3lem  15405  supcvg  15909  eulerthlem2  16840  pgpfac1lem3  20148  iscnp4  23399  cncls2  23409  cncls  23410  cnntr  23411  1stcelcls  23597  cnpflf  24137  fclsnei  24155  cnpfcf  24177  alexsublem  24180  iscau4  25417  caussi  25435  equivcfil  25437  ismbf3d  25792  i1fmullem  25832  abelth  26580  nosupbnd1lem5  27852  ocsh  31601  fpwrelmap  33044  locfinreflem  34196  matunitlindf  38213  isdrngo3  38554  keridl  38627  pmapjat1  40573  grlimpredg  48708