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  6344  cfub  10286  cflm  10287  fzind  12713  uzss  12898  cau3lem  15389  supcvg  15888  eulerthlem2  16815  pgpfac1lem3  20111  iscnp4  23286  cncls2  23296  cncls  23297  cnntr  23298  1stcelcls  23484  cnpflf  24024  fclsnei  24042  cnpfcf  24064  alexsublem  24067  iscau4  25326  caussi  25344  equivcfil  25346  ismbf3d  25702  i1fmullem  25742  abelth  26499  nosupbnd1lem5  27771  ocsh  31311  fpwrelmap  32750  locfinreflem  33800  matunitlindf  37604  isdrngo3  37945  keridl  38018  pmapjat1  39835