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  6562  omcan  6583  ecovdi  6787  distrpi  8538  axltadd  8912  ccatlcan  11480  absmulgcd  12742  fh1  22213  fh2  22214  cm2j  22215  hoadddi  22399  hosubdi  22404  leopmul2i  22731  axlowdimlem14  24655  dvconstbi  27654  reccot  28482  rectan  28483  eel2131  28799  uun2131  28880  uun2131p1  28881
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