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  8625  cflm  8626  fzind  10955  uzss  11098  cau3lem  13143  supcvg  13623  eulerthlem2  14164  pgpfac1lem3  16915  iscnp4  19527  cncls2  19537  cncls  19538  cnntr  19539  1stcelcls  19725  cnpflf  20234  fclsnei  20252  cnpfcf  20274  alexsublem  20276  iscau4  21450  caussi  21468  equivcfil  21470  ismbf3d  21793  i1fmullem  21833  abelth  22567  ocsh  25874  fpwrelmap  27225  isdrngo3  29963  keridl  30030  pmapjat1  34649
  Copyright terms: Public domain W3C validator