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

Theorem 3exp2 1169
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3exp2.1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
Assertion
Ref Expression
3exp2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem 3exp2
StepHypRef Expression
1 3exp2.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
21ex 423 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
323expd 1168 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anassrs  1173  ralrimivvva  2636  euotd  4267  po2nr  4327  fliftfund  5812  frfi  7102  fin33i  7995  axdc3lem4  8079  iscatd  13575  isfuncd  13739  isposd  14089  joinle  14127  pospropd  14238  imasmnd2  14409  grpinveu  14516  grpid  14517  imasgrp2  14610  dmdprdd  15237  pgpfac1lem5  15314  imasrng  15402  islmodd  15633  lmodvsdi1OLD  15651  lmodvsdi2OLD  15653  lmodvsassOLD  15655  lmodvsghm  15686  islssd  15693  islmhm2  15795  psrbaglefi  16118  mulgghm2  16459  isphld  16558  riinopn  16654  ordtbaslem  16918  subbascn  16984  haust1  17080  isnrm2  17086  isnrm3  17087  lmmo  17108  nllyidm  17215  tx1stc  17344  filin  17549  filtop  17550  isfil2  17551  infil  17558  fgfil  17570  isufil2  17603  ufileu  17614  filufint  17615  flimopn  17670  flimrest  17678  isxmetd  17891  met2ndc  18069  icccmplem2  18328  lmmbr  18684  cfil3i  18695  equivcfil  18725  bcthlem5  18750  volfiniun  18904  dvidlem  19265  ulmdvlem3  19779  grporcan  20888  grpoinveu  20889  grpoid  20890  grpoasscan1  20904  cvxpcon  23773  cvxscon  23774  predpo  24184  ax5seg  24566  axcontlem4  24595  axcont  24604  broutsideof2  24745  trooo  25394  cmpltr2  25407  cmperltr  25409  negveud  25668  nn0prpwlem  26238  fgmin  26319  cntotbnd  26520  heiborlem6  26540  heiborlem10  26544  rngonegmn1l  26580  rngonegmn1r  26581  rngoneglmul  26582  rngonegrmul  26583  crngm23  26627  prnc  26692  pridlc3  26698  dmncan1  26701  lsmsat  29198  eqlkr  29289  llncmp  29711  2at0mat0  29714  llncvrlpln  29747  lplncmp  29751  lplnexllnN  29753  lplncvrlvol  29805  lvolcmp  29806  linepsubN  29941  pmapsub  29957  paddasslem16  30024  pmodlem2  30036  lhp2lt  30190  ltrneq2  30337  cdlemf2  30751  cdlemk34  31099  cdlemn11pre  31400  dihord2pre  31415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator