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

Theorem 3exp2 1214
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 434 . 2
323expd 1213 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3anassrs  1218  pm2.61da3ne  2777  po2nr  4818  fliftfund  6211  frfi  7785  fin33i  8770  axdc3lem4  8854  iscatd  15070  isfuncd  15234  isposd  15585  pospropd  15764  imasmnd2  15957  grpinveu  16084  grpid  16085  imasgrp2  16185  dmdprdd  17030  pgpfac1lem5  17130  imasring  17268  islmodd  17518  lmodvsghm  17571  islssd  17582  islmhm2  17684  psrbaglefi  18023  psrbaglefiOLD  18024  mulgghm2  18531  mulgghm2OLD  18534  isphld  18689  riinopn  19417  ordtbaslem  19689  subbascn  19755  haust1  19853  isnrm2  19859  isnrm3  19860  lmmo  19881  nllyidm  19990  tx1stc  20151  filin  20355  filtop  20356  isfil2  20357  infil  20364  fgfil  20376  isufil2  20409  ufileu  20420  filufint  20421  flimopn  20476  flimrest  20484  isxmetd  20829  met2ndc  21026  icccmplem2  21328  lmmbr  21697  cfil3i  21708  equivcfil  21738  bcthlem5  21767  volfiniun  21957  dvidlem  22319  ulmdvlem3  22797  ax5seg  24241  axcontlem4  24270  axcont  24279  grporcan  25223  grpoinveu  25224  grpoid  25225  grpoasscan1  25239  cvxpcon  28687  cvxscon  28688  mclsax  28929  mclsppslem  28943  predpo  29264  broutsideof2  29772  nn0prpwlem  30140  fgmin  30188  cntotbnd  30292  heiborlem6  30312  heiborlem10  30316  rngonegmn1l  30352  rngonegmn1r  30353  rngoneglmul  30354  rngonegrmul  30355  crngm23  30399  prnc  30464  pridlc3  30470  dmncan1  30473  lsmsat  34733  eqlkr  34824  llncmp  35246  2at0mat0  35249  llncvrlpln  35282  lplncmp  35286  lplnexllnN  35288  lplncvrlvol  35340  lvolcmp  35341  linepsubN  35476  pmapsub  35492  paddasslem16  35559  pmodlem2  35571  lhp2lt  35725  ltrneq2  35872  cdlemf2  36288  cdlemk34  36636  cdlemn11pre  36937  dihord2pre  36952
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