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  7875  cflm  7876  fzind  10110  uzss  10248  cau3lem  11838  supcvg  12314  eulerthlem2  12850  pgpfac1lem3  15312  cncls2  17002  cncls  17003  cnntr  17004  1stcelcls  17187  cnpflf  17696  fclsnei  17714  cnpfcf  17736  alexsublem  17738  iscau4  18705  caussi  18723  equivcfil  18725  ismbf3d  19009  i1fmullem  19049  abelth  19817  ocsh  21862  iscnp4  25563  islimrs3  25581  islimrs4  25582  imdistandaOLD  26337  isdrngo3  26590  keridl  26657  pmapjat1  30042
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