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

Theorem imdistanda 575
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 416 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imdistand 574 1 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  predtrss  6197  cfub  9887  cflm  9888  fzind  12299  uzss  12485  cau3lem  14942  supcvg  15444  eulerthlem2  16359  pgpfac1lem3  19488  iscnp4  22184  cncls2  22194  cncls  22195  cnntr  22196  1stcelcls  22382  cnpflf  22922  fclsnei  22940  cnpfcf  22962  alexsublem  22965  iscau4  24200  caussi  24218  equivcfil  24220  ismbf3d  24575  i1fmullem  24615  abelth  25357  ocsh  29388  fpwrelmap  30812  locfinreflem  31528  nosupbnd1lem5  33678  matunitlindf  35538  isdrngo3  35880  keridl  35953  pmapjat1  37630
  Copyright terms: Public domain W3C validator