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

Theorem 3impdi 1283
Description: Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
Hypothesis
Ref Expression
3impdi.1
Assertion
Ref Expression
3impdi

Proof of Theorem 3impdi
StepHypRef Expression
1 3impdi.1 . . 3
21anandis 830 . 2
323impb 1192 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  oacan  7216  omcan  7237  ecovdi  7438  distrpi  9297  axltadd  9679  ccatlcan  12697  absmulgcd  14185  axlowdimlem14  24258  fh1  26536  fh2  26537  cm2j  26538  hoadddi  26722  hosubdi  26727  leopmul2i  27054  dvconstbi  31239  reccot  33152  rectan  33153  eel2131  33507  uun2131  33588  uun2131p1  33589
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  df-3an 975
  Copyright terms: Public domain W3C validator