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:  cfub  9648  cflm  9649  fzind  12058  uzss  12243  cau3lem  14693  supcvg  15190  eulerthlem2  16096  pgpfac1lem3  19177  iscnp4  21846  cncls2  21856  cncls  21857  cnntr  21858  1stcelcls  22044  cnpflf  22584  fclsnei  22602  cnpfcf  22624  alexsublem  22627  iscau4  23861  caussi  23879  equivcfil  23881  ismbf3d  24236  i1fmullem  24276  abelth  25014  ocsh  29044  fpwrelmap  30455  locfinreflem  31114  nosupbnd1lem5  33219  matunitlindf  34935  isdrngo3  35277  keridl  35350  pmapjat1  37029
  Copyright terms: Public domain W3C validator