Theorem imdistanda 579

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  predtrss  6309  cfub  10216  cflm  10217  fzind  12681  uzss  12872  cau3lem  15392  supcvg  15896  eulerthlem2  16827  pgpfac1lem3  20129  iscnp4  23330  cncls2  23340  cncls  23341  cnntr  23342  1stcelcls  23528  cnpflf  24068  fclsnei  24086  cnpfcf  24108  alexsublem  24111  iscau4  25348  caussi  25366  equivcfil  25368  ismbf3d  25723  i1fmullem  25763  abelth  26511  nosupbnd1lem5  27783  ocsh  31493  fpwrelmap  32941  locfinreflem  34139  matunitlindf  38122  isdrngo3  38463  keridl  38536  pmapjat1  40482  grlimpredg  48611