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  6290  cfub  10173  cflm  10174  fzind  12604  uzss  12788  cau3lem  15292  supcvg  15793  eulerthlem2  16723  pgpfac1lem3  20025  iscnp4  23224  cncls2  23234  cncls  23235  cnntr  23236  1stcelcls  23422  cnpflf  23962  fclsnei  23980  cnpfcf  24002  alexsublem  24005  iscau4  25252  caussi  25270  equivcfil  25272  ismbf3d  25628  i1fmullem  25668  abelth  26424  nosupbnd1lem5  27697  ocsh  31377  fpwrelmap  32829  locfinreflem  34024  matunitlindf  37898  isdrngo3  38239  keridl  38312  pmapjat1  40258  grlimpredg  48387