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

Theorem imdistanda 572
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 413 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imdistand 571 1 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  cfub  9660  cflm  9661  fzind  12069  uzss  12254  cau3lem  14704  supcvg  15201  eulerthlem2  16109  pgpfac1lem3  19130  iscnp4  21801  cncls2  21811  cncls  21812  cnntr  21813  1stcelcls  21999  cnpflf  22539  fclsnei  22557  cnpfcf  22579  alexsublem  22582  iscau4  23811  caussi  23829  equivcfil  23831  ismbf3d  24184  i1fmullem  24224  abelth  24958  ocsh  28988  fpwrelmap  30396  locfinreflem  31004  nosupbnd1lem5  33110  matunitlindf  34772  isdrngo3  35120  keridl  35193  pmapjat1  36871
  Copyright terms: Public domain W3C validator