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

Theorem imdistanda 724
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 448 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imdistand 723 1 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  cfub  8931  cflm  8932  fzind  11307  uzss  11540  cau3lem  13888  supcvg  14373  eulerthlem2  15271  pgpfac1lem3  18245  iscnp4  20819  cncls2  20829  cncls  20830  cnntr  20831  1stcelcls  21016  cnpflf  21557  fclsnei  21575  cnpfcf  21597  alexsublem  21600  iscau4  22803  caussi  22821  equivcfil  22823  ismbf3d  23144  i1fmullem  23184  abelth  23916  ocsh  27332  fpwrelmap  28702  locfinreflem  29041  matunitlindf  32373  isdrngo3  32724  keridl  32797  pmapjat1  33953
  Copyright terms: Public domain W3C validator