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  6343  cfub  10289  cflm  10290  fzind  12716  uzss  12901  cau3lem  15393  supcvg  15892  eulerthlem2  16819  pgpfac1lem3  20097  iscnp4  23271  cncls2  23281  cncls  23282  cnntr  23283  1stcelcls  23469  cnpflf  24009  fclsnei  24027  cnpfcf  24049  alexsublem  24052  iscau4  25313  caussi  25331  equivcfil  25333  ismbf3d  25689  i1fmullem  25729  abelth  26485  nosupbnd1lem5  27757  ocsh  31302  fpwrelmap  32744  locfinreflem  33839  matunitlindf  37625  isdrngo3  37966  keridl  38039  pmapjat1  39855