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  2649  euotd  4283  po2nr  4343  fliftfund  5828  frfi  7118  fin33i  8011  axdc3lem4  8095  iscatd  13591  isfuncd  13755  isposd  14105  joinle  14143  pospropd  14254  imasmnd2  14425  grpinveu  14532  grpid  14533  imasgrp2  14626  dmdprdd  15253  pgpfac1lem5  15330  imasrng  15418  islmodd  15649  lmodvsdi1OLD  15667  lmodvsdi2OLD  15669  lmodvsassOLD  15671  lmodvsghm  15702  islssd  15709  islmhm2  15811  psrbaglefi  16134  mulgghm2  16475  isphld  16574  riinopn  16670  ordtbaslem  16934  subbascn  17000  haust1  17096  isnrm2  17102  isnrm3  17103  lmmo  17124  nllyidm  17231  tx1stc  17360  filin  17565  filtop  17566  isfil2  17567  infil  17574  fgfil  17586  isufil2  17619  ufileu  17630  filufint  17631  flimopn  17686  flimrest  17694  isxmetd  17907  met2ndc  18085  icccmplem2  18344  lmmbr  18700  cfil3i  18711  equivcfil  18741  bcthlem5  18766  volfiniun  18920  dvidlem  19281  ulmdvlem3  19795  grporcan  20904  grpoinveu  20905  grpoid  20906  grpoasscan1  20920  cvxpcon  23788  cvxscon  23789  predpo  24255  ax5seg  24638  axcontlem4  24667  axcont  24676  broutsideof2  24817  trooo  25497  cmpltr2  25510  cmperltr  25512  negveud  25771  nn0prpwlem  26341  fgmin  26422  cntotbnd  26623  heiborlem6  26643  heiborlem10  26647  rngonegmn1l  26683  rngonegmn1r  26684  rngoneglmul  26685  rngonegrmul  26686  crngm23  26730  prnc  26795  pridlc3  26801  dmncan1  26804  lsmsat  29820  eqlkr  29911  llncmp  30333  2at0mat0  30336  llncvrlpln  30369  lplncmp  30373  lplnexllnN  30375  lplncvrlvol  30427  lvolcmp  30428  linepsubN  30563  pmapsub  30579  paddasslem16  30646  pmodlem2  30658  lhp2lt  30812  ltrneq2  30959  cdlemf2  31373  cdlemk34  31721  cdlemn11pre  32022  dihord2pre  32037
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