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  6322  cfub  10246  cflm  10247  fzind  12664  uzss  12849  cau3lem  15305  supcvg  15806  eulerthlem2  16719  pgpfac1lem3  19988  iscnp4  22987  cncls2  22997  cncls  22998  cnntr  22999  1stcelcls  23185  cnpflf  23725  fclsnei  23743  cnpfcf  23765  alexsublem  23768  iscau4  25027  caussi  25045  equivcfil  25047  ismbf3d  25403  i1fmullem  25443  abelth  26189  nosupbnd1lem5  27451  ocsh  30803  fpwrelmap  32225  locfinreflem  33118  matunitlindf  36789  isdrngo3  37130  keridl  37203  pmapjat1  39027