Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imdistanda Structured version   Visualization version   GIF version

Theorem imdistanda 729
 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
StepHypRef Expression
1 imdistanda.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 449 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imdistand 728 1 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  cfub  9109  cflm  9110  fzind  11513  uzss  11746  cau3lem  14138  supcvg  14632  eulerthlem2  15534  pgpfac1lem3  18522  iscnp4  21115  cncls2  21125  cncls  21126  cnntr  21127  1stcelcls  21312  cnpflf  21852  fclsnei  21870  cnpfcf  21892  alexsublem  21895  iscau4  23123  caussi  23141  equivcfil  23143  ismbf3d  23466  i1fmullem  23506  abelth  24240  ocsh  28270  fpwrelmap  29636  locfinreflem  30035  nosupbnd1lem5  31983  matunitlindf  33537  isdrngo3  33888  keridl  33961  pmapjat1  35457
 Copyright terms: Public domain W3C validator