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  6274  cfub  10162  cflm  10163  fzind  12592  uzss  12776  cau3lem  15280  supcvg  15781  eulerthlem2  16711  pgpfac1lem3  19976  iscnp4  23166  cncls2  23176  cncls  23177  cnntr  23178  1stcelcls  23364  cnpflf  23904  fclsnei  23922  cnpfcf  23944  alexsublem  23947  iscau4  25195  caussi  25213  equivcfil  25215  ismbf3d  25571  i1fmullem  25611  abelth  26367  nosupbnd1lem5  27640  ocsh  31245  fpwrelmap  32689  locfinreflem  33806  matunitlindf  37597  isdrngo3  37938  keridl  38011  pmapjat1  39832