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

Theorem 3imp1 1209
 Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3imp1.1
Assertion
Ref Expression
3imp1

Proof of Theorem 3imp1
StepHypRef Expression
1 3imp1.1 . . 3
213imp 1190 . 2
32imp 429 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  /\w3a 973 This theorem is referenced by:  reupick2  3783  indcardi  8443  expcan  12218  ltexp2  12219  leexp1a  12224  expnbnd  12295  xrsdsreclblem  18464  matecl  18927  scmateALT  19014  riinopn  19417  neindisj2  19624  filufint  20421  tsmsxp  20657  spthonepeq  24589  usg2wlkeq  24708  rusgraprop4  24944  vdn0frgrav2  25023  vdn1frgrav2  25025  usgreghash2spot  25069  zerdivemp1  25436  homco1  26720  homulass  26721  hoadddir  26723  relexpindlem  29062  rtrclreclem.min  29070  mblfinlem3  30053  zerdivemp1x  30358  eluzge0nn0  32329  athgt  35180  psubspi  35471  paddasslem14  35557 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