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

Theorem imdistanda 693
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 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imdistand 692 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ps 
/\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  cfub  8430  cflm  8431  fzind  10752  uzss  10893  cau3lem  12854  supcvg  13330  eulerthlem2  13869  pgpfac1lem3  16590  iscnp4  18879  cncls2  18889  cncls  18890  cnntr  18891  1stcelcls  19077  cnpflf  19586  fclsnei  19604  cnpfcf  19626  alexsublem  19628  iscau4  20802  caussi  20820  equivcfil  20822  ismbf3d  21144  i1fmullem  21184  abelth  21918  ocsh  24698  fpwrelmap  26045  isdrngo3  28777  keridl  28844  pmapjat1  33509
  Copyright terms: Public domain W3C validator