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  6287  cfub  10171  cflm  10172  fzind  12627  uzss  12811  cau3lem  15317  supcvg  15821  eulerthlem2  16752  pgpfac1lem3  20054  iscnp4  23228  cncls2  23238  cncls  23239  cnntr  23240  1stcelcls  23426  cnpflf  23966  fclsnei  23984  cnpfcf  24006  alexsublem  24009  iscau4  25246  caussi  25264  equivcfil  25266  ismbf3d  25621  i1fmullem  25661  abelth  26406  nosupbnd1lem5  27676  ocsh  31354  fpwrelmap  32806  locfinreflem  33984  matunitlindf  37939  isdrngo3  38280  keridl  38353  pmapjat1  40299  grlimpredg  48468