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

Theorem imdistanda 675
Description: Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
imdistanda.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
imdistanda  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ps 
/\  th ) ) )

Proof of Theorem imdistanda
StepHypRef Expression
1 imdistanda.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 424 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imdistand 674 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ps 
/\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  cfub  8129  cflm  8130  fzind  10368  uzss  10506  cau3lem  12158  supcvg  12635  eulerthlem2  13171  pgpfac1lem3  15635  iscnp4  17327  cncls2  17337  cncls  17338  cnntr  17339  1stcelcls  17524  cnpflf  18033  fclsnei  18051  cnpfcf  18073  alexsublem  18075  iscau4  19232  caussi  19250  equivcfil  19252  ismbf3d  19546  i1fmullem  19586  abelth  20357  ocsh  22785  isdrngo3  26575  keridl  26642  pmapjat1  30650
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator