Theorem imdistanda 581

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  predtrss  6323  cfub  10238  cflm  10239  fzind  12700  uzss  12891  cau3lem  15413  supcvg  15917  eulerthlem2  16847  pgpfac1lem3  20155  isdrng5  20865  iscnp4  23431  cncls2  23441  cncls  23442  cnntr  23443  1stcelcls  23629  cnpflf  24169  fclsnei  24187  cnpfcf  24209  alexsublem  24212  iscau4  25449  caussi  25467  equivcfil  25469  ismbf3d  25824  i1fmullem  25864  abelth  26615  nosupbnd1lem5  27887  ocsh  31646  fpwrelmap  33089  locfinreflem  34239  matunitlindf  38297  isdrngo3  38638  keridl  38711  pmapjat1  40655  grlimpredg  48791