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  6281  cfub  10163  cflm  10164  fzind  12594  uzss  12778  cau3lem  15282  supcvg  15783  eulerthlem2  16713  pgpfac1lem3  20012  iscnp4  23211  cncls2  23221  cncls  23222  cnntr  23223  1stcelcls  23409  cnpflf  23949  fclsnei  23967  cnpfcf  23989  alexsublem  23992  iscau4  25239  caussi  25257  equivcfil  25259  ismbf3d  25615  i1fmullem  25655  abelth  26411  nosupbnd1lem5  27684  ocsh  31341  fpwrelmap  32793  locfinreflem  33978  matunitlindf  37790  isdrngo3  38131  keridl  38204  pmapjat1  40150  grlimpredg  48280