Theorem imdistanda 572

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  predtrss  6281  cfub  10194  cflm  10195  fzind  12610  uzss  12795  cau3lem  15251  supcvg  15752  eulerthlem2  16665  pgpfac1lem3  19870  iscnp4  22651  cncls2  22661  cncls  22662  cnntr  22663  1stcelcls  22849  cnpflf  23389  fclsnei  23407  cnpfcf  23429  alexsublem  23432  iscau4  24680  caussi  24698  equivcfil  24700  ismbf3d  25055  i1fmullem  25095  abelth  25837  nosupbnd1lem5  27097  ocsh  30288  fpwrelmap  31718  locfinreflem  32510  matunitlindf  36149  isdrngo3  36491  keridl  36564  pmapjat1  38389