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  6322  cfub  10271  cflm  10272  fzind  12699  uzss  12883  cau3lem  15375  supcvg  15874  eulerthlem2  16801  pgpfac1lem3  20065  iscnp4  23217  cncls2  23227  cncls  23228  cnntr  23229  1stcelcls  23415  cnpflf  23955  fclsnei  23973  cnpfcf  23995  alexsublem  23998  iscau4  25249  caussi  25267  equivcfil  25269  ismbf3d  25625  i1fmullem  25665  abelth  26421  nosupbnd1lem5  27693  ocsh  31230  fpwrelmap  32679  locfinreflem  33798  matunitlindf  37584  isdrngo3  37925  keridl  37998  pmapjat1  39814