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

Theorem imdistanda 691
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 432 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imdistand 690 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ps 
/\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  cfub  8661  cflm  8662  fzind  11001  uzss  11147  cau3lem  13336  supcvg  13819  eulerthlem2  14521  pgpfac1lem3  17448  iscnp4  20057  cncls2  20067  cncls  20068  cnntr  20069  1stcelcls  20254  cnpflf  20794  fclsnei  20812  cnpfcf  20834  alexsublem  20836  iscau4  22010  caussi  22028  equivcfil  22030  ismbf3d  22353  i1fmullem  22393  abelth  23128  ocsh  26615  fpwrelmap  28003  locfinreflem  28296  isdrngo3  31644  keridl  31711  pmapjat1  32870
  Copyright terms: Public domain W3C validator