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

Step	Hyp	Ref	Expression
1		3imp1.1	. . 3
2	1	3imp 1190	. 2
3	2	imp 429	1

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