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  6275  cfub  10146  cflm  10147  fzind  12577  uzss  12761  cau3lem  15268  supcvg  15769  eulerthlem2  16699  pgpfac1lem3  19997  iscnp4  23184  cncls2  23194  cncls  23195  cnntr  23196  1stcelcls  23382  cnpflf  23922  fclsnei  23940  cnpfcf  23962  alexsublem  23965  iscau4  25212  caussi  25230  equivcfil  25232  ismbf3d  25588  i1fmullem  25628  abelth  26384  nosupbnd1lem5  27657  ocsh  31270  fpwrelmap  32723  locfinreflem  33860  matunitlindf  37664  isdrngo3  38005  keridl  38078  pmapjat1  39958  grlimpredg  48103