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  6328  cfub  10272  cflm  10273  fzind  12690  uzss  12875  cau3lem  15333  supcvg  15834  eulerthlem2  16750  pgpfac1lem3  20038  iscnp4  23197  cncls2  23207  cncls  23208  cnntr  23209  1stcelcls  23395  cnpflf  23935  fclsnei  23953  cnpfcf  23975  alexsublem  23978  iscau4  25237  caussi  25255  equivcfil  25257  ismbf3d  25613  i1fmullem  25653  abelth  26408  nosupbnd1lem5  27675  ocsh  31149  fpwrelmap  32572  locfinreflem  33511  matunitlindf  37161  isdrngo3  37502  keridl  37575  pmapjat1  39395