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  6295  cfub  10202  cflm  10203  fzind  12632  uzss  12816  cau3lem  15321  supcvg  15822  eulerthlem2  16752  pgpfac1lem3  20009  iscnp4  23150  cncls2  23160  cncls  23161  cnntr  23162  1stcelcls  23348  cnpflf  23888  fclsnei  23906  cnpfcf  23928  alexsublem  23931  iscau4  25179  caussi  25197  equivcfil  25199  ismbf3d  25555  i1fmullem  25595  abelth  26351  nosupbnd1lem5  27624  ocsh  31212  fpwrelmap  32656  locfinreflem  33830  matunitlindf  37612  isdrngo3  37953  keridl  38026  pmapjat1  39847