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

Theorem 3exp2 1190
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3exp2.1
Assertion
Ref Expression
3exp2

Proof of Theorem 3exp2
StepHypRef Expression
1 3exp2.1 . . 3
21ex 427 . 2
323expd 1189 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  /\w3a 950
This theorem is referenced by:  3anassrs  1194  po2nr  4625  fliftfund  5974  frfi  7516  fin33i  8485  axdc3lem4  8569  iscatd  14551  isfuncd  14715  isposd  15065  pospropd  15244  imasmnd2  15398  grpinveu  15509  grpid  15510  imasgrp2  15607  dmdprdd  16369  pgpfac1lem5  16446  imasrng  16535  islmodd  16767  lmodvsghm  16818  islssd  16826  islmhm2  16928  psrbaglefi  17257  mulgghm2  17633  mulgghm2OLD  17636  isphld  17791  riinopn  18225  ordtbaslem  18496  subbascn  18562  haust1  18660  isnrm2  18666  isnrm3  18667  lmmo  18688  nllyidm  18797  tx1stc  18927  filin  19131  filtop  19132  isfil2  19133  infil  19140  fgfil  19152  isufil2  19185  ufileu  19196  filufint  19197  flimopn  19252  flimrest  19260  isxmetd  19601  met2ndc  19798  icccmplem2  20100  lmmbr  20469  cfil3i  20480  equivcfil  20510  bcthlem5  20539  volfiniun  20728  dvidlem  21090  ulmdvlem3  21608  ax5seg  22863  axcontlem4  22892  axcont  22901  grporcan  23387  grpoinveu  23388  grpoid  23389  grpoasscan1  23403  cvxpcon  26834  cvxscon  26835  predpo  27347  broutsideof2  27855  nn0prpwlem  28188  fgmin  28262  cntotbnd  28366  heiborlem6  28386  heiborlem10  28390  rngonegmn1l  28426  rngonegmn1r  28427  rngoneglmul  28428  rngonegrmul  28429  crngm23  28473  prnc  28538  pridlc3  28544  dmncan1  28547  lsmsat  32090  eqlkr  32181  llncmp  32603  2at0mat0  32606  llncvrlpln  32639  lplncmp  32643  lplnexllnN  32645  lplncvrlvol  32697  lvolcmp  32698  linepsubN  32833  pmapsub  32849  paddasslem16  32916  pmodlem2  32928  lhp2lt  33082  ltrneq2  33229  cdlemf2  33643  cdlemk34  33991  cdlemn11pre  34292  dihord2pre  34307
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 179  df-an 364  df-3an 952
  Copyright terms: Public domain W3C validator