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  6311  cfub  10263  cflm  10264  fzind  12691  uzss  12875  cau3lem  15373  supcvg  15872  eulerthlem2  16801  pgpfac1lem3  20060  iscnp4  23201  cncls2  23211  cncls  23212  cnntr  23213  1stcelcls  23399  cnpflf  23939  fclsnei  23957  cnpfcf  23979  alexsublem  23982  iscau4  25231  caussi  25249  equivcfil  25251  ismbf3d  25607  i1fmullem  25647  abelth  26403  nosupbnd1lem5  27676  ocsh  31264  fpwrelmap  32710  locfinreflem  33871  matunitlindf  37642  isdrngo3  37983  keridl  38056  pmapjat1  39872