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

Theorem 3impdi 1237
Description: Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
Hypothesis
Ref Expression
3impdi.1  |-  ( ( ( ph  /\  ps )  /\  ( ph  /\  ch ) )  ->  th )
Assertion
Ref Expression
3impdi  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impdi
StepHypRef Expression
1 3impdi.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ( ph  /\  ch ) )  ->  th )
21anandis 803 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323impb 1147 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  oacan  6546  omcan  6567  ecovdi  6771  distrpi  8522  axltadd  8896  ccatlcan  11464  absmulgcd  12726  fh1  22197  fh2  22198  cm2j  22199  hoadddi  22383  hosubdi  22388  leopmul2i  22715  axlowdimlem14  24583  dvconstbi  27551  reccot  28228  rectan  28229  eel2131  28492  uun2131  28566  uun2131p1  28567
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  df-3an 936
  Copyright terms: Public domain W3C validator