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

Theorem con3dimp 441
 Description: Variant of con3d 133 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
con3dimp.1
Assertion
Ref Expression
con3dimp

Proof of Theorem con3dimp
StepHypRef Expression
1 con3dimp.1 . . 3
21con3d 133 . 2
32imp 429 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  /\wa 369 This theorem is referenced by:  nelneq  2574  nelneq2  2575  nelss  3562  dtru  4643  sofld  5460  card2inf  8002  gchen1  9024  gchen2  9025  bcpasc  12399  fiinfnf1o  12423  hashfn  12443  swrdvalodm2  12664  swrdvalodm  12665  swrdccat  12718  pcprod  14414  lubval  15614  glbval  15627  mplmonmul  18126  regr1lem  20240  blcld  21008  stdbdxmet  21018  itgss  22218  isosctrlem2  23153  isppw2  23389  dchrelbas3  23513  lgsdir  23605  rplogsum  23712  nb3graprlem2  24452  orngsqr  27794  qqhval2lem  27962  qqhf  27967  esumpinfval  28079  isfldidl  30465  jm2.23  30938  cncfiooicclem1  31696  fourierdlem81  31970  2f1fvneq  32307  bj-dtru  34383  lssat  34741  paddasslem1  35544  lcfrlem21  37290  hdmap10lem  37569  hdmap11lem2  37572 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
 Copyright terms: Public domain W3C validator