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  6275  cfub  10160  cflm  10161  fzind  12616  uzss  12800  cau3lem  15306  supcvg  15810  eulerthlem2  16741  pgpfac1lem3  20043  iscnp4  23216  cncls2  23226  cncls  23227  cnntr  23228  1stcelcls  23414  cnpflf  23954  fclsnei  23972  cnpfcf  23994  alexsublem  23997  iscau4  25234  caussi  25252  equivcfil  25254  ismbf3d  25609  i1fmullem  25649  abelth  26394  nosupbnd1lem5  27664  ocsh  31342  fpwrelmap  32794  locfinreflem  33972  matunitlindf  37927  isdrngo3  38268  keridl  38341  pmapjat1  40287  grlimpredg  48462