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  6281  cfub  10164  cflm  10165  fzind  12595  uzss  12779  cau3lem  15283  supcvg  15784  eulerthlem2  16714  pgpfac1lem3  20013  iscnp4  23212  cncls2  23222  cncls  23223  cnntr  23224  1stcelcls  23410  cnpflf  23950  fclsnei  23968  cnpfcf  23990  alexsublem  23993  iscau4  25240  caussi  25258  equivcfil  25260  ismbf3d  25616  i1fmullem  25656  abelth  26412  nosupbnd1lem5  27685  ocsh  31363  fpwrelmap  32815  locfinreflem  34010  matunitlindf  37832  isdrngo3  38173  keridl  38246  pmapjat1  40192  grlimpredg  48321