Theorem imdistanda 570

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  predtrss  6330  cfub  10274  cflm  10275  fzind  12693  uzss  12878  cau3lem  15337  supcvg  15838  eulerthlem2  16754  pgpfac1lem3  20046  iscnp4  23211  cncls2  23221  cncls  23222  cnntr  23223  1stcelcls  23409  cnpflf  23949  fclsnei  23967  cnpfcf  23989  alexsublem  23992  iscau4  25251  caussi  25269  equivcfil  25271  ismbf3d  25627  i1fmullem  25667  abelth  26423  nosupbnd1lem5  27691  ocsh  31165  fpwrelmap  32597  locfinreflem  33572  matunitlindf  37222  isdrngo3  37563  keridl  37636  pmapjat1  39456