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

Theorem imdistanda 674
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 423 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imdistand 673 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ps 
/\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  cfub  7891  cflm  7892  fzind  10126  uzss  10264  cau3lem  11854  supcvg  12330  eulerthlem2  12866  pgpfac1lem3  15328  cncls2  17018  cncls  17019  cnntr  17020  1stcelcls  17203  cnpflf  17712  fclsnei  17730  cnpfcf  17752  alexsublem  17754  iscau4  18721  caussi  18739  equivcfil  18741  ismbf3d  19025  i1fmullem  19065  abelth  19833  ocsh  21878  iscnp4  25666  islimrs3  25684  islimrs4  25685  imdistandaOLD  26440  isdrngo3  26693  keridl  26760  pmapjat1  30664
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 177  df-an 360
  Copyright terms: Public domain W3C validator