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  6278  cfub  10160  cflm  10161  fzind  12591  uzss  12775  cau3lem  15279  supcvg  15780  eulerthlem2  16710  pgpfac1lem3  20012  iscnp4  23206  cncls2  23216  cncls  23217  cnntr  23218  1stcelcls  23404  cnpflf  23944  fclsnei  23962  cnpfcf  23984  alexsublem  23987  iscau4  25224  caussi  25242  equivcfil  25244  ismbf3d  25599  i1fmullem  25639  abelth  26391  nosupbnd1lem5  27664  ocsh  31343  fpwrelmap  32795  locfinreflem  33990  matunitlindf  37930  isdrngo3  38271  keridl  38344  pmapjat1  40290  grlimpredg  48432