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

Theorem 3impdi 1240
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 805 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323impb 1150 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  oacan  6793  omcan  6814  ecovdi  7019  distrpi  8777  axltadd  9151  ccatlcan  11780  absmulgcd  13049  fh1  23122  fh2  23123  cm2j  23124  hoadddi  23308  hosubdi  23313  leopmul2i  23640  axlowdimlem14  25896  dvconstbi  27530  reccot  28563  rectan  28564  eel2131  28884  uun2131  28965  uun2131p1  28966
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator