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

Theorem imdistanda 731
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 730 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  9263  cflm  9264  fzind  11667  uzss  11900  cau3lem  14293  supcvg  14787  eulerthlem2  15689  pgpfac1lem3  18676  iscnp4  21269  cncls2  21279  cncls  21280  cnntr  21281  1stcelcls  21466  cnpflf  22006  fclsnei  22024  cnpfcf  22046  alexsublem  22049  iscau4  23277  caussi  23295  equivcfil  23297  ismbf3d  23620  i1fmullem  23660  abelth  24394  ocsh  28451  fpwrelmap  29817  locfinreflem  30216  nosupbnd1lem5  32164  matunitlindf  33720  isdrngo3  34071  keridl  34144  pmapjat1  35642
  Copyright terms: Public domain W3C validator