Theorem imdistanda 582

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

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

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 402

This theorem is used by:  predtrss  6343  cfub  10353  cflm  10354  fzind  12824  uzss  13015  cau3lem  15551  supcvg  16054  eulerthlem2  16988  pgpfac1lem3  20323  isdrng5  21038  matunitlindf  23026  iscnp4  23611  cncls2  23621  cncls  23622  cnntr  23623  1stcelcls  23810  cnpflf  24350  fclsnei  24368  cnpfcf  24390  alexsublem  24393  iscau4  25630  caussi  25648  equivcfil  25650  ismbf3d  26005  i1fmullem  26045  abelth  26798  nosupbnd1lem5  28099  ocsh  31915  fpwrelmap  33395  locfinreflem  34542  mpofvd  35797  isdrngo3  39085  keridl  39158  pmapjat1  41102  grlimpredg  49301